{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:03:51Z","timestamp":1784844231575,"version":"3.55.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906428","type":"print"},{"value":"9783031906435","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Formal verification techniques based on computer algebra\u00a0have proven highly effective for circuit verification. The circuit, given as an and-inverter graph, is encoded\u00a0using polynomials that automatically generate a Gr\u00f6bner basis with respect to a lexicographic term ordering. Correctness of the circuit is derived by computing\u00a0the polynomial remainder of the specification. However, the main obstacle is the monomial blow-up during the reduction, as the degree can increase.<\/jats:p>\n          <jats:p>In this paper, we investigate an orthogonal approach and focus\u00a0the computational effort on rewriting the Gr\u00f6bner basis itself. Our\u00a0goal is to ensure the basis contains linear polynomials that can\u00a0be effectively used to rewrite the linearized specification. We\u00a0first prove the soundness and completeness of this technique and\u00a0then demonstrate its practical application. Our implementation of\u00a0this method shows promising results on benchmarks related to multiplier verification.<\/jats:p>","DOI":"10.1007\/978-3-031-90643-5_19","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:31Z","timestamp":1745993311000},"page":"355-374","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Extracting Linear Relations from Gr\u00f6bner Bases for Formal Verification of And-Inverter Graphs"],"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-0002-9011-2211","authenticated-orcid":false,"given":"J\u00e9r\u00e9my","family":"Berthomieu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"19_CR1","unstructured":"Berkeley Logic Synthesis and Verification Group: ABC: A System for Sequential Synthesis and Verification. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/ (2019), bitbucket Version 1.01"},{"key":"19_CR2","doi-asserted-by":"publisher","unstructured":"Berthomieu, J., Neiger, V., Safey El\u00a0Din, M.: Faster Change of Order Algorithm for Gr\u00f6bner Bases under Shape and Stability Assumptions. In: ISSAC. pp. 409\u2013418. ACM (2022). https:\/\/doi.org\/10.1145\/3476446.3535484","DOI":"10.1145\/3476446.3535484"},{"key":"19_CR3","doi-asserted-by":"publisher","unstructured":"Berthomieu, J., Eder, C., Safey El Din, M.: msolve: A Library for Solving Polynomial Systems. In: ISSAC. pp. 51\u201358. ACM (2021). https:\/\/doi.org\/10.1145\/3452143.3465545","DOI":"10.1145\/3452143.3465545"},{"key":"19_CR4","unstructured":"Biere, A.: Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016. In: SAT Competition 2016. Dep. of Computer Science Report Series B, vol. B-2016-1, pp. 65\u201366. University of Helsinki (2016)"},{"key":"19_CR5","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Ph.D. thesis, University of Innsbruck (1965)"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Buchberger, B., Kauers, M.: Gr\u00f6bner basis. Scholarpedia 5(10), \u00a07763 (2010), http:\/\/www.scholarpedia.org\/article\/Groebner_basis","DOI":"10.4249\/scholarpedia.7763"},{"key":"19_CR7","doi-asserted-by":"publisher","unstructured":"Chen, Y., Bryant, R.E.: Verification of Arithmetic Circuits with Binary Moment Diagrams. In: DAC. pp. 535\u2013541. ACM (1995). https:\/\/doi.org\/10.1145\/217474.217583","DOI":"10.1145\/217474.217583"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms. Springer-Verlag New York (1997)","DOI":"10.1007\/978-1-4757-2693-0"},{"key":"19_CR9","doi-asserted-by":"publisher","unstructured":"Faug\u00e8re, J.Ch.: A New Efficient Algorithm for Computing Gr\u00f6bner bases (F4). Journal of Pure and Applied Algebra 139(1), 61\u201388 (1999). https:\/\/doi.org\/10.1016\/S0022-4049(99)00005-5","DOI":"10.1016\/S0022-4049(99)00005-5"},{"key":"19_CR10","doi-asserted-by":"publisher","unstructured":"Faug\u00e8re, J.Ch., Gaudry, P., Huot, L., Renault, G.: Sub-Cubic Change of Ordering for Gr\u00f6bner Basis: A Probabilistic Approach. In: ISSAC. pp. 170\u2013177. ACM (2014). https:\/\/doi.org\/10.1145\/2608628.2608669","DOI":"10.1145\/2608628.2608669"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"Faug\u00e8re, J.Ch., Gianni, P., Lazard, D., Mora, T.: Efficient Computation of Zero-dimensional Gr\u00f6bner Bases by Change of Ordering. J. Symbolic Comput. 16(4), 329\u2013344 (1993). https:\/\/doi.org\/10.1006\/jsco.1993.1051","DOI":"10.1006\/jsco.1993.1051"},{"key":"19_CR12","doi-asserted-by":"publisher","unstructured":"Faug\u00e8re, J.Ch., Mou, C.: Sparse FGLM algorithms. Journal of Symbolic Computation 80(3), 538\u2013569 (2017). https:\/\/doi.org\/10.1016\/j.jsc.2016.07.025","DOI":"10.1016\/j.jsc.2016.07.025"},{"key":"19_CR13","doi-asserted-by":"publisher","unstructured":"Homma, N., Watanabe, Y., Aoki, T., Higuchi, T.: Formal Design of Arithmetic Circuits Based on Arithmetic Description Language. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. 89-A(12), 3500\u20133509 (2006). https:\/\/doi.org\/10.1093\/IETFEC\/E89-A.12.3500","DOI":"10.1093\/IETFEC\/E89-A.12.3500"},{"key":"19_CR14","unstructured":"Kaufmann, D.: MultiLinG (2025), https:\/\/www.github.com\/d-kfmnn\/multiling"},{"key":"19_CR15","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Beame, P., Biere, A., Nordstr\u00f6m, J.: Adding dual variables to algebraic reasoning for gate-level multiplier verification. In: DATE. pp. 1431\u20131436. IEEE (2022). https:\/\/doi.org\/10.23919\/DATE54114.2022.9774587","DOI":"10.23919\/DATE54114.2022.9774587"},{"key":"19_CR16","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Berthomieu, J.: MultiLinG - Extracting Linear Relations from Gr\u00f6bner Bases for Formal Verification of And-Inverter Graphs (Artifact) (2025). https:\/\/doi.org\/10.5281\/zenodo.14609934","DOI":"10.5281\/zenodo.14609934"},{"key":"19_CR17","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Biere, A.: Amulet 2.0 for verifying multiplier circuits. In: TACAS (2). LNCS, vol. 12652, pp. 357\u2013364. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_19","DOI":"10.1007\/978-3-030-72013-1_19"},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Biere, A., Kauers, M.: Verifying Large Multipliers by Combining SAT and Computer Algebra. In: FMCAD 2019. pp. 28\u201336. IEEE (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894250","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Biere, A., Kauers, M.: Incremental Column-wise verification of arithmetic circuits using computer algebra. Formal Methods Syst. Des. 56(1), 22\u201354 (2020). https:\/\/doi.org\/10.1007\/S10703-018-00329-2","DOI":"10.1007\/S10703-018-00329-2"},{"key":"19_CR20","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Fleury, M., Biere, A., Kauers, M.: Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Past\u00e8que and Nuss-Checker. Formal Methods in System Design , 1\u201335 (2022). https:\/\/doi.org\/10.1007\/s10703-022-00391-x","DOI":"10.1007\/s10703-022-00391-x"},{"key":"19_CR21","doi-asserted-by":"publisher","unstructured":"Konrad, A., Scholl, C.: Symbolic Computer Algebra for Multipliers Revisited - It\u2019s All About Orders and Phases. In: FMCAD 2024. pp. 261\u2013271. TU Wien Academic Press (2024). https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_32","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_32"},{"key":"19_CR22","doi-asserted-by":"publisher","unstructured":"Konrad, A., Scholl, C., Mahzoon, A., Gro\u00dfe, D., Drechsler, R.: Divider verification using symbolic computer algebra and delayed don\u2019t care optimization. In: FMCAD. pp. 1\u201310. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_17","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_17"},{"key":"19_CR23","doi-asserted-by":"publisher","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE TCAD 21(12), 1377\u20131394 (2002). https:\/\/doi.org\/10.1109\/TCAD.2002.804386","DOI":"10.1109\/TCAD.2002.804386"},{"key":"19_CR24","doi-asserted-by":"publisher","unstructured":"Li, R., Li, L., Yu, H., Fujita, M., Jiang, W., Ha, Y.: Refscat: Formal verification of logic-optimized multipliers via automated reference multiplier generation and sca-sat synergy. IEEE TCAD pp.\u00a01\u20131 (2024). https:\/\/doi.org\/10.1109\/TCAD.2024.3442987","DOI":"10.1109\/TCAD.2024.3442987"},{"key":"19_CR25","doi-asserted-by":"publisher","unstructured":"Liew, V., Beame, P., Devriendt, J., Elffers, J., Nordstr\u00f6m, J.: Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning. In: FMCAD 2020. FMCAD, vol.\u00a01, pp. 194\u2013204. TU Vienna Academic Press (2020). https:\/\/doi.org\/10.34727\/2020\/ISBN.978-3-85448-042-6_27","DOI":"10.34727\/2020\/ISBN.978-3-85448-042-6_27"},{"key":"19_CR26","doi-asserted-by":"publisher","unstructured":"Liu, H., Liao, P., Huang, J., Zhen, H.L., Yuan, M., Ho, T.Y., Yu, B.: Parallel gr\u00f6bner basis rewriting and memory optimization for efficient multiplier verification. In: DATE. pp.\u00a01\u20136 (2024). https:\/\/doi.org\/10.23919\/DATE58400.2024.10546568","DOI":"10.23919\/DATE58400.2024.10546568"},{"key":"19_CR27","doi-asserted-by":"publisher","unstructured":"Lv, J., Kalla, P., Enescu, F.: Efficient Gr\u00f6bner Basis Reductions for Formal Verification of Galois Field Arithmetic Circuits. IEEE TCAD 32(9), 1409\u20131420 (2013). https:\/\/doi.org\/10.1109\/TCAD.2013.2259540","DOI":"10.1109\/TCAD.2013.2259540"},{"key":"19_CR28","doi-asserted-by":"publisher","unstructured":"Mahzoon, A., Gro\u00dfe, D., Drechsler, R.: PolyCleaner: Clean your Polynomials before Backward Rewriting to verify Million-gate Multipliers. In: ICCAD 2018. pp. 129:1 \u2013 129:8. ACM (2018). https:\/\/doi.org\/10.1145\/3240765.3240837","DOI":"10.1145\/3240765.3240837"},{"key":"19_CR29","doi-asserted-by":"publisher","unstructured":"Mahzoon, A., Gro\u00dfe, D., Scholl, C., Drechsler, R.: Towards formal verification of optimized and industrial multipliers. In: DATE. pp. 544\u2013549. IEEE (2020). https:\/\/doi.org\/10.23919\/DATE48585.2020.9116485","DOI":"10.23919\/DATE48585.2020.9116485"},{"key":"19_CR30","doi-asserted-by":"publisher","unstructured":"Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Adv. Math. 46(3), 305\u2013329 (1982). https:\/\/doi.org\/10.1016\/0001-8708(82)90048-2","DOI":"10.1016\/0001-8708(82)90048-2"},{"key":"19_CR31","doi-asserted-by":"publisher","unstructured":"Neiger, V., Schost, \u00c9.: Computing syzygies in finite dimension using fast linear algebra. J. Complex. 60, 101502 (2020). https:\/\/doi.org\/10.1016\/j.jco.2020.101502","DOI":"10.1016\/j.jco.2020.101502"},{"key":"19_CR32","unstructured":"Sharangpani, H., Barton, M.L.: Statistical analysis of floating point flaw in the pentium processor (1994)"},{"key":"19_CR33","doi-asserted-by":"publisher","unstructured":"Temel, M.: Vescmul: Verified implementation of s-c-rewriting for multiplier verification. In: TACAS (1). LNCS, vol. 14570, pp. 340\u2013349. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_19","DOI":"10.1007\/978-3-031-57246-3_19"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90643-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:37Z","timestamp":1745993317000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90643-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906428","9783031906435"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90643-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}