{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T10:32:33Z","timestamp":1760783553192,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,3,26]],"date-time":"2012-03-26T00:00:00Z","timestamp":1332720000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2012,3,26]]},"DOI":"10.1145\/2245276.2231986","type":"proceedings-article","created":{"date-parts":[[2012,6,11]],"date-time":"2012-06-11T13:03:31Z","timestamp":1339419811000},"page":"1326-1331","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["On construction of a library of formally verified low-level arithmetic functions"],"prefix":"10.1145","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[{"name":"National Institute of Advanced Industrial Science and Technology Central, Umezono, Tsukuba, Ibaraki, Japan"}]}],"member":"320","published-online":{"date-parts":[[2012,3,26]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"volume-title":"Addison-Wesley","year":"1997","author":"Knuth D. E.","key":"e_1_3_2_1_2_1"},{"volume-title":"5th printing","year":"2001","author":"Menezes A. J.","key":"e_1_3_2_1_3_1"},{"key":"e_1_3_2_1_4_1","unstructured":"MIPS Technologies. MIPS32 4KS Processor Core Family Software User's Manual. 2001.  MIPS Technologies. MIPS32 4KS Processor Core Family Software User's Manual . 2001."},{"key":"e_1_3_2_1_5_1","first-page":"55","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symp. on Logic in Computer Science Proceedings","author":"Reynolds J. C.","year":"2002"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_1_7_1","first-page":"346","volume-title":"11th Annual Asian Computing Science Conf.","volume":"4435","author":"Affeldt R.","year":"2008"},{"volume-title":"Verification of Machine Code Implementations of Arithmetic Functions for Cryptography. In TPHOLs Emerging Trends Proceedings. Technical report 364\/07","year":"2007","author":"Myreen M.","key":"e_1_3_2_1_8_1"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_34"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"volume-title":"INRIA","year":"2010","author":"Proof Assistant The Coq","key":"e_1_3_2_1_11_1"},{"key":"e_1_3_2_1_12_1","unstructured":"The GNU Multi Precision Arithmetic Library. Edition 5.0.2. http:\/\/gmplib.org\/. 2011. The GNU Multi Precision Arithmetic Library . Edition 5.0.2. http:\/\/gmplib.org\/. 2011."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926402"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.003"},{"key":"e_1_3_2_1_15_1","first-page":"48","volume-title":"6th Intl. Wksp. on Systems Software Verification Proceedings","author":"Berghofer S.","year":"2011"},{"key":"e_1_3_2_1_16_1","unstructured":"R. Affeldt A Library for Formal Verification of Low-level Programs http:\/\/staff.aist.go.jp\/reynald.affeldt\/coqdev.  R. Affeldt A Library for Formal Verification of Low-level Programs http:\/\/staff.aist.go.jp\/reynald.affeldt\/coqdev."}],"event":{"name":"SAC 2012: ACM Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Trento Italy","acronym":"SAC 2012"},"container-title":["Proceedings of the 27th Annual ACM Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2245276.2231986","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2245276.2231986","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:08:04Z","timestamp":1750273684000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2245276.2231986"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,26]]},"references-count":16,"alternative-id":["10.1145\/2245276.2231986","10.1145\/2245276"],"URL":"https:\/\/doi.org\/10.1145\/2245276.2231986","relation":{},"subject":[],"published":{"date-parts":[[2012,3,26]]},"assertion":[{"value":"2012-03-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}