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

^*Korrespondierende/r Autor/-in für diese Arbeit

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

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.

Originalsprache	Englisch
Titel	Automated Reasoning
Untertitel	13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I
Herausgeber*innen	Armin Biere, Carsten Lutz, Sara Negri
Verlag	Springer, Cham
Seiten	175-193
Seitenumfang	19
Auflage	1
ISBN (elektronisch)	978-3-032-32589-1
ISBN (Print)	978-3-032-32588-4
DOIs	https://doi.org/10.1007/978-3-032-32589-1_11
Publikationsstatus	Veröffentlicht - 24 Juli 2026
Veranstaltung	International Joint Conference, IJCAR 2026 - Edifício II - ISCTE, Lisbon, Portugal Dauer: 26 Juli 2026 → 29 Juli 2026 Konferenznummer: 13 https://www.floc26.org/ijcar

Publikationsreihe

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

Konferenz

Konferenz	International Joint Conference, IJCAR 2026
Kurztitel	IJCAR 2026
Land/Gebiet	Portugal
Ort	Lisbon
Zeitraum	26.07.2026 → 29.07.2026
Internetadresse	https://www.floc26.org/ijcar

Wissenschaftszweige

102031 Theoretische Informatik
101005 Computeralgebra
102011 Formale Sprachen
102022 Softwareentwicklung
102001 Artificial Intelligence
102030 Semantische Technologien
101001 Algebra
102 Informatik
101013 Mathematische Logik
101 Mathematik
101012 Kombinatorik
603109 Logik
101009 Geometrie
101020 Technische Mathematik

JKU-Schwerpunkte

Digital Transformation

Zugriff auf Dokument

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

Andere Dateien und Links

1 Laufend

Cluster of Excellence "Bilateral Artificial Intelligence"
Fürnkranz, J. (Projektleiter*in), Hochreiter, S. (Projektleiter*in), Klambauer, G. (Projektleiter*in), Schedl, M. (Projektleiter*in), Seidl, M. (Projektleiter*in), Widmer, G. (Projektleiter*in), Brandstetter, J. (Projektleiter*in), Kobler, E. (Projektleiter*in), Aichernig, B. (Projektleiter*in), Heisinger, M. (Forscher*in), Hoedt, P.-J. (Forscher*in), Pfeiffer, P. (Forscher*in), Plank, A. (Forscher*in), Radler, A. (Forscher*in), Rebola Pardo, A. (Forscher*in), Lin, W. (Forscher*in), Eckert, H. (Forscher*in), Cranganore, S. S. (Forscher*in), Hartl, A.-R. (Forscher*in), Plasser, M. (Forscher*in), Pammer, T. (Forscher*in), Tommasel, A. (Forscher*in), Nawaz, S. (Forscher*in), Masoudian, S. (Forscher*in) & Freinschlag, R. (Forscher*in)
01.10.2024 → 30.09.2029
Projekt: Geförderte Forschung › FWF - Österreichischer Wissenschaftsfonds

1 Vorabpublikation

Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits
Hofstadler, C., Kaufmann, D. & Chen, C., 10 März 2026, arXiv, 23 S. (arXiv.org; Nr. 2603.09501).
Publikation: Preprints, Working Paper und Forschungsberichte › Vorabpublikation

Open Access

1 Vortrag nach Bewerbung und Auswahl

Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits
Hofstadler, C. (Vortragende*r)
29 Juli 2026
Aktivität: Vortrag oder Präsentation › Vortrag nach Bewerbung und Auswahl › Science-to-science

Dieses zitieren

Hofstadler, C., Kaufmann, D., & Chen, C. (2026). Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits. in A. Biere, C. Lutz, & S. Negri (Hrsg.), Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I (1 Aufl., S. 175-193). (Lecture Notes in Computer Science; Band 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. Hrsg. / Armin Biere ; Carsten Lutz ; Sara Negri. 1. Aufl. Springer, Cham, 2026. S. 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 (Hrsg.), Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I. 1 Aufl., Lecture Notes in Computer Science, Bd. 16688 LNCS, Springer, Cham, S. 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. Hrsg. / Armin Biere; Carsten Lutz; Sara Negri. 1. Aufl. Springer, Cham, 2026. S. 175-193 (Lecture Notes in Computer Science; Band 16688 LNCS).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

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, Hrsg., Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I. 1 Aufl. Springer, Cham. 2026. S. 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

Publikationsreihe

Konferenz

Wissenschaftszweige

JKU-Schwerpunkte

Zugriff auf Dokument

Andere Dateien und Links

Projekte

Cluster of Excellence "Bilateral Artificial Intelligence"

Publikationen