{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:13:56Z","timestamp":1755839636180,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T00:00:00Z","timestamp":1701302400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62002228"],"award-info":[{"award-number":["62002228"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003453","name":"Natural Science Foundation of Guangdong Province","doi-asserted-by":"publisher","award":["2022A1515011458,2022A1515010880"],"award-info":[{"award-number":["2022A1515011458,2022A1515010880"]}],"id":[{"id":"10.13039\/501100003453","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100017610","name":"Shenzhen Science and Technology Innovation Program","doi-asserted-by":"publisher","award":["JCYJ20210324094202008"],"award-info":[{"award-number":["JCYJ20210324094202008"]}],"id":[{"id":"10.13039\/501100017610","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100020595","name":"National Science and Technology Council","doi-asserted-by":"publisher","award":["NSTC110-2221-E-001-008-MY3,NSTC111-2221-E-001-014-MY3,NSTC111-2634-F-002-019"],"award-info":[{"award-number":["NSTC110-2221-E-001-008-MY3,NSTC111-2221-E-001-014-MY3,NSTC111-2634-F-002-019"]}],"id":[{"id":"10.13039\/100020595","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Sinica Investigator Award","award":["AS-IA-109-M01"],"award-info":[{"award-number":["AS-IA-109-M01"]}]},{"name":"Data Safety and Talent Cultivation Project","award":["AS-KPQ-109-DSTCP"],"award-info":[{"award-number":["AS-KPQ-109-DSTCP"]}]},{"name":"Intel Fast Verified Postquantum Software Project","award":[""],"award-info":[{"award-number":[""]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,11,30]]},"DOI":"10.1145\/3611643.3613096","type":"proceedings-article","created":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T23:14:38Z","timestamp":1701386078000},"page":"2167-2171","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-6925-9327","authenticated-orcid":false,"given":"Ruiling","family":"Chen","sequence":"first","affiliation":[{"name":"Shenzhen University, Shenzhen, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6725-8167","authenticated-orcid":false,"given":"Jiaxiang","family":"Liu","sequence":"additional","affiliation":[{"name":"Shenzhen University, Shenzhen, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6277-2813","authenticated-orcid":false,"given":"Xiaomu","family":"Shi","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-7621-7981","authenticated-orcid":false,"given":"Ming-Hsien","family":"Tsai","sequence":"additional","affiliation":[{"name":"National Institute of Cyber Security, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5757-545X","authenticated-orcid":false,"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9362-5282","authenticated-orcid":false,"given":"Bo-Yin","family":"Yang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}]}],"member":"320","published-online":{"date-parts":[[2023,11,30]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_32"},{"key":"e_1_3_2_2_4_1","unstructured":"The NaCl Developers. 2011. NaCl: Networking and Cryptography library. https:\/\/nacl.cr.yp.to\/"},{"key":"e_1_3_2_2_5_1","unstructured":"The wolfSSL Developers. 2023. The wolfSSL Library. https:\/\/github.com\/wolfSSL\/wolfssl"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_40"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354199"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_15"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_39"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_2_12_1","volume-title":"Elliptic curve cryptosystems. Mathematics of computation, 48, 177","author":"Koblitz Neal","year":"1987","unstructured":"Neal Koblitz. 1987. Elliptic curve cryptosystems. Mathematics of computation, 48, 177 (1987), 203\u2013209."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00058"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39799-X_31"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11734727_14"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.4"},{"key":"e_1_3_2_2_18_1","unstructured":"The OpenSSL Project. 2023. The OpenSSL Library. https:\/\/github.com\/openssl\/openssl"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_19"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_16"}],"event":{"name":"ESEC\/FSE '23: 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"San Francisco CA USA","acronym":"ESEC\/FSE '23"},"container-title":["Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3613096","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3611643.3613096","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:10Z","timestamp":1750178230000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3613096"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,30]]},"references-count":21,"alternative-id":["10.1145\/3611643.3613096","10.1145\/3611643"],"URL":"https:\/\/doi.org\/10.1145\/3611643.3613096","relation":{},"subject":[],"published":{"date-parts":[[2023,11,30]]},"assertion":[{"value":"2023-11-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}