Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits

Clemens Hofstadler; Daniela Kaufmann; Chen Chen

doi:10.1007/978-3-032-32589-1_11

Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits

Clemens Hofstadler^*
, Daniela Kaufmann
, Chen Chen

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

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 TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.

Original language	English
Title of host publication	Automated Reasoning
Subtitle of host publication	13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I
Editors	Armin Biere, Carsten Lutz, Sara Negri
Publisher	Springer, Cham
Pages	175-193
Number of pages	19
Edition	1
ISBN (Electronic)	978-3-032-32589-1
ISBN (Print)	978-3-032-32588-4
DOIs	https://doi.org/10.1007/978-3-032-32589-1_11
Publication status	Published - 24 Jul 2026
Event	International Joint Conference, IJCAR 2026 - Edifício II - ISCTE, Lisbon, Portugal Duration: 26 Jul 2026 → 29 Jul 2026 Conference number: 13 https://www.floc26.org/ijcar

Publication series

Name	Lecture Notes in Computer Science
Volume	16688 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Joint Conference, IJCAR 2026
Abbreviated title	IJCAR 2026
Country/Territory	Portugal
City	Lisbon
Period	26.07.2026 → 29.07.2026
Internet address	https://www.floc26.org/ijcar

Fields of science

102031 Theoretical computer science
101005 Computer algebra
102011 Formal languages
102022 Software development
102001 Artificial intelligence
102030 Semantic technologies
101001 Algebra
102 Computer Sciences
101013 Mathematical logic
101 Mathematics
101012 Combinatorics
603109 Logic
101009 Geometry
101020 Technical mathematics

JKU Focus areas

Digital Transformation

Access to Document

10.1007/978-3-032-32589-1_11Licence: CC BY

Cite this

Hofstadler, C., Kaufmann, D., & Chen, C. (2026). Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits. In A. Biere, C. Lutz, & S. Negri (Eds.), Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I (1 ed., pp. 175-193). (Lecture Notes in Computer Science; Vol. 16688 LNCS). Springer, Cham. https://doi.org/10.1007/978-3-032-32589-1_11

Hofstadler, Clemens ; Kaufmann, Daniela ; Chen, Chen. / Avoiding Big Integers : Parallel Multimodular Algebraic Verification of Arithmetic Circuits. Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I. editor / Armin Biere ; Carsten Lutz ; Sara Negri. 1. ed. Springer, Cham, 2026. pp. 175-193 (Lecture Notes in Computer Science).

@inproceedings{bee8aabc7fc548af8df33ca9468ade39,

title = "Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits",

abstract = "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 TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.",

author = "Clemens Hofstadler and Daniela Kaufmann and Chen Chen",

year = "2026",

month = jul,

day = "24",

doi = "10.1007/978-3-032-32589-1\_11",

language = "English",

isbn = "978-3-032-32588-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Cham",

pages = "175--193",

editor = "Armin Biere and Carsten Lutz and Sara Negri",

booktitle = "Automated Reasoning",

edition = "1",

note = "International Joint Conference, IJCAR 2026, IJCAR 2026 ; Conference date: 26-07-2026 Through 29-07-2026",

url = "https://www.floc26.org/ijcar",

}

Hofstadler, C, Kaufmann, D & Chen, C 2026, Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits. in A Biere, C Lutz & S Negri (eds), Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I. 1 edn, Lecture Notes in Computer Science, vol. 16688 LNCS, Springer, Cham, pp. 175-193, International Joint Conference, IJCAR 2026, Lisbon, Portugal, 26.07.2026. https://doi.org/10.1007/978-3-032-32589-1_11

Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits. / Hofstadler, Clemens; Kaufmann, Daniela; Chen, Chen.
Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I. ed. / Armin Biere; Carsten Lutz; Sara Negri. 1. ed. Springer, Cham, 2026. p. 175-193 (Lecture Notes in Computer Science; Vol. 16688 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - Avoiding Big Integers

T2 - International Joint Conference, IJCAR 2026

AU - Hofstadler, Clemens

AU - Kaufmann, Daniela

AU - Chen, Chen

N1 - Conference code: 13

PY - 2026/7/24

Y1 - 2026/7/24

N2 - 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 TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.

AB - 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 TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.

UR - https://link.springer.com/content/pdf/10.1007/978-3-032-32589-1.pdf

UR - https://www.scopus.com/pages/publications/105047026113

U2 - 10.1007/978-3-032-32589-1_11

DO - 10.1007/978-3-032-32589-1_11

M3 - Conference proceedings

SN - 978-3-032-32588-4

T3 - Lecture Notes in Computer Science

SP - 175

EP - 193

BT - Automated Reasoning

A2 - Biere, Armin

A2 - Lutz, Carsten

A2 - Negri, Sara

PB - Springer, Cham

Y2 - 26 July 2026 through 29 July 2026

ER -

Hofstadler C, Kaufmann D, Chen C. Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits. In Biere A, Lutz C, Negri S, editors, Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I. 1 ed. Springer, Cham. 2026. p. 175-193. (Lecture Notes in Computer Science). doi: 10.1007/978-3-032-32589-1_11

Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits

Abstract

Publication series

Conference

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cluster of Excellence "Bilateral Artificial Intelligence"