{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:20:28Z","timestamp":1778498428681,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,7,10]],"date-time":"2022-07-10T00:00:00Z","timestamp":1657411200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["GR 3104\/6-1, DR 297\/37-1, SCHO 894\/5-1"],"award-info":[{"award-number":["GR 3104\/6-1, DR 297\/37-1, SCHO 894\/5-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,7,10]]},"DOI":"10.1145\/3489517.3530605","type":"proceedings-article","created":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T23:19:29Z","timestamp":1661296769000},"page":"1183-1188","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability"],"prefix":"10.1145","author":[{"given":"Alireza","family":"Mahzoon","sequence":"first","affiliation":[{"name":"University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Gro\u00dfe","sequence":"additional","affiliation":[{"name":"Johannes Kepler University Linz, Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Konrad","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"University of Bremen\/DFKI, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,23]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"A system for sequential synthesis and verification.","year":"2018","unstructured":"Abc: A system for sequential synthesis and verification. available at https:\/\/people.eecs.berkeley.edu\/~alanmi\/abc\/, 2018."},{"key":"e_1_3_2_1_2_1","first-page":"502","volume-title":"SAT","author":"E\u00e9n N.","year":"2003","unstructured":"N. E\u00e9n and N. S\u00f6rensson. An extensible SAT-solver. In SAT, pages 502--518, 2003."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/82.559370"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240837"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3316781.3317898"},{"key":"e_1_3_2_1_8_1","first-page":"544","volume-title":"DATE","author":"Mahzoon A.","year":"2020","unstructured":"A. Mahzoon, D. Gro\u00dfe, C. Scholl, and R. Drechsler. Towards formal verification of optimized and industrial multipliers. In DATE, pages 544--549, 2020."},{"key":"e_1_3_2_1_9_1","volume-title":"Computer Arithmetic : Algorithms and Hardware Designs","author":"Parhami B.","year":"2002","unstructured":"B. Parhami. Computer Arithmetic : Algorithms and Hardware Designs. Oxford University Press Inc, 2002."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2971808.2972053"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218721"},{"key":"e_1_3_2_1_12_1","first-page":"1110","volume-title":"DATE","author":"Scholl C.","year":"2021","unstructured":"C. Scholl, A. Konrad, A. Mahzoon, D. Gro\u00dfe, and R. Drechsler. Verifying dividers using symbolic computer algebra and don't care optimization. In DATE, pages 1110--1115, 2021."},{"key":"e_1_3_2_1_13_1","article-title":"A universal architecture for designing efficient modulo 2n+1 multipliers","author":"Sousa L.","year":"2005","unstructured":"L. Sousa and R. Chaves. A universal architecture for designing efficient modulo 2n+1 multipliers. IEEE Trans. Circuits Syst. I, 52-I(6):1166--1178, 2005.","journal-title":"IEEE Trans. Circuits Syst. I, 52-I(6):1166--1178"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1049\/iet-cdt:20060026"},{"key":"e_1_3_2_1_15_1","first-page":"505","volume-title":"CAV","author":"Walther C.","year":"2018","unstructured":"C. Walther. Formally verified montgomery multiplication. In CAV, pages 505--522, 2018."},{"issue":"9","key":"e_1_3_2_1_16_1","first-page":"1907","article-title":"Fast algebraic rewriting based on and-inverter graphs","volume":"37","author":"Yu C.","year":"2017","unstructured":"C. Yu, M. Ciesielski, and A. Mishchenko. Fast algebraic rewriting based on and-inverter graphs. TCAD, 37(9):1907--1911, 2017.","journal-title":"TCAD"},{"key":"e_1_3_2_1_17_1","first-page":"158","volume-title":"ARITH","author":"Zimmermann R.","year":"1999","unstructured":"R. Zimmermann. Efficient VLSI implementation of modulo (2n \u00b1 1) addition and multiplication. In ARITH, pages 158--167, 1999."}],"event":{"name":"DAC '22: 59th ACM\/IEEE Design Automation Conference","location":"San Francisco California","acronym":"DAC '22","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE CEDA"]},"container-title":["Proceedings of the 59th ACM\/IEEE Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3489517.3530605","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3489517.3530605","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:23Z","timestamp":1750186943000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3489517.3530605"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,10]]},"references-count":16,"alternative-id":["10.1145\/3489517.3530605","10.1145\/3489517"],"URL":"https:\/\/doi.org\/10.1145\/3489517.3530605","relation":{},"subject":[],"published":{"date-parts":[[2022,7,10]]},"assertion":[{"value":"2022-08-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}