{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:42:24Z","timestamp":1740134544667,"version":"3.37.3"},"reference-count":16,"publisher":"Wiley","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61272002","91218302","010CB328003"],"award-info":[{"award-number":["61272002","91218302","010CB328003"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61272002","91218302","010CB328003"],"award-info":[{"award-number":["61272002","91218302","010CB328003"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004407","name":"Tsinghua National Laboratory for Information Science and Technology","doi-asserted-by":"publisher","award":["61272002","91218302","010CB328003"],"award-info":[{"award-number":["61272002","91218302","010CB328003"]}],"id":[{"id":"10.13039\/501100004407","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012166","name":"National Basic Research Program of China","doi-asserted-by":"crossref","award":["61272002","91218302","010CB328003"],"award-info":[{"award-number":["61272002","91218302","010CB328003"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2014]]},"abstract":"<jats:p>Addition arithmetic design plays a crucial role in high performance digital systems. The paper proposes a systematic method to formalize and verify adders in a formal proof assistant C<jats:sc>OQ<\/jats:sc>. The proposed approach succeeds in formalizing the gate-level implementations and verifying the functional correctness of the most important adders of interest in industry, in a faithful, scalable, and modularized way. The methodology can be extended to other adder architectures as well.<\/jats:p>","DOI":"10.1155\/2014\/197252","type":"journal-article","created":{"date-parts":[[2014,4,10]],"date-time":"2014-04-10T21:01:23Z","timestamp":1397163683000},"page":"1-9","source":"Crossref","is-referenced-by-count":2,"title":["Functional Verification of High Performance Adders in COQ"],"prefix":"10.1155","volume":"2014","author":[{"given":"Qian","family":"Wang","sequence":"first","affiliation":[{"name":"School of Software, Tsinghua University, Beijing 100084, China"}]},{"given":"Xiaoyu","family":"Song","sequence":"additional","affiliation":[{"name":"Department of ECE, Portland State University, Portland, OR 97207, USA"}]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[{"name":"School of Software, Tsinghua University, Beijing 100084, China"}]},{"given":"Jiaguang","family":"Sun","sequence":"additional","affiliation":[{"name":"School of Software, Tsinghua University, Beijing 100084, China"}]}],"member":"311","reference":[{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-97226-9_34"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/54.143145"},{"year":"1986","key":"3"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_72"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0048-3"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_24"},{"year":"1993","key":"9"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005180"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1016\/j.mcm.2010.02.008"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2009.2034346"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008610818519"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_11"},{"key":"16","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"653","volume-title":"Semantics of intensional type theory extended with decidable equational theories","volume":"23","year":"2013"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1147\/rd.252.0156"},{"year":"2002","key":"19"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1973.5009159"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/197252.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/197252.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/197252.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,11]],"date-time":"2020-05-11T21:56:01Z","timestamp":1589234161000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2014\/197252\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":16,"alternative-id":["197252","197252"],"URL":"https:\/\/doi.org\/10.1155\/2014\/197252","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"type":"print","value":"1110-757X"},{"type":"electronic","value":"1687-0042"}],"subject":[],"published":{"date-parts":[[2014]]}}}