{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T11:00:41Z","timestamp":1784804441396,"version":"3.55.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325884","type":"print"},{"value":"9783032325891","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word sizes grow. In this paper, we present a hybrid algebraic verification technique based on polynomial reasoning that combines linear and nonlinear rewriting. Our approach relies on multimodular reasoning using homomorphic images, where computations are performed in parallel modulo different primes, thereby avoiding any large-integer arithmetic. We implement the proposed method in the verification tool\n                    <jats:sc>TalisMan2.0<\/jats:sc>\n                    and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32589-1_11","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:02:01Z","timestamp":1784800921000},"page":"175-193","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Avoiding Big Integers: Parallel Multimodular Algebraic Verification of\u00a0Arithmetic Circuits"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3025-0604","authenticated-orcid":false,"given":"Clemens","family":"Hofstadler","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5645-0292","authenticated-orcid":false,"given":"Daniela","family":"Kaufmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-8825-6260","authenticated-orcid":false,"given":"Chen","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"issue":"4","key":"11_CR1","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1016\/S0747-7171(02)00140-2","volume":"35","author":"EA Arnold","year":"2003","unstructured":"Arnold, E.A.: Modular algorithms for computing Gr\u00f6bner bases. J. Symb. Comput. 35(4), 403\u2013419 (2003)","journal-title":"J. Symb. Comput."},{"key":"11_CR2","unstructured":"Berkeley Logic Synthesis and Verification Group: ABC: a system for sequential synthesis and verification (2019). http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/, bitbucket Version 1.01"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Gurfinkel, A., Ganesh, V. (eds.) Proceedings of the 36th International Conference on Computer Aided Verification (CAV) 2024, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 133\u2013152. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","DOI":"10.1007\/978-3-031-65627-9_7"},{"issue":"4","key":"11_CR4","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1145\/321662.321664","volume":"18","author":"WS Brown","year":"1971","unstructured":"Brown, W.S.: On Euclid\u2019s algorithm and the computation of polynomial greatest common divisors. J. ACM 18(4), 478\u2013504 (1971)","journal-title":"J. ACM"},{"key":"11_CR5","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Ph.D. thesis, University of Innsbruck (1965)"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Cox, D.A., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms - An Introduction to Computational Algebraic Geometry and Commutative Algebra, 2nd edn. Undergraduate Texts in Mathematics, Springer, New York, NY (1997). https:\/\/doi.org\/10.1007\/978-1-4757-2693-0","DOI":"10.1007\/978-1-4757-2693-0"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Cox, D.A., Little, J., O\u2019Shea, D.: Using Algebraic Geometry. Springer, New York, NY (2005). https:\/\/doi.org\/10.1007\/b138611","DOI":"10.1007\/b138611"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Gerhard, J., Von\u00a0zur Gathen, J.: Modern Computer Algebra, 3rd edn. Cambridge University Press (2013)","DOI":"10.1017\/CBO9781139856065"},{"key":"11_CR9","unstructured":"GMP: The GNU multiple precision arithmetic library. https:\/\/gmplib.org"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Golia, P., Soos, M., Chakraborty, S., Meel, K.S.: Designing samplers is easy: the boon of testers. In: Proceedings of 2021 Formal Methods in Computer Aided Design (FMCAD), pp. 222\u2013230 (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_31","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_31"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Heisinger, M., Hofstadler, C.: f4ncgb: high performance Gr\u00f6bner basis computations in free algebras. In: Boulier, F., Mou, C., Sadykov, T.M., Vorozhtsov, E.V. (eds.) Proceedings of the International Workshop on Computer Algebra in Scientific Computing (CASC) 2025, pp. 79\u201397. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-032-09645-6_5","DOI":"10.1007\/978-3-032-09645-6_5"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Hofstadler, C., Kaufmann, D.: TalisMan. https:\/\/doi.org\/10.4230\/artifacts.23376, https:\/\/github.com\/d-kfmnn\/talisman\/tree\/be8187d, software, version 1.0., swhId: swh:1:dir:8af022a61661d2b7fb281abbdc2f18d51f221c20 (visited on 2025-08-08)","DOI":"10.4230\/artifacts.23376"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Hofstadler, C., Kaufmann, D.: Guess and prove: a hybrid approach to linear polynomial recovery in circuit verification. In: Proceedings of the 31st International Conference on Principles and Practice of Constraint Programming (CP) 2025. Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0340, pp. 14:1\u201314:22 (2025). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2025.14","DOI":"10.4230\/LIPIcs.CP.2025.14"},{"key":"11_CR14","unstructured":"Hofstadler, C., Kaufmann, D., Chen, C.: Avoiding big integers: parallel multimodular algebraic verification of arithmetic circuits. arXiv:2603.09501 (2026), extended version with appendices"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Hofstadler, C., Kaufmann, D., Chen, C.: TalisMan2.0 - Artifact (2026). https:\/\/doi.org\/10.5281\/zenodo.20019348","DOI":"10.5281\/zenodo.20019348"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"102581","DOI":"10.1016\/j.jsc.2026.102581","volume":"137","author":"C Hofstadler","year":"2026","unstructured":"Hofstadler, C., Levandovskyy, V.: Modular algorithms for computing Gr\u00f6bner bases in free algebras. J. Symb. Comput. 137, 102581 (2026)","journal-title":"J. Symb. Comput."},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"102325","DOI":"10.1016\/j.jsc.2024.102325","volume":"125","author":"C Hofstadler","year":"2024","unstructured":"Hofstadler, C., Verron, T.: Short proofs of ideal membership. J. Symb. Comput. 125, 102325 (2024)","journal-title":"J. Symb. Comput."},{"key":"11_CR18","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":"11_CR19","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: Proceedings of 2022 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1431\u20131436. IEEE (2022). https:\/\/doi.org\/10.23919\/DATE54114.2022.9774587","DOI":"10.23919\/DATE54114.2022.9774587"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Berthomieu, J.: Extracting linear relations from Gr\u00f6bner bases for formal verification of and-inverter graphs. In: Gurfinkel, A., Heule, M. (eds.) Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 15696, pp. 355\u2013374. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_19","DOI":"10.1007\/978-3-031-90643-5_19"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Biere, A.: AMulet 2.0 for verifying multiplier circuits. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 12652, pp. 357\u2013364. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_19","DOI":"10.1007\/978-3-030-72013-1_19"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Biere, A., Kauers, M.: Verifying large multipliers by combining SAT and computer algebra. In: Proceedings of Formal Methods in Computer Aided Design (FMCAD), pp. 28\u201336. IEEE (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894250","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"11_CR23","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":"11_CR24","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 Syst. Des. 64(1), 73\u2013107 (2024). https:\/\/doi.org\/10.1007\/s10703-022-00391-x","DOI":"10.1007\/s10703-022-00391-x"},{"key":"11_CR25","unstructured":"Kaufmann, D., Hofstadler, C.: Recycling algebraic proof certificates. In: Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square) 2025, vol. 4116, pp. 35\u201340. Ceur (2025). https:\/\/ceur-ws.org\/Vol-4116\/"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Konrad, A., Scholl, C.: FastPoly: an efficient polynomial package for the verification of integer arithmetic circuits. In: Proceedings of Formal Methods in Computer Aided Design (FMCAD), pp. 139\u2013144 (2025). https:\/\/doi.org\/10.34727\/2025\/isbn.978-3-85448-084-6_20","DOI":"10.34727\/2025\/isbn.978-3-85448-084-6_20"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Konrad, A., Scholl, C.: Symbolic computer algebra for multipliers revisited - It\u2019s all about orders and phases. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD), pp. 261\u2013271. IEEE (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":"11_CR28","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: Proceedings of Formal Methods in Computer-Aided Design (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":"11_CR29","doi-asserted-by":"publisher","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 21(12), 1377\u20131394 (2002). https:\/\/doi.org\/10.1109\/TCAD.2002.804386","DOI":"10.1109\/TCAD.2002.804386"},{"key":"11_CR30","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: Proceedings of International Conference on Computer-Aided Design (ICCAD). ACM (2018). https:\/\/doi.org\/10.1145\/3240765.3240837","DOI":"10.1145\/3240765.3240837"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Mahzoon, A., Gro\u00dfe, D., Scholl, C., Drechsler, R.: Towards formal verification of optimized and industrial multipliers. In: Proceedings of Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 544\u2013549. IEEE (2020). https:\/\/doi.org\/10.23919\/DATE48585.2020.9116485","DOI":"10.23919\/DATE48585.2020.9116485"},{"issue":"3","key":"11_CR32","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","volume":"46","author":"EW Mayr","year":"1982","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)","journal-title":"Adv. Math."},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Monagan, M., Pearce, R.: A compact parallel implementation of F4. In: Proceedings of the 2015 International Workshop on Parallel Symbolic Computation, pp. 95\u2013100 (2015)","DOI":"10.1145\/2790282.2790293"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Philipp, T., Steinke, P.: PBLib - A library for encoding pseudo-boolean constraints into CNF. In: Heule, M., Weaver, S. (eds.) Proceedings of 18th International Conference on Theory and Applications of Satisfiability Testing (SAT) 2015. LNCS, vol.\u00a09340, pp. 9\u201316. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_2","DOI":"10.1007\/978-3-319-24318-4_2"},{"key":"11_CR35","unstructured":"Rosen, K.H.: Elementary Number Theory and Its Applications, Pearson Education London (2011)"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Stein, W.A.: Modular Forms: A Computational Approach, vol. 79. American Mathematical Society (2007)","DOI":"10.1090\/gsm\/079"},{"key":"11_CR37","unstructured":"The FLINT team: FLINT: fast library for number theory (2025). https:\/\/flintlib.org, version 3.4.0"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32589-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:02:08Z","timestamp":1784800928000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32589-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325884","9783032325891"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32589-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/ijcar","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}