2024 |
Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner, Laura Kovács PolySAT: Word-level Bit-vector Reasoning in Z3 Conference International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2024. @conference{RathEisenhoferKaufmannBjornerKovacs-VSTTE24, title = {PolySAT: Word-level Bit-vector Reasoning in Z3}, author = {Jakob Rath and Clemens Eisenhofer and Daniela Kaufmann and Nikolaj Bjørner and Laura Kovács}, url = {https://arxiv.org/abs/2406.04696, PrePrint}, year = {2024}, date = {2024-10-15}, booktitle = { International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE)}, abstract = {PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For the purpose of conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has potential applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For the purpose of conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has potential applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale. |
Thomas Hader, Daniela Kaufmann, Stéphan Graham-Lengrand, Ahmed Irfan, Laura Kovács MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver Conference International Joint Conference on Automated Reasoning (IJCAR), 2024. @conference{HaderKaufmannGrahamIrfanKovacs-IJCAR24, title = {MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver}, author = {Thomas Hader and Daniela Kaufmann and Stéphan Graham-Lengrand and Ahmed Irfan and Laura Kovács}, url = {https://danielakaufmann.at/wp-content/uploads/2024/07/978-3-031-63498-7_23.pdf, Paper https://merz.gitlabpages.inria.fr/2024-ijcar/, Conference}, year = {2024}, date = {2024-07-01}, booktitle = {International Joint Conference on Automated Reasoning (IJCAR)}, abstract = {This system description introduces an enhancement to the YICES2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is based on zero decomposition techniques, which find finite basis explanations for theory conflicts over finite fields. As the MCSat solver within YICES2 can support (and combine) several theories via theory plugins, we implemented our reasoning approach as a new plugin for finite fields and extended YICES2 ’s frontend to parse finite field problems, making our implementation the first MCSat-based reasoning engine for finite fields. We present its evaluation on finite field benchmarks, comparing it against cvc5. Additionally, our work leverages the modular architecture of the MCSat solver in YICES2 to provide a foundation for the rapid implementation of further reasoning techniques for this theory.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } This system description introduces an enhancement to the YICES2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is based on zero decomposition techniques, which find finite basis explanations for theory conflicts over finite fields. As the MCSat solver within YICES2 can support (and combine) several theories via theory plugins, we implemented our reasoning approach as a new plugin for finite fields and extended YICES2 ’s frontend to parse finite field problems, making our implementation the first MCSat-based reasoning engine for finite fields. We present its evaluation on finite field benchmarks, comparing it against cvc5. Additionally, our work leverages the modular architecture of the MCSat solver in YICES2 to provide a foundation for the rapid implementation of further reasoning techniques for this theory. |
Hannes Sochor, Flavio Ferrarotti and Daniela Kaufmann Fuzzing-based grammar learning from a minimal set of seed inputs Journal Journal of Computer Languages, 2024. @article{SochorFerrarrottiKaufmann2023, title = {Fuzzing-based grammar learning from a minimal set of seed inputs}, author = {Hannes Sochor and Flavio Ferrarotti and Daniela Kaufmann}, url = {https://www.sciencedirect.com/science/article/abs/pii/S259011842300062X, Article}, year = {2024}, date = {2024-03-01}, journal = {Journal of Computer Languages}, abstract = {To be effective, a fuzzer needs to generate inputs that are well formed, so that they are not outright rejected by the Software Under Test (SUT) and can thus detect meaningful bugs. Grammar based fuzzers solve this problem, but they obviously require a grammar of the input language accepted by the SUT. Many times such grammar is unknown. Therefore, different black- and white-box algorithms have been proposed for learning them from SUTs. Black-box algorithms rely only on membership queries, but need access to carefully crafted well formed inputs in order to obtain good results. White-box algorithms require access to the source code and generally produce grammars with higher precision and recall, but at the expense of working only for specific programming languages and libraries. We propose a new algorithm and show through extensive experimentation that it can learn grammars from recursive descendent parsers with consistently high levels of both, recall and precision. Notably, this result was obtained starting with a couple of arbitrary seed inputs and includes evaluations with sophisticated languages such as Java Script Object Notation (JSON). Different to other state of the art white-box approaches, our method does not require sophisticated program analysis techniques such as dynamic tainting or symbolic execution. In fact, the experiments confirm that our method performs extremely well with just a (standard) generic Abstract Syntax Tree (AST) of the parsing program as input. The core of our method uses fuzzing techniques combined with fundamental theoretical results on grammar learning. Compared to other white-box approaches, ours is not tied to specific programming languages and tools, and thus can be easily ported. Regarding performance, we have shown that our algorithm works well in practice and that, under reasonable assumptions, its worst-case complexity is polynomial (with low exponents) w.r.t. time and space requirements.}, keywords = {}, pubstate = {published}, tppubtype = {article} } To be effective, a fuzzer needs to generate inputs that are well formed, so that they are not outright rejected by the Software Under Test (SUT) and can thus detect meaningful bugs. Grammar based fuzzers solve this problem, but they obviously require a grammar of the input language accepted by the SUT. Many times such grammar is unknown. Therefore, different black- and white-box algorithms have been proposed for learning them from SUTs. Black-box algorithms rely only on membership queries, but need access to carefully crafted well formed inputs in order to obtain good results. White-box algorithms require access to the source code and generally produce grammars with higher precision and recall, but at the expense of working only for specific programming languages and libraries. We propose a new algorithm and show through extensive experimentation that it can learn grammars from recursive descendent parsers with consistently high levels of both, recall and precision. Notably, this result was obtained starting with a couple of arbitrary seed inputs and includes evaluations with sophisticated languages such as Java Script Object Notation (JSON). Different to other state of the art white-box approaches, our method does not require sophisticated program analysis techniques such as dynamic tainting or symbolic execution. In fact, the experiments confirm that our method performs extremely well with just a (standard) generic Abstract Syntax Tree (AST) of the parsing program as input. The core of our method uses fuzzing techniques combined with fundamental theoretical results on grammar learning. Compared to other white-box approaches, ours is not tied to specific programming languages and tools, and thus can be easily ported. Regarding performance, we have shown that our algorithm works well in practice and that, under reasonable assumptions, its worst-case complexity is polynomial (with low exponents) w.r.t. time and space requirements. |
Mathias Fleury, Daniela Kaufmann Life span of SAT techniques Workshop Pragmatics of SAT 2023, 2024. @conference{FleuryKaufmann-POS23, title = {Life span of SAT techniques}, author = {Mathias Fleury and Daniela Kaufmann}, url = {https://arxiv.org/pdf/2402.01202.pdf, Article http://www.pragmaticsofsat.org/2023/, Workshop https://zenodo.org/records/10608480, Data}, year = {2024}, date = {2024-02-01}, booktitle = {Pragmatics of SAT 2023}, abstract = {In this paper we take 4 different features of the SAT solver CaDiCaL, blocked clause elimination, vivification, on-the-fly self subsumption, and increasing the bound of variable elimination over the SAT Competitions benchmarks between 2009 and 2022. We study these features by both activating them one-by-one and deactivating them one-by-one. We have three hypothesis regarding the experiments: (i) disabling features is always harmful; (ii) the life span of the techniques is limited; and (iii) features simulate each other. Our experiments cannot confirm any of the hypothesis.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } In this paper we take 4 different features of the SAT solver CaDiCaL, blocked clause elimination, vivification, on-the-fly self subsumption, and increasing the bound of variable elimination over the SAT Competitions benchmarks between 2009 and 2022. We study these features by both activating them one-by-one and deactivating them one-by-one. We have three hypothesis regarding the experiments: (i) disabling features is always harmful; (ii) the life span of the techniques is limited; and (iii) features simulate each other. Our experiments cannot confirm any of the hypothesis. |
2023 |
Thomas Hader, Daniela Kaufmann, Laura Kovács SMT Solving over Finite Field Arithmetic Conference In Proc. of 24th Intl. Conf. Logic for Programming, Artificial Intelligence and Reasoning (LPAR), 2023. @conference{HaderKaufmannKovacs-LPAR23, title = {SMT Solving over Finite Field Arithmetic}, author = {Thomas Hader, Daniela Kaufmann, Laura Kovács}, url = {https://danielakaufmann.at/wp-content/uploads/2023/07/HaderKaufmannKovacs_LPAR23.pdf, Paper https://github.com/Ovascos/ffsat, Data https://easychair.org/smart-program/LPAR2023/index.html, Conference }, year = {2023}, date = {2023-06-03}, booktitle = {In Proc. of 24th Intl. Conf. Logic for Programming, Artificial Intelligence and Reasoning (LPAR)}, abstract = {Non-linear polynomial systems over finite fields are used to model functional behavior of cryptosystems, with applications in system security, computer cryptography, and post- quantum cryptography. Solving polynomial systems is also one of the most difficult problems in mathematics. In this paper, we propose an automated reasoning procedure for deciding the satisfiability of a system of non-linear equations over finite fields. We introduce zero decomposition techniques to prove that polynomial constraints over finite fields yield finite basis explanation functions. We use these explanation functions in model constructing satisfiability solving, allowing us to equip a CDCL-style search procedure with tailored theory reasoning in SMT solving over finite fields. We implemented our approach and provide a novel and effective reasoning prototype for non-linear arithmetic over finite fields.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Non-linear polynomial systems over finite fields are used to model functional behavior of cryptosystems, with applications in system security, computer cryptography, and post- quantum cryptography. Solving polynomial systems is also one of the most difficult problems in mathematics. In this paper, we propose an automated reasoning procedure for deciding the satisfiability of a system of non-linear equations over finite fields. We introduce zero decomposition techniques to prove that polynomial constraints over finite fields yield finite basis explanation functions. We use these explanation functions in model constructing satisfiability solving, allowing us to equip a CDCL-style search procedure with tailored theory reasoning in SMT solving over finite fields. We implemented our approach and provide a novel and effective reasoning prototype for non-linear arithmetic over finite fields. |
Daniela Kaufmann, Armin Biere Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra Journal International Journal on Software Tools for Technology Transfer, 2023. @article{KaufmannBiere-STTT, title = {Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra}, author = {Daniela Kaufmann and Armin Biere}, url = {https://link.springer.com/article/10.1007/s10009-022-00688-6, Article https://www.springer.com/journal/10009, Journal}, year = {2023}, date = {2023-01-11}, journal = {International Journal on Software Tools for Technology Transfer}, abstract = {Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice is still considered to be challenging. One of the currently most successful verification techniques relies on algebraic reasoning. In this article, we present AMulet2, a fully automatic tool for verification of integer multipliers combining SAT solving and computer algebra. Our tool models multipliers given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases. Finally, it uses a polynomial reduction algorithm to verify the correctness of the given circuit. AMulet2 is a re-factorization and improved re-implementation of our previous verification tool AMulet1 and cannot only be used as a stand-alone tool but also serves as a polynomial reasoning framework. We present a novel XOR-based slicing approach and discuss improvements on the data structures including monomial sharing.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice is still considered to be challenging. One of the currently most successful verification techniques relies on algebraic reasoning. In this article, we present AMulet2, a fully automatic tool for verification of integer multipliers combining SAT solving and computer algebra. Our tool models multipliers given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases. Finally, it uses a polynomial reduction algorithm to verify the correctness of the given circuit. AMulet2 is a re-factorization and improved re-implementation of our previous verification tool AMulet1 and cannot only be used as a stand-alone tool but also serves as a polynomial reasoning framework. We present a novel XOR-based slicing approach and discuss improvements on the data structures including monomial sharing. |
2022 |
Hannes Sochor, Flavio Ferrarotti and Daniela Kaufmann Fuzzing-Based Grammar Inference ConferenceBest Paper Award Model and Data Engineering (MEDI), Springer, 2022. @conference{SochorFerrarottiKaufmann-MEDI22, title = { Fuzzing-Based Grammar Inference}, author = {Hannes Sochor and Flavio Ferrarotti and Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2022/11/SochorFerrarottiKaufmann_MEDI22.pdf, Paper https://www.medi22.org/, Conference}, year = {2022}, date = {2022-11-19}, booktitle = {Model and Data Engineering (MEDI)}, pages = {72--86}, publisher = {Springer}, abstract = {In this paper we propose and suggest a novel approach for grammar inference that is based on grammar-based fuzzing. While executing a target program with random inputs, our method identifies the program input language as a human-readable context-free grammar. Our strategy, which integrates machine learning techniques with program analysis of call trees, uses a far smaller set of seed inputs than earlier work. As a further contribution we also combine the processes of grammar inference and grammar-based fuzzing to incorporate random sample information into our inference technique. Our evaluation shows that our technique is effective in practice and that the input languages of tested recursive-descending parser are correctly inferred.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } In this paper we propose and suggest a novel approach for grammar inference that is based on grammar-based fuzzing. While executing a target program with random inputs, our method identifies the program input language as a human-readable context-free grammar. Our strategy, which integrates machine learning techniques with program analysis of call trees, uses a far smaller set of seed inputs than earlier work. As a further contribution we also combine the processes of grammar inference and grammar-based fuzzing to incorporate random sample information into our inference technique. Our evaluation shows that our technique is effective in practice and that the input languages of tested recursive-descending parser are correctly inferred. |
Daniela Kaufmann and Armin Biere Fuzzing and Delta Debugging And-Inverter Graph Verification Tools Conference Tests and Proofs (TAP), EasyChair, 2022. @conference{KaufmannBiere-TAP22, title = {Fuzzing and Delta Debugging And-Inverter Graph Verification Tools}, author = {Daniela Kaufmann and Armin Biere}, url = {https://danielakaufmann.at/wp-content/uploads/2022/07/TAP_Kaufmann.pdf, Paper http://fmv.jku.at/aigfuzzing_artifact/, Experiments https://easychair.org/smart-program/TAP22/, Conference}, year = {2022}, date = {2022-07-05}, booktitle = {Tests and Proofs (TAP), EasyChair}, abstract = {Ensuring correctness of verification tools is equally important as the correctness of the actual problems they try to establish. In this paper we evaluate automated fuzzing and debugging techniques applied to state-of-the-art multiplier verification tools, which take the common gate-level representation of and-inverter graphs as input. With a generation- and mutation-based fuzzing approach our tools are able to uncover major faults in verification tools including crashes as well as inaccurate verification results. Additionally we demonstrate the usefulness of certificates for automated reasoning tools. We further apply delta debugging techniques and show their effectiveness in reducing failure-inducing inputs.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Ensuring correctness of verification tools is equally important as the correctness of the actual problems they try to establish. In this paper we evaluate automated fuzzing and debugging techniques applied to state-of-the-art multiplier verification tools, which take the common gate-level representation of and-inverter graphs as input. With a generation- and mutation-based fuzzing approach our tools are able to uncover major faults in verification tools including crashes as well as inaccurate verification results. Additionally we demonstrate the usefulness of certificates for automated reasoning tools. We further apply delta debugging techniques and show their effectiveness in reducing failure-inducing inputs. |
Daniela Kaufmann Formal verification of multiplier circuits using computer algebra Journal it - Information Technology, 2022. @article{Kaufmann-IT2022, title = {Formal verification of multiplier circuits using computer algebra}, author = {Daniela Kaufmann}, url = {https://www.degruyter.com/document/doi/10.1515/itit-2022-0039/html, Article https://www.degruyter.com/journal/key/itit/html, Journal }, year = {2022}, date = {2022-06-24}, journal = { it - Information Technology}, abstract = {Digital circuits are widely utilized in computers, because they provide models for various digital components and arithmetic operations. Arithmetic circuits are a subclass of digital circuits that are used to execute Boolean algebra. To avoid problems like the infamous Pentium FDIV bug, it is critical to ensure that arithmetic circuits are correct. Formal verification can be used to determine the correctness of a circuit with respect to a certain specification. However, arithmetic circuits, particularly integer multipliers, represent a challenge to current verification methodologies and, in reality, still necessitate a significant amount of manual labor. In my dissertation we examine and develop automated reasoning approaches based on computer algebra, where the word-level specification, modeled as a polynomial, is reduced by a Gröbner basis inferred by the gate-level representation of the circuit. We provide a precise formalization of this reasoning process, which includes soundness and completeness arguments and adds to the mathematical background in this field. On the practical side we present an unique incremental column-wise verification algorithm and preprocessing approaches based on variable elimination that simplify the inferred Gröbner basis. Furthermore, we provide an algebraic proof calculus in this thesis that allows obtaining certificates as a by-product of circuit verification in order to boost confidence in the outcomes of automated reasoning tools. These certificates can be efficiently verified with independent proof checking tools.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Digital circuits are widely utilized in computers, because they provide models for various digital components and arithmetic operations. Arithmetic circuits are a subclass of digital circuits that are used to execute Boolean algebra. To avoid problems like the infamous Pentium FDIV bug, it is critical to ensure that arithmetic circuits are correct. Formal verification can be used to determine the correctness of a circuit with respect to a certain specification. However, arithmetic circuits, particularly integer multipliers, represent a challenge to current verification methodologies and, in reality, still necessitate a significant amount of manual labor. In my dissertation we examine and develop automated reasoning approaches based on computer algebra, where the word-level specification, modeled as a polynomial, is reduced by a Gröbner basis inferred by the gate-level representation of the circuit. We provide a precise formalization of this reasoning process, which includes soundness and completeness arguments and adds to the mathematical background in this field. On the practical side we present an unique incremental column-wise verification algorithm and preprocessing approaches based on variable elimination that simplify the inferred Gröbner basis. Furthermore, we provide an algebraic proof calculus in this thesis that allows obtaining certificates as a by-product of circuit verification in order to boost confidence in the outcomes of automated reasoning tools. These certificates can be efficiently verified with independent proof checking tools. |
Daniela Kaufmann, Paul Beame, Armin Biere, Jakob Nordström Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification Conference In Proc. Design, Automation and Test in Europe (DATE'22), IEEE, 2022. @conference{KaufmannBeamerBiereNordstroem-DATE22, title = {Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification}, author = {Daniela Kaufmann and Paul Beame and Armin Biere and Jakob Nordström}, url = {https://danielakaufmann.at/wp-content/uploads/2022/01/KaufmannBeameBiereNordstrom-DATE22.pdf, Paper http://fmv.jku.at/teluma/, Experiments https://www.date-conference.com/, Conference}, year = {2022}, date = {2022-03-21}, booktitle = {In Proc. Design, Automation and Test in Europe (DATE'22), IEEE}, abstract = {Algebraic reasoning has proven to be one of the most effective approaches for verifying gate-level integer multipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this paper that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Algebraic reasoning has proven to be one of the most effective approaches for verifying gate-level integer multipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this paper that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate. |
Daniela Kaufmann, Mathias Fleury, Armin Biere, Manuel Kauers Formal Methods in System Design, 2022. @article{KaufmannFleuryBiereKauers-FMSD22, title = {Practical Algebraic Calculus and Nullstellensatz with the Checkers Pacheck and Pastèque and Nuss-Checker}, author = {Daniela Kaufmann and Mathias Fleury and Armin Biere and Manuel Kauers}, url = {https://link.springer.com/article/10.1007/s10703-022-00391-x, Article http://fmv.jku.at/lpac/, Experiments}, year = {2022}, date = {2022-03-02}, journal = {Formal Methods in System Design}, abstract = {Automated reasoning techniques based on computer algebra have seen renewed interest in recent years and are for example heavily used in formal verification of arithmetic circuits. However, the verification process might contain errors. Generating and checking proof certificates is important to increase the trust in automated reasoning tools. For algebraic reasoning, two proof systems, Nullstellensatz and polynomial calculus, are available and are well-known in proof complexity. A Nullstellensatz proof captures whether a polynomial can be represented as a linear combination of a given set of polynomials by providing the co-factors of the linear combination. Proofs in polynomial calculus dynamically capture that a polynomial can be derived from a given set of polynomials using algebraic ideal theory. In this article we present the practical algebraic calculus as an instantiation of the polynomial calculus that can be checked efficiently. We further modify the practical algebraic calculus and gain LPAC (practical algebraic calculus + linear combinations) that includes linear combinations. In this way we are not only able to represent both Nullstellensatz and polynomial calculus proofs, but we are also able to blend both proof formats. Furthermore, we introduce extension rules to simulate essential rewriting techniques required in practice. For efficiency we also make use of indices for existing polynomials and include deletion rules too. We demonstrate the different proof formats on the use case of arithmetic circuit verification and discuss how these proofs can be produced as a by-product in formal verification. We present the proof checkers Pacheck, Pastèque, and Nuss-Checker. Pacheck checks proofs in practical algebraic calculus more efficiently than Pastèque, but the latter is formally verified using the proof assistant Isabelle/HOL. The tool Nuss-Checker is used to check proofs in the Nullstellensatz format.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Automated reasoning techniques based on computer algebra have seen renewed interest in recent years and are for example heavily used in formal verification of arithmetic circuits. However, the verification process might contain errors. Generating and checking proof certificates is important to increase the trust in automated reasoning tools. For algebraic reasoning, two proof systems, Nullstellensatz and polynomial calculus, are available and are well-known in proof complexity. A Nullstellensatz proof captures whether a polynomial can be represented as a linear combination of a given set of polynomials by providing the co-factors of the linear combination. Proofs in polynomial calculus dynamically capture that a polynomial can be derived from a given set of polynomials using algebraic ideal theory. In this article we present the practical algebraic calculus as an instantiation of the polynomial calculus that can be checked efficiently. We further modify the practical algebraic calculus and gain LPAC (practical algebraic calculus + linear combinations) that includes linear combinations. In this way we are not only able to represent both Nullstellensatz and polynomial calculus proofs, but we are also able to blend both proof formats. Furthermore, we introduce extension rules to simulate essential rewriting techniques required in practice. For efficiency we also make use of indices for existing polynomials and include deletion rules too. We demonstrate the different proof formats on the use case of arithmetic circuit verification and discuss how these proofs can be produced as a by-product in formal verification. We present the proof checkers Pacheck, Pastèque, and Nuss-Checker. Pacheck checks proofs in practical algebraic calculus more efficiently than Pastèque, but the latter is formally verified using the proof assistant Isabelle/HOL. The tool Nuss-Checker is used to check proofs in the Nullstellensatz format. |
2021 |
Daniela Kaufmann Formale Verifikation von Multiplizierern mit Computeralgebra Technical ReportWorkshop Ausgezeichnete Informatikdissertationen 2020, 2021. @conference{GI-Kaufmann2021, title = {Formale Verifikation von Multiplizierern mit Computeralgebra}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2022/01/GI21_Kaufmann.pdf, Paper}, year = {2021}, date = {2021-09-29}, booktitle = {Ausgezeichnete Informatikdissertationen 2020}, abstract = {Arithmetische Schaltungen werden in Prozessoren zur Implementierung von Boolescher Algebra genutzt. Aufgrund des weitreichenden Einsatzes von Prozessoren ist es äußerst wichtig, die Korrektheit dieser Schaltungen garantieren zu können, um Fehler wie den berühmten Pentium FDIV-Bug zu vermeiden. Mithilfe formaler Verifikation kann festgestellt werden, ob eine Schaltung ihrer gewünschten Spezifikation entspricht. Allerdings stellen arithmetische Schaltungen, insbesondere Integer-Multiplizierer auf Gatterebene, eine Herausforderung für bestehende Verifikationstechniken dar. In dieser Dissertation [Ka20] werden aktuelle Verifikationsmethoden basierend auf Computeralgebra verbessert. Wir zeigen eine rigorose präzise mathematische Formulierung, welche auch die Anwendung der Mathematik in diesem Gebiet erweitert. Außerdem haben wir neue Methoden zur vollautomatischen Verifikation von Integer-Multiplizierern entworfen und implementiert, sowie ein kompaktes Beweisformat entwickelt, um das Ergebnis der Verifikation zertifizieren zu können.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Arithmetische Schaltungen werden in Prozessoren zur Implementierung von Boolescher Algebra genutzt. Aufgrund des weitreichenden Einsatzes von Prozessoren ist es äußerst wichtig, die Korrektheit dieser Schaltungen garantieren zu können, um Fehler wie den berühmten Pentium FDIV-Bug zu vermeiden. Mithilfe formaler Verifikation kann festgestellt werden, ob eine Schaltung ihrer gewünschten Spezifikation entspricht. Allerdings stellen arithmetische Schaltungen, insbesondere Integer-Multiplizierer auf Gatterebene, eine Herausforderung für bestehende Verifikationstechniken dar. In dieser Dissertation [Ka20] werden aktuelle Verifikationsmethoden basierend auf Computeralgebra verbessert. Wir zeigen eine rigorose präzise mathematische Formulierung, welche auch die Anwendung der Mathematik in diesem Gebiet erweitert. Außerdem haben wir neue Methoden zur vollautomatischen Verifikation von Integer-Multiplizierern entworfen und implementiert, sowie ein kompaktes Beweisformat entwickelt, um das Ergebnis der Verifikation zertifizieren zu können. |
Daniela Kaufmann Formal Verification of Integer Multiplier Circuits using Algebraic Reasoning: A Survey WorkshopKeynoteInvited In Recent Findings in Boolean Techniques - Selected Papers from the 14th Intl. Workshop on Boolean Problems (IWSBP), 2021. @conference{Kaufmann-IWSBP20, title = {Formal Verification of Integer Multiplier Circuits using Algebraic Reasoning: A Survey}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2021/01/Kaufmann-IWSBP20.pdf, Paper http://www.informatik.uni-bremen.de/iwsbp/, Workshop}, year = {2021}, date = {2021-04-24}, booktitle = {In Recent Findings in Boolean Techniques - Selected Papers from the 14th Intl. Workshop on Boolean Problems (IWSBP)}, abstract = {Digital circuits are extensively used in computers and digital systems and it is of high importance to guarantee that these circuits are correct in order to prevent issues like the famous Pentium FDIV bug. Formal verification can be used to derive the correctness of a given circuit with respect to a certain specification. However arithmetic circuits, and most prominently multipliers, impose a challenge for existing verification techniques. Currently one of the most effective techniques is based on algebraic reasoning. In this approach the circuit is modeled as a set of pseudo-Boolean polynomials and the word-level specification is reduced by a Gröbner basis, which is implied by the polynomial representation of the circuit. The circuit is correct if and only if the final result is zero. Nonetheless the verification process might not be error-free. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. In this paper we survey the current state of the art of this work. We give an overview over recent solving techniques, available benchmarks, and include a comprehensive evaluation.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Digital circuits are extensively used in computers and digital systems and it is of high importance to guarantee that these circuits are correct in order to prevent issues like the famous Pentium FDIV bug. Formal verification can be used to derive the correctness of a given circuit with respect to a certain specification. However arithmetic circuits, and most prominently multipliers, impose a challenge for existing verification techniques. Currently one of the most effective techniques is based on algebraic reasoning. In this approach the circuit is modeled as a set of pseudo-Boolean polynomials and the word-level specification is reduced by a Gröbner basis, which is implied by the polynomial representation of the circuit. The circuit is correct if and only if the final result is zero. Nonetheless the verification process might not be error-free. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. In this paper we survey the current state of the art of this work. We give an overview over recent solving techniques, available benchmarks, and include a comprehensive evaluation. |
Daniela Kaufmann, Armin Biere AMulet 2.0 for Verifying Multiplier Circuits Conference In Proc. 27th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2021. @conference{KAufmannBiere-TACAS21, title = {AMulet 2.0 for Verifying Multiplier Circuits}, author = {Daniela Kaufmann and Armin Biere}, url = {https://danielakaufmann.at/wp-content/uploads/2021/01/KaufmannBiere-TACAS21.pdf, Paper http://fmv.jku.at/amulet2_artifact/, Artifact https://etaps.org/2021/tacas, Conference}, year = {2021}, date = {2021-01-08}, booktitle = {In Proc. 27th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, abstract = {AMulet 2.0 is a fully automatic tool for the verification of integer multipliers using computer algebra. Our tool models multiplier circuits given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases. Finally it uses a polynomial reduction algorithm to verify the correctness of the given circuit. AMulet 2.0 is a re-factorization and improved re-implementation of our previous multiplier verification tool AMulet 1.0.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } AMulet 2.0 is a fully automatic tool for the verification of integer multipliers using computer algebra. Our tool models multiplier circuits given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases. Finally it uses a polynomial reduction algorithm to verify the correctness of the given circuit. AMulet 2.0 is a re-factorization and improved re-implementation of our previous multiplier verification tool AMulet 1.0. |
2020 |
Daniela Kaufmann, Mathias Fleury, Armin Biere The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus Conference In Proc. 20th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'20), 2020. @conference{KaufmannFleuryBiere-FMCAD20, title = {The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus}, author = {Daniela Kaufmann and Mathias Fleury and Armin Biere}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/KaufmannFleuryBiere-FMCAD20.pdf, Paper http://fmv.jku.at/pacheck_pasteque/, Experiments https://fmcad.forsyte.at/FMCAD20/, Conference}, year = {2020}, date = {2020-11-02}, booktitle = {In Proc. 20th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'20)}, abstract = {Generating and checking proof certificates is important to increase the trust in automated reasoning tools. In recent years formal verification using computer algebra became more important and is heavily used in automated circuit verification. An existing proof format which covers algebraic reasoning and allows efficient proof checking is the practical algebraic calculus. In this paper we present two independent proof checkers Pacheck and Pastèque. The checker Pacheck checks algebraic proofs more efficiently than Pastèque, but the latter is formally verified using the proof assistant Isabelle/HOL. Furthermore, we introduce extension rules to simulate essential rewriting techniques required in practice. For efficiency we also make use of indices for existing polynomials and include deletion rules too.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Generating and checking proof certificates is important to increase the trust in automated reasoning tools. In recent years formal verification using computer algebra became more important and is heavily used in automated circuit verification. An existing proof format which covers algebraic reasoning and allows efficient proof checking is the practical algebraic calculus. In this paper we present two independent proof checkers Pacheck and Pastèque. The checker Pacheck checks algebraic proofs more efficiently than Pastèque, but the latter is formally verified using the proof assistant Isabelle/HOL. Furthermore, we introduce extension rules to simulate essential rewriting techniques required in practice. For efficiency we also make use of indices for existing polynomials and include deletion rules too. |
Mathias Fleury, Daniela Kaufmann Practical Algebraic Calculus Checker Technical Report Archive of Formal Proofs, 2020. @conference{FleuryKaufmann-AFP20, title = {Practical Algebraic Calculus Checker}, author = {Mathias Fleury, Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2021/01/FleuryKaufmann-AFP.pdf, Document https://www.isa-afp.org/entries/PAC_Checker.html, Archive of Formal Proofs}, year = {2020}, date = {2020-10-01}, booktitle = {Archive of Formal Proofs}, abstract = {Generating and checking proof certificates is important to increase the trust in automated reasoning tools. In recent years formal verification using computer algebra became more important and is heavily used in automated circuit verification. An existing proof format which covers algebraic reasoning and allows efficient proof checking is the practical algebraic calculus. In this development, we present the verified checker Pastèque that is obtained by synthesis via the Refinement Framework. This is the formalization going with our FMCAD’20 tool presentation}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Generating and checking proof certificates is important to increase the trust in automated reasoning tools. In recent years formal verification using computer algebra became more important and is heavily used in automated circuit verification. An existing proof format which covers algebraic reasoning and allows efficient proof checking is the practical algebraic calculus. In this development, we present the verified checker Pastèque that is obtained by synthesis via the Refinement Framework. This is the formalization going with our FMCAD’20 tool presentation |
Daniela Kaufmann, Armin Biere Nullstellensatz-Proofs for Multiplier Verification Conference In Proc. Computer Algebra in Scientific Computing (CASC'20), vol. 12291 , LNCS Springer, 2020. @conference{KaufmannBiere-CASC20, title = {Nullstellensatz-Proofs for Multiplier Verification}, author = {Daniela Kaufmann and Armin Biere}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/KaufmannBiere-CASC20.pdf, Paper http://fmv.jku.at/nussproofs/, Experiments http://www.casc-conference.org/2020/index.html, Conference}, year = {2020}, date = {2020-08-05}, booktitle = {In Proc. Computer Algebra in Scientific Computing (CASC'20)}, volume = {vol. 12291}, pages = {368--389}, publisher = {Springer}, series = {LNCS}, abstract = {Automated reasoning techniques based on computer algebra are an essential ingredient in formal verification of gate-level multiplier circuits. Generating and independently checking proof certificates helps to validate the verification results. Two algebraic proof systems, Nullstellensatz and polynomial calculus, are well-known in proof complexity. The practical application of the polynomial calculus has been studied recently. However, producing and checking Nullstellensatz certificates for multiplier verification has not been considered so far. In this paper we show how Nullstellensatz proofs can be generated as a by-product of multiplier verification and present our Nullstellensatz proof checker Nuss-Checker. Additionally, we prove quadratic upper bounds on the proof size for simple array multipliers.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Automated reasoning techniques based on computer algebra are an essential ingredient in formal verification of gate-level multiplier circuits. Generating and independently checking proof certificates helps to validate the verification results. Two algebraic proof systems, Nullstellensatz and polynomial calculus, are well-known in proof complexity. The practical application of the polynomial calculus has been studied recently. However, producing and checking Nullstellensatz certificates for multiplier verification has not been considered so far. In this paper we show how Nullstellensatz proofs can be generated as a by-product of multiplier verification and present our Nullstellensatz proof checker Nuss-Checker. Additionally, we prove quadratic upper bounds on the proof size for simple array multipliers. |
Daniela Kaufmann Formal Verification of Multiplier Circuits using Computer Algebra PhD Thesis Johannes Kepler University, 2020. @phdthesis{Kaufmann-PhdThesis20, title = {Formal Verification of Multiplier Circuits using Computer Algebra}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-PhD-Thesis-2020.pdf, Thesis}, year = {2020}, date = {2020-06-03}, address = {Linz, Austria}, school = {Johannes Kepler University}, abstract = {Digital circuits are extensively used in computers and digital systems because they are able to represent models for various digital components and arithmetic operations. A subclass of digital circuits are arithmetic circuits, which are used in computer circuits to perform Boolean algebra. It is of high importance to guarantee that these circuits are correct in order to prevent issues like the famous Pentium FDIV bug. Formal verification can be used to derive the correctness of a given circuit with respect to a certain specification. However, arithmetic circuits, and most prominently gate-level multipliers, impose a challenge for existing verification techniques and in practice still require substantial manual effort. Approaches based on satisfiability checking (SAT) or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. In principle, theorem provers in combination with SAT are able to verify industrial multipliers, but this approach cannot be applied fully automated. Currently, the most effective automated reasoning technique relies on computer algebra. In this approach the word-level specification, modeled as a polynomial, is reduced by a Gröbner basis, which is implied by the gate-level representation of the circuit. The reduction returns zero if and only if the circuit is correct. In this thesis we give a rigorous formalization of this reasoning method including soundness and completeness arguments, first for polynomial rings, where the coefficient domain is a field and later for more general polynomial rings. As a consequence we are able to verify not only large unsigned and signed integer multipliers very efficiently, but are also able to verify truncated multipliers. We further improve the algebraic verification approach and present a new incremental column-wise verification algorithm, which splits the verification problem into smaller more manageable sub-problems and thus does not require to consider a full word-level specification. We present preprocessing approaches based on variable elimination in order to rewrite and hence simplify the implied Gröbner basis. However, certain parts of a multiplier, namely final-stage adders, are hard to verify using computer algebra. In our approach we use SAT to replace complex adders by equivalent adders, which can be verified using computer algebra. We develop a dedicated reduction engine, which is able to apply adder substitution and verifies large multipliers of input bit-width 2048 fully automated. Nonetheless, the verification process might not be error-free. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. We show how the polynomial calculus can be instantiated to yield a practical algebraic calculus (PAC). Proofs in this format can be obtained as a by-product of verifying multiplier circuits in our reduction engine and can be checked with our independent proof checking tools.}, keywords = {}, pubstate = {published}, tppubtype = {phdthesis} } Digital circuits are extensively used in computers and digital systems because they are able to represent models for various digital components and arithmetic operations. A subclass of digital circuits are arithmetic circuits, which are used in computer circuits to perform Boolean algebra. It is of high importance to guarantee that these circuits are correct in order to prevent issues like the famous Pentium FDIV bug. Formal verification can be used to derive the correctness of a given circuit with respect to a certain specification. However, arithmetic circuits, and most prominently gate-level multipliers, impose a challenge for existing verification techniques and in practice still require substantial manual effort. Approaches based on satisfiability checking (SAT) or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. In principle, theorem provers in combination with SAT are able to verify industrial multipliers, but this approach cannot be applied fully automated. Currently, the most effective automated reasoning technique relies on computer algebra. In this approach the word-level specification, modeled as a polynomial, is reduced by a Gröbner basis, which is implied by the gate-level representation of the circuit. The reduction returns zero if and only if the circuit is correct. In this thesis we give a rigorous formalization of this reasoning method including soundness and completeness arguments, first for polynomial rings, where the coefficient domain is a field and later for more general polynomial rings. As a consequence we are able to verify not only large unsigned and signed integer multipliers very efficiently, but are also able to verify truncated multipliers. We further improve the algebraic verification approach and present a new incremental column-wise verification algorithm, which splits the verification problem into smaller more manageable sub-problems and thus does not require to consider a full word-level specification. We present preprocessing approaches based on variable elimination in order to rewrite and hence simplify the implied Gröbner basis. However, certain parts of a multiplier, namely final-stage adders, are hard to verify using computer algebra. In our approach we use SAT to replace complex adders by equivalent adders, which can be verified using computer algebra. We develop a dedicated reduction engine, which is able to apply adder substitution and verifies large multipliers of input bit-width 2048 fully automated. Nonetheless, the verification process might not be error-free. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. We show how the polynomial calculus can be instantiated to yield a practical algebraic calculus (PAC). Proofs in this format can be obtained as a by-product of verifying multiplier circuits in our reduction engine and can be checked with our independent proof checking tools. |
Daniela Kaufmann, Armin Biere, Manuel Kauers From DRUP to PAC and Back Conference In Proc. Design, Automation and Test in Europe (DATE'20), IEEE, 2020. @conference{KaufmannBiereKauers-DATE20, title = {From DRUP to PAC and Back}, author = {Daniela Kaufmann and Armin Biere and Manuel Kauers}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/KaufmannBiereKauers-DATE20.pdf, Paper http://fmv.jku.at/drup2pac/, Experiments https://www.date-conference.com/, Conference}, year = {2020}, date = {2020-06-01}, booktitle = {In Proc. Design, Automation and Test in Europe (DATE'20)}, pages = {654--657}, publisher = {IEEE}, abstract = {Currently the most efficient automatic approach to verify gate-level multipliers combines SAT solving and computer algebra. In order to increase confidence in the verification, proof certificates are generated. However, due to different solving techniques, these certificates require two different proof formats, namely DRUP and PAC. A combined proof has so far been missing. Correctness of this approach can thus only be trusted up to the correctness of compositional reasoning. In this paper we show how to generate a single proof in one proof format, which then allows to certify correctness using one simple proof checker. We further investigate empirically the effect on proof generation and checking time as well as on proof size. It turns out that PAC proofs are much more compact and faster to check.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Currently the most efficient automatic approach to verify gate-level multipliers combines SAT solving and computer algebra. In order to increase confidence in the verification, proof certificates are generated. However, due to different solving techniques, these certificates require two different proof formats, namely DRUP and PAC. A combined proof has so far been missing. Correctness of this approach can thus only be trusted up to the correctness of compositional reasoning. In this paper we show how to generate a single proof in one proof format, which then allows to certify correctness using one simple proof checker. We further investigate empirically the effect on proof generation and checking time as well as on proof size. It turns out that PAC proofs are much more compact and faster to check. |
Daniela Kaufmann Verifying Multipliers using Computer Algebra Student Forum PhD Forum of Design, Automation and Test in Europe (DATE'20), 2020. @misc{Kaufmann-SFDATE20, title = {Verifying Multipliers using Computer Algebra}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/paper-1.pdf, Paper https://www.date-conference.com/, Conference}, year = {2020}, date = {2020-03-03}, abstract = {Formal verification is used to guarantee the correctness of a given circuit with respect to a certain specification. However arithmetic circuits, and most prominently gate-level multipliers, impose a challenge for existing verification techniques and in practice still require substantial manual effort. The focus of this thesis is to improve automated formal verification of multiplier circuits using computer algebra to make it practically applicable for non-trivial and optimized multiplier designs. In the thesis a rigorous formalization of the problem is given and several optimization techniques are developed which make automated verification an order of magnitude faster than related approaches. As a further contribution a dedicated reduction engine is developed which in addition allows to generate proof certificates, validating the result of the verification approach.}, howpublished = {PhD Forum of Design, Automation and Test in Europe (DATE'20)}, keywords = {}, pubstate = {published}, tppubtype = {misc} } Formal verification is used to guarantee the correctness of a given circuit with respect to a certain specification. However arithmetic circuits, and most prominently gate-level multipliers, impose a challenge for existing verification techniques and in practice still require substantial manual effort. The focus of this thesis is to improve automated formal verification of multiplier circuits using computer algebra to make it practically applicable for non-trivial and optimized multiplier designs. In the thesis a rigorous formalization of the problem is given and several optimization techniques are developed which make automated verification an order of magnitude faster than related approaches. As a further contribution a dedicated reduction engine is developed which in addition allows to generate proof certificates, validating the result of the verification approach. |
Daniela Kaufmann, Manuel Kauers, Armin Biere SAT, Computer Algebra, Multipliers WorkshopInvited In Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops, EasyChair, 2020. @conference{KaufmannBiereKauers-Vampire19, title = {SAT, Computer Algebra, Multipliers}, author = {Daniela Kaufmann and Manuel Kauers and Armin Biere}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/KaufmannBiereKauers-Vampire19.pdf, Paper https://easychair.org/smart-program/Vampire2019/index.html, Workshop}, year = {2020}, date = {2020-02-04}, booktitle = {In Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops}, pages = {1--18}, publisher = {EasyChair}, abstract = {Verifying multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning. However parts of a multiplier, i.e., complex final stage adders are hard to verify using computer algebra. In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers. In this paper we focus on the implementation details of our new dedicated reduction engine, which not only allows fully automated adder substitution, but also employs polynomial reduction efficiently. Our tool is furthermore able to generate proof certificates in the practical algebraic calculus and we also investigate the size of these proofs for one specific multiplier architecture.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Verifying multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning. However parts of a multiplier, i.e., complex final stage adders are hard to verify using computer algebra. In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers. In this paper we focus on the implementation details of our new dedicated reduction engine, which not only allows fully automated adder substitution, but also employs polynomial reduction efficiently. Our tool is furthermore able to generate proof certificates in the practical algebraic calculus and we also investigate the size of these proofs for one specific multiplier architecture. |
Daniela Kaufmann, Armin Biere, Manuel Kauers Incremental Column-Wise Verification of Arithmetic Circuits Using Computer Algebra Journal Formal Methods in System Design, 2020. @article{KaufmannBiereKauers-FMSD19, title = {Incremental Column-Wise Verification of Arithmetic Circuits Using Computer Algebra}, author = {Daniela Kaufmann and Armin Biere and Manuel Kauers}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/KaufmannBiereKauers-FMSD19.pdf, Article http://fmv.jku.at/fmsd18/, Experiments https://link.springer.com/article/10.1007/s10703-018-00329-2, Journal}, year = {2020}, date = {2020-01-01}, journal = {Formal Methods in System Design}, publisher = {Springer}, abstract = {Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is reduced by a Gröbner basis which is implied by the gate-level representation of the circuit. This reduction returns zero if and only if the circuit is correct. We give a rigorous formalization of this approach including soundness and completeness arguments. Furthermore we present a novel incremental column-wise technique to verify gate-level multipliers. This approach is further improved by extracting full- and half-adder constraints in the circuit which allows to rewrite and reduce the Gröbner basis. We also present a new technical theorem which allows to rewrite local parts of the Gröbner basis. Optimizing the Gröbner basis reduces computation time substantially. In addition we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification. Our experiments show that regular multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. We discuss in detail our complete verification approach including all optimizations.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is reduced by a Gröbner basis which is implied by the gate-level representation of the circuit. This reduction returns zero if and only if the circuit is correct. We give a rigorous formalization of this approach including soundness and completeness arguments. Furthermore we present a novel incremental column-wise technique to verify gate-level multipliers. This approach is further improved by extracting full- and half-adder constraints in the circuit which allows to rewrite and reduce the Gröbner basis. We also present a new technical theorem which allows to rewrite local parts of the Gröbner basis. Optimizing the Gröbner basis reduces computation time substantially. In addition we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification. Our experiments show that regular multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. We discuss in detail our complete verification approach including all optimizations. |
2019 |
Daniela Kaufmann Influence of the Reduction Order in Multiplier Verification using Computer Algebra Student Forum Student Forum of 19th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19), 2019. @misc{Kaufmann-SFFMCAD19, title = {Influence of the Reduction Order in Multiplier Verification using Computer Algebra}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/paper.pdf, Paper https://fmcad.forsyte.at/FMCAD19/, Conference}, year = {2019}, date = {2019-11-21}, abstract = {Currently the most promising approach for automatically verifying multiplier circuits relies on computer algebra. In this approach the circuit as well as its specification are modeled as polynomials and a polynomial reduction algorithm is applied to show correctness. We want to elaborate on the influence of the reduction order by employing a wide range of valid orderings. In our experiments we measure and compare the size of the intermediate reduction results and gain a clear preference towards a column-wise ordering.}, howpublished = {Student Forum of 19th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19)}, keywords = {}, pubstate = {published}, tppubtype = {misc} } Currently the most promising approach for automatically verifying multiplier circuits relies on computer algebra. In this approach the circuit as well as its specification are modeled as polynomials and a polynomial reduction algorithm is applied to show correctness. We want to elaborate on the influence of the reduction order by employing a wide range of valid orderings. In our experiments we measure and compare the size of the intermediate reduction results and gain a clear preference towards a column-wise ordering. |
Daniela Kaufmann, Armin Biere, Manuel Kauers Verifying Large Multipliers by Combining SAT and Computer Algebra Conference In Proc. 19th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19), IEEE, 2019. @conference{KaufmannBiereKauers-FMCAD19, title = {Verifying Large Multipliers by Combining SAT and Computer Algebra}, author = {Daniela Kaufmann and Armin Biere and Manuel Kauers}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/KaufmannBiereKauers-FMCAD19.pdf, Paper http://fmv.jku.at/amulet/, Experiments https://fmcad.forsyte.at/FMCAD19/, Conference}, year = {2019}, date = {2019-11-15}, booktitle = {In Proc. 19th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19)}, pages = {28--36}, publisher = {IEEE}, abstract = {We combine SAT and computer algebra to substantially improve the most effective approach for automatically verifying integer multipliers. In our approach complex final stage adders are detected and replaced by simple adders. These simplified multipliers are verified by computer algebra techniques and correctness of the replacement step by SAT solvers. Our new dedicated reduction engine relies on a Gröbner basis theory for coefficient rings which in contrast to previous work no longer are required to be fields. Modular reasoning allows us to verify not only large unsigned and signed multipliers much more efficiently but also truncated multipliers. We are further able to generate and check proofs an order of magnitude faster than in our previous work, relative to verification time, while other competing approaches do not provide certificates.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } We combine SAT and computer algebra to substantially improve the most effective approach for automatically verifying integer multipliers. In our approach complex final stage adders are detected and replaced by simple adders. These simplified multipliers are verified by computer algebra techniques and correctness of the replacement step by SAT solvers. Our new dedicated reduction engine relies on a Gröbner basis theory for coefficient rings which in contrast to previous work no longer are required to be fields. Modular reasoning allows us to verify not only large unsigned and signed multipliers much more efficiently but also truncated multipliers. We are further able to generate and check proofs an order of magnitude faster than in our previous work, relative to verification time, while other competing approaches do not provide certificates. |
Daniela Kaufmann, Manuel Kauers, Armin Biere, David Cok Arithmetic Verification Problems Submitted to the SAT Race 2019 Technical Report In Proc. of SAT Race 2019 - Solver and Benchmark Descriptions, B-2019-1 , Department of Computer Science Series of Publications B, 2019. @conference{KaufmannKauersBiereCok-SATRACE19, title = {Arithmetic Verification Problems Submitted to the SAT Race 2019}, author = {Daniela Kaufmann and Manuel Kauers and Armin Biere and David Cok}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/KaufmannKauersBiereCok-SAT-Race-2019-benchmarks.pdf, Paper http://sat-race-2019.ciirc.cvut.cz/, SAT Race}, year = {2019}, date = {2019-07-31}, booktitle = {In Proc. of SAT Race 2019 - Solver and Benchmark Descriptions}, volume = {B-2019-1}, pages = {49}, publisher = {Department of Computer Science Series of Publications B}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
2018 |
Daniela Ritirc (*), Armin Biere, Manuel Kauers A Practical Polynomial Calculus for Arithmetic Circuit Verification Workshop In Proc. 3rd Intl. Workshop on Satisfiability Checking and Symbolic Computation (SC2'18), CEUR-WS, 2018. @conference{RitircBiereKauers-SC218, title = {A Practical Polynomial Calculus for Arithmetic Circuit Verification}, author = {Daniela Ritirc (*) and Armin Biere and Manuel Kauers }, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/RitircBiereKauers-scsc18.pdf, Paper http://fmv.jku.at/pac/, Experiments http://www.sc-square.org/CSA/workshop3.html, Workshop}, year = {2018}, date = {2018-08-20}, booktitle = {In Proc. 3rd Intl. Workshop on Satisfiability Checking and Symbolic Computation (SC2'18)}, pages = {61--76}, publisher = {CEUR-WS}, abstract = {Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. The use of computer algebra is an essential ingredient in recent substantial improvements to scale verification of arithmetic gate-level circuits, such as multipliers, to large bit-widths. There is also a large body of work on theoretical aspects of propositional algebraic proof systems in the proof complexity community starting with the seminal paper introducing the polynomial calculus. We show that the polynomial calculus provides a frame-work to define a practical algebraic calculus (PAC) proof format to capture low-level algebraic proofs needed in scalable gate-level verification of arithmetic circuits. We apply these techniques to generate proofs obtained as by-product of verifying gate-level multipliers using state-of-the-art techniques. Our experiments show that these proofs can be checked efficiently with independent tools.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. The use of computer algebra is an essential ingredient in recent substantial improvements to scale verification of arithmetic gate-level circuits, such as multipliers, to large bit-widths. There is also a large body of work on theoretical aspects of propositional algebraic proof systems in the proof complexity community starting with the seminal paper introducing the polynomial calculus. We show that the polynomial calculus provides a frame-work to define a practical algebraic calculus (PAC) proof format to capture low-level algebraic proofs needed in scalable gate-level verification of arithmetic circuits. We apply these techniques to generate proofs obtained as by-product of verifying gate-level multipliers using state-of-the-art techniques. Our experiments show that these proofs can be checked efficiently with independent tools. |
Daniela Ritirc (*), Armin Biere, Manuel Kauers Improving and Extending the Algebraic Approach for Verifying Gate-Level Multipliers Conference In Proc. Design, Automation and Test in Europe (DATE'18), IEEE, 2018. @conference{RitircBiereKauers-DATE18, title = {Improving and Extending the Algebraic Approach for Verifying Gate-Level Multipliers}, author = {Daniela Ritirc (*) and Armin Biere and Manuel Kauers }, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/RitircBiereKauers-DATE18.pdf, Paper http://fmv.jku.at/algeq/, Experiments https://www.date-conference.com/, Conference}, year = {2018}, date = {2018-03-15}, booktitle = {In Proc. Design, Automation and Test in Europe (DATE'18)}, pages = {1556--1561}, publisher = {IEEE}, abstract = {The currently most effective approach for verifying gate-level multipliers uses Computer Algebra. It reduces a word-level multiplier specification by a Gröbner basis derived from a gate-level implementation. This reduction produces zero if and only if the circuit is a multiplier. We improve this approach by extracting full- and half-adder constraints to reduce the Gröbner basis, which speeds up computation substantially. Refactoring the specification in terms of partial products instead of inputs yields further improvements. As a third contribution we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } The currently most effective approach for verifying gate-level multipliers uses Computer Algebra. It reduces a word-level multiplier specification by a Gröbner basis derived from a gate-level implementation. This reduction produces zero if and only if the circuit is a multiplier. We improve this approach by extracting full- and half-adder constraints to reduce the Gröbner basis, which speeds up computation substantially. Refactoring the specification in terms of partial products instead of inputs yields further improvements. As a third contribution we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification. |
2017 |
Armin Biere, Manuel Kauers, Daniela Ritirc (*) Challenges in Verifying Arithmetic Circuits Using Computer Algebra ConferenceInvited In Proc. 19th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'17), IEEE, 2017. @conference{BiereKauersRitirc-SYNASC17, title = {Challenges in Verifying Arithmetic Circuits Using Computer Algebra}, author = {Armin Biere and Manuel Kauers and Daniela Ritirc (*)}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/BiereKauersRitirc-SYNASC17.pdf, Paper https://synasc.ro/2017/, Conference}, year = {2017}, date = {2017-12-31}, booktitle = {In Proc. 19th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'17)}, pages = {9--16}, publisher = {IEEE}, abstract = {Verifying arithmetic circuits is an important problem which still requires considerable manual effort. For instance multipliers are considered difficult to verify. The currently most effective approach for arithmetic circuit verification uses computer algebra. In this approach the circuit is modeled as a set of pseudo-boolean polynomials and it is checked if the given word-level specification is implied by the circuit polynomials. For this purpose the theory of Gröbner bases is used. In this paper we give a summary of two recent papers on this work. We reword the theory and illustrate the results of these papers by examples. We also present a new technical theorem which allows to rewrite local parts of the Gröbner basis. Rewriting the Gröbner basis has tremendous effect on computation time.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Verifying arithmetic circuits is an important problem which still requires considerable manual effort. For instance multipliers are considered difficult to verify. The currently most effective approach for arithmetic circuit verification uses computer algebra. In this approach the circuit is modeled as a set of pseudo-boolean polynomials and it is checked if the given word-level specification is implied by the circuit polynomials. For this purpose the theory of Gröbner bases is used. In this paper we give a summary of two recent papers on this work. We reword the theory and illustrate the results of these papers by examples. We also present a new technical theorem which allows to rewrite local parts of the Gröbner basis. Rewriting the Gröbner basis has tremendous effect on computation time. |
Daniela Ritirc (*), Armin Biere, Manuel Kauers Column-Wise Verification of Mulitpliers Using Computer Algebra ConferenceBest Paper Award In Proc. 17th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17), IEEE, 2017. @conference{RitircBiereKauers-FMCAD17, title = {Column-Wise Verification of Mulitpliers Using Computer Algebra}, author = {Daniela Ritirc (*) and Armin Biere and Manuel Kauers}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/RitircBiereKauers-FMCAD17.pdf, Paper http://fmv.jku.at/cwmulverca/index.html, Experiments https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD17/, Conference}, year = {2017}, date = {2017-09-20}, booktitle = {In Proc. 17th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17)}, journal = {Proc. 17th Intl. Conf. on Formal Methods in Computer Aided Design}, pages = {23--30}, publisher = {IEEE}, abstract = {Verifying arithmetic circuits, and most prominently multipliers, is an important problem but in practice still requires substantial manual effort. Recent work tries to solve this issue using techniques from computer algebra. The most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this paper we give a rigorous formalization of this approach and present a new column-wise verification technique for the correctness of gate-level multipliers which does not require the reduction of a full word-level specification. We formally prove soundness and completeness of our technique, making use of our precise formalization. Our experiments show that simple multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. Further, our paper independently confirms the effectiveness of previous related work. We make all benchmarks and tools publicly available.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Verifying arithmetic circuits, and most prominently multipliers, is an important problem but in practice still requires substantial manual effort. Recent work tries to solve this issue using techniques from computer algebra. The most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this paper we give a rigorous formalization of this approach and present a new column-wise verification technique for the correctness of gate-level multipliers which does not require the reduction of a full word-level specification. We formally prove soundness and completeness of our technique, making use of our precise formalization. Our experiments show that simple multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. Further, our paper independently confirms the effectiveness of previous related work. We make all benchmarks and tools publicly available. |
(*) Before 10/2018 I published using my maiden name ‘Ritirc’.