{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:04:44Z","timestamp":1784844284881,"version":"3.55.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:sc>AMulet\u00a02.0<\/jats:sc> is a fully automatic tool for the verification of integer multipliers using computer algebra. Our tool models multiplier circuits given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gr\u00f6bner bases. Finally it uses a polynomial reduction algorithm to verify the correctness of the given circuit. <jats:sc>AMulet\u00a02.0<\/jats:sc> is a re-factorization and improved re-implementation of our previous multiplier verification tool <jats:sc>AMulet\u00a01.0<\/jats:sc>.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_19","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"357-364","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["AMulet\u00a02.0 for Verifying Multiplier Circuits"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5645-0292","authenticated-orcid":false,"given":"Daniela","family":"Kaufmann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"P. Beame, R. Impagliazzo, J. Kraj\u00edcek, T. Pitassi, and P. Pudl\u00e1k. Lower Bounds on Hilbert\u2019s Nullstellensatz and Propositional Proofs. In Proc. London Math. Society, volume s3-73, pages 1\u201326, 1996.","DOI":"10.1112\/plms\/s3-73.1.1"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"T. Becker, V. Weispfenning, and H. Kredel. Gr\u00f6bner Bases, volume 141 of Graduate texts in mathematics. Springer, 1993.","DOI":"10.1007\/978-1-4612-0913-3_5"},{"key":"19_CR3","unstructured":"A. Biere. Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016. In SAT Competition 2016, volume B-2016-1 of Dep. of Computer Science Report Series B, pages 65\u201366. University of Helsinki, 2016."},{"key":"19_CR4","unstructured":"A. Biere, K. Fazekas, M. Fleury, and M. Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Dep. of Computer Science Report Series B, pages 51\u201353. University of Helsinki, 2020."},{"key":"19_CR5","unstructured":"A. Biere, K. Heljanko, and S. Wieringa. AIGER 1.9 And Beyond. Technical report, FMV Reports Series, JKU Linz, Austria, 2011."},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"R. E. Bryant and Y. Chen. Verification of arithmetic circuits using binary moment diagrams. STTT, 3(2), 137\u2013155, 2001.","DOI":"10.1007\/s100090100037"},{"key":"19_CR7","unstructured":"M. J. Ciesielski, T. Su, A. Yasin, and C. Yu. Understanding Algebraic Rewriting for Arithmetic Circuit Verification: a Bit-Flow Model. IEEE TCAD, pages 1\u20131, 2019. Early acces."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"M. Clegg, J. Edmonds, and R. Impagliazzo. Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability. In STOC 1996, pages 174\u2013183. ACM, 1996.","DOI":"10.1145\/237814.237860"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"D. Cox, J. Little, and D. O\u2019Shea. Ideals, Varieties, and Algorithms. Springer-Verlag, New York, 1997.","DOI":"10.1007\/978-1-4757-2693-0"},{"key":"19_CR10","unstructured":"T. Granlund and the GMP development team. GNU MP: The GNU Multiple Precision Arithmetic Library, 2016. Version 6.1.2."},{"key":"19_CR11","unstructured":"E. Hirsch, D. Itsykson, A. Kojevnikov, E. Kulikov, and S. Nikolenko. Report on the Mixed Boolean-Algebraic Solver. Technical report, Laboratory of Mathematical Logic of St. Petersburg Dep. of Steklov Institute of Mathematics, 2005."},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"N. Homma, Y. Watanabe, T. Aoki, and T. Higuchi. Formal Design of Arithmetic Circuits Based on Arithmetic Description Language. IEICE Transactions, 89-A(12):3500\u20133509, 2006.","DOI":"10.1093\/ietfec\/e89-a.12.3500"},{"key":"19_CR13","unstructured":"D. Kaufmann. Amulet 1.5. https:\/\/github.com\/d-kfmnn\/amulet, 2020."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"D. Kaufmann. Artifact for AMulet2.0 for verifying multiplier circuits. http:\/\/fmv.jku.at\/amulet2_artifact, 2020.","DOI":"10.26226\/morressier.604907f41a80aac83ca25ce2"},{"key":"19_CR15","unstructured":"D. Kaufmann. Formal Verification of Multiplier Circuits using Computer Algebra. PhD thesis, Informatik, Johannes Kepler University Linz, 2020."},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"D. Kaufmann and A. Biere. Nullstellensatz-proofs for multiplier verification. In Computer Algebra in Scientific Computing, volume 12291 of LNCS, pages 368\u2013389. Springer, 2020.","DOI":"10.1007\/978-3-030-60026-6_21"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"D. Kaufmann, A. Biere, and M. Kauers. Verifying Large Multipliers by Combining SAT and Computer Algebra. In FMCAD 2019, pages 28\u201336. IEEE, 2019.","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"D. Kaufmann, A. Biere, and M. Kauers. Incremental Column-wise verification of arithmetic circuits using computer algebra. Formal Methods Syst. Des., 56(1):22\u201354, 2020.","DOI":"10.1007\/s10703-018-00329-2"},{"key":"19_CR19","unstructured":"D. Kaufmann, A. Biere, and M. Kauers. SAT, Computer Algebra, Multipliers. In Vampire 2018 and Vampire 2019, volume 71 of EPiC Series in Computing, pages 1\u201318. EasyChair, 2020."},{"key":"19_CR20","unstructured":"D. Kaufmann, M. Fleury, and A. Biere. Pacheck and Past\u00e8que, Checking Practical Algebraic Calculus Proofs. In FMCAD 2020, volume 1 of FMCAD, pages 264\u2013269. TU Vienna Academic Press, 2020."},{"key":"19_CR21","unstructured":"D. Kaufmann, M. Kauers, A. Biere, and D. Cok. Arithmetic Verification Problems Submitted to the SAT Race 2019. In SAT Race 2019, volume B-2019-1 of Dep. of Computer Science Report Series B, page 49. University of Helsinki, 2019."},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"A. Kuehlmann, V. Paruthi, F. Krohm, and M. Ganai. Robust Boolean reasoning for equivalence checking and functional property verification. IEEE TCAD, 21(12), 1377\u20131394, 2002.","DOI":"10.1109\/TCAD.2002.804386"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"J. Lv, P. Kalla, and F. Enescu. Efficient Gr\u00f6bner Basis Reductions for Formal Verification of Galois Field Arithmetic Circuits. IEEE TCAD, 32(9):1409\u20131420, 2013.","DOI":"10.1109\/TCAD.2013.2259540"},{"key":"19_CR24","unstructured":"A. Mahzoon, D. Gro\u00dfe, and R. Drechsler. PolyCleaner: Clean your Polynomials before Backward Rewriting to verify Million-gate Multipliers. In ICCAD 2018, pages 129:1\u2013129:8. ACM, 2018."},{"key":"19_CR25","unstructured":"A. Mahzoon, D. Gro\u00dfe, and R. Drechsler. RevSCA: Using Reverse Engineering to Bring Light into Backward Rewriting for Big and Dirty Multipliers. In DAC 2019, pages 185:1\u2013185:6. ACM, 2019."},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"A. Mahzoon, D. Gro\u00dfe, C. Scholl, and R. Drechsler. Towards formal verification of optimized and industrial multipliers. In DATE, pages 544\u2013549. IEEE, 2020.","DOI":"10.23919\/DATE48585.2020.9116485"},{"key":"19_CR27","unstructured":"B. Parhami. Computer Arithmetic - Algorithms and Hardware designs. Oxford University Press, 2000."},{"key":"19_CR28","unstructured":"H. Sharangpani and M. L. Barton. Statistical analysis of floating point flaw in the pentium processor. 1994."},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"M. Temel, A. Slobodov\u00e1, and W. A. Hunt. Automated and scalable verification of integer multipliers. In CAV (1), volume 12224 of Lecture Notes in Computer Science, pages 485\u2013507. Springer, 2020.","DOI":"10.1007\/978-3-030-53288-8_23"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72013-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:15:38Z","timestamp":1616436938000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}