3 papers
cs.SC2026
Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits
Clemens Hofstadler, Daniela Kaufmann, Chen Chen
Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word…
cs.SC2025
Recycling Algebraic Proof Certificates
Daniela Kaufmann, Clemens Hofstadler
Proof certificates can be used to validate the correctness of algebraic derivations. However, in practice, we frequently observed that the exact same proof steps are repeated for d…
cs.SC2025
Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs
Daniela Kaufmann, Jérémy Berthomieu
Formal verification techniques based on computer algebra have proven highly effective for circuit verification. The circuit, given as an and-inverter graph, is encoded as a set of…