2023 |
Daniela Kaufmann Lifespan of SAT Techniques Workshop Pragmatics of SAT, Italy, 2023. @conference{Kaufmann-POS23, title = {Lifespan of SAT Techniques}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2023/07/talk.pdf, Slides http://www.pragmaticsofsat.org/2023/, Workshop}, year = {2023}, date = {2023-07-04}, booktitle = {Pragmatics of SAT, Italy}, 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. |
Daniela Kaufmann Combining SAT and Computer Algebra for Circuit Verification WorkshopInvited Dagstuhl Seminar: SAT Encodings and Beyond, 2023. @conference{Kaufmann-Dagstuhl23, title = {Combining SAT and Computer Algebra for Circuit Verification}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2023/07/talk-1.pdf, Slides https://www.dagstuhl.de/en/seminars/seminar-calendar/seminar-details/23261, Workshop}, year = {2023}, date = {2023-06-27}, booktitle = {Dagstuhl Seminar: SAT Encodings and Beyond}, abstract = {Verifying multiplier circuits is an important problem which in practice still requires substantial manual effort. In this talk, I will demonstrate that encoding the entire problem into SAT is not the ideal strategy, nor is using a pure algebraic encoding. We use a combination of SAT and computer algebra in our method to significantly improve automated verification of integer multipliers.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Verifying multiplier circuits is an important problem which in practice still requires substantial manual effort. In this talk, I will demonstrate that encoding the entire problem into SAT is not the ideal strategy, nor is using a pure algebraic encoding. We use a combination of SAT and computer algebra in our method to significantly improve automated verification of integer multipliers. |
Daniela Kaufmann MCSat Based Approaches for Non-linear Modular Arithmetic WorkshopInvited Satisfiability: Theory, Practice, and Beyond Simons Institute, Berkeley, CA, US, 2023. @conference{Kaufmann-Berkeley23, title = {MCSat Based Approaches for Non-linear Modular Arithmetic}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2023/04/Kaufmann_Berkeley23.pdf, Slides https://simons.berkeley.edu/talks/daniela-kaufmann-tu-wien-2023-04-20, Video https://simons.berkeley.edu/workshops/satisfiability-theory-practice-beyond, Workshop}, year = {2023}, date = {2023-04-20}, booktitle = {Satisfiability: Theory, Practice, and Beyond Simons Institute, Berkeley, CA, US}, abstract = {Solving a system of polynomial equations is one of the hardest problems in mathematics, with emerging applications in cryptography, software security, and code optimizations. Modern cryptosystems, such as smart contracts, require reasoning techniques over non-linear polynomial systems in finite domains. In this talk we present two MCSat based approaches that address this problem for the use cases of bit-vector reasoning and reasoning over finite fields. We introduce PolySAT, a new bitvector solver that, instead of bit-blasting, performs reasoning on the word level. Constraints in PolySAT are based on polynomials over bitvector variables, i.e., modulo 2^k. PolySAT is being implemented as a theory solver in the SMT solver Z3. Secondly we present our work on solving non-linear polynomial systems over finite fields. We have designed a MCSat style search procedure with two different approaches for explanation functions that rely on algebraic variable elimination techniques.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Solving a system of polynomial equations is one of the hardest problems in mathematics, with emerging applications in cryptography, software security, and code optimizations. Modern cryptosystems, such as smart contracts, require reasoning techniques over non-linear polynomial systems in finite domains. In this talk we present two MCSat based approaches that address this problem for the use cases of bit-vector reasoning and reasoning over finite fields. We introduce PolySAT, a new bitvector solver that, instead of bit-blasting, performs reasoning on the word level. Constraints in PolySAT are based on polynomials over bitvector variables, i.e., modulo 2^k. PolySAT is being implemented as a theory solver in the SMT solver Z3. Secondly we present our work on solving non-linear polynomial systems over finite fields. We have designed a MCSat style search procedure with two different approaches for explanation functions that rely on algebraic variable elimination techniques. |
2022 |
Daniela Kaufmann Exploring Algebraic Methods for Circuit Verification WorkshopInvited Dagstuhl Seminar: Theory and Practice of SAT and Combinatorial Solving, Schloss Dagstuhl, Germany, 2022. @conference{Kaufmann-Dagstuhl22b, title = {Exploring Algebraic Methods for Circuit Verification}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2022/10/Kaufmann-Dagstuhl22.pdf, Slides https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=22411, Dagstuhl Seminar}, year = {2022}, date = {2022-10-10}, booktitle = {Dagstuhl Seminar: Theory and Practice of SAT and Combinatorial Solving, Schloss Dagstuhl, Germany}, abstract = {Digital circuits are widely utilized in computers, because they provide models for various digital components and arithmetic operations. To avoid problems like the infamous Pentium FDIV bug, it is critical to ensure that these circuits are correct. Formal verification can be used to evaluate whether a circuit meets a given specification. Arithmetic circuits, in particular integer multipliers, pose a challenge to current verification approaches. Techniques that rely solely on SAT solving or decision diagrams appear incapable of tackling this problem in an acceptable period of time. In practice, circuit verification still requires a substantial amount of manual labor. In this talk, we will demonstrate an automated verification technique that is based on algebraic reasoning and is currently considered to be one of the most successful verification methods for circuit verification. In this approach the circuit is modeled as a set of polynomial equations that is implied by the circuit. For a correct circuit, we must demonstrate that the specification is implied by the polynomial representation of the given circuit. However, some sections of the multiplier, such as final stage adders, are difficult to check using simply computer algebra. To address this issue, we will provide a hybrid solution that blends SAT and computer algebra. But who verifies the verifier? The ability to independently generate and check proof certificates boosts confidence in the outcomes of automated reasoning tools. We present an algebraic proof calculus that allows us to obtain certificates as a by-product of circuit verification and that can be efficiently verified with our independent proof checking tools. }, keywords = {}, pubstate = {published}, tppubtype = {conference} } Digital circuits are widely utilized in computers, because they provide models for various digital components and arithmetic operations. To avoid problems like the infamous Pentium FDIV bug, it is critical to ensure that these circuits are correct. Formal verification can be used to evaluate whether a circuit meets a given specification. Arithmetic circuits, in particular integer multipliers, pose a challenge to current verification approaches. Techniques that rely solely on SAT solving or decision diagrams appear incapable of tackling this problem in an acceptable period of time. In practice, circuit verification still requires a substantial amount of manual labor. In this talk, we will demonstrate an automated verification technique that is based on algebraic reasoning and is currently considered to be one of the most successful verification methods for circuit verification. In this approach the circuit is modeled as a set of polynomial equations that is implied by the circuit. For a correct circuit, we must demonstrate that the specification is implied by the polynomial representation of the given circuit. However, some sections of the multiplier, such as final stage adders, are difficult to check using simply computer algebra. To address this issue, we will provide a hybrid solution that blends SAT and computer algebra. But who verifies the verifier? The ability to independently generate and check proof certificates boosts confidence in the outcomes of automated reasoning tools. We present an algebraic proof calculus that allows us to obtain certificates as a by-product of circuit verification and that can be efficiently verified with our independent proof checking tools. |
Daniela Kaufmann Fuzzing and Delta Debugging And-Inverter Graph Verification Tools Conference Tests and Proofs, Nantes, France & online, 2022. @conference{KaufmannBiere-TAPSlides, title = {Fuzzing and Delta Debugging And-Inverter Graph Verification Tools}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2022/07/talk.pdf, Slides https://danielakaufmann.at/wp-content/uploads/2022/07/TAP_Kaufmann.mp4, Presentation https://easychair.org/smart-program/TAP22/, Conference}, year = {2022}, date = {2022-07-05}, booktitle = {Tests and Proofs, Nantes, France & online}, 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 Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification Conference Design, Automation and Test in Europe Conference, online, 2022. @conference{Kaufmann-DATE22, title = {Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2022/03/Kaufmann-DATE22.pdf, Slides https://danielakaufmann.at/wp-content/uploads/2022/03/TalkDATE22.mp4, Presentation https://www.date-conference.com/, Conference}, year = {2022}, date = {2022-03-23}, booktitle = {Design, Automation and Test in Europe Conference, online}, 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 SATisfiable Algebraic Circuit Verification Workshop Dagstuhl Seminar: New Perspectives in Symbolic Computation and Satisfiability Checking, Schloss Dagstuhl, Germany & online, 2022. @article{Kaufmann-Dagstuhl22, title = {SATisfiable Algebraic Circuit Verification}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2022/02/Kaufmann-Dagstuhl22.pdf, Slides https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=22072, Dagstuhl Seminar}, year = {2022}, date = {2022-02-16}, journal = {Dagstuhl Seminar: New Perspectives in Symbolic Computation and Satisfiability Checking, Schloss Dagstuhl, Germany & online}, abstract = {Although algebraic reasoning is one of the most successful methods for verifying gate-level integer multipliers, it has limitations with particular components, necessitating the use of SAT solvers in addition. As a result, proofs in two different formats are required for validation certifications. The validation results can only be trusted up to compositional reasoning because approaches to unifying certificates are not scalable. The use of dual variables in the algebraic encoding and replicating SAT-based notions in polynomial reasoning, on the other hand, eliminates the need for SAT solvers in the verification flow, resulting in a single, uniform proof certificate. In this session, I will discuss open issues in incorporating dual variables into algebraic reasoning. }, keywords = {}, pubstate = {published}, tppubtype = {article} } Although algebraic reasoning is one of the most successful methods for verifying gate-level integer multipliers, it has limitations with particular components, necessitating the use of SAT solvers in addition. As a result, proofs in two different formats are required for validation certifications. The validation results can only be trusted up to compositional reasoning because approaches to unifying certificates are not scalable. The use of dual variables in the algebraic encoding and replicating SAT-based notions in polynomial reasoning, on the other hand, eliminates the need for SAT solvers in the verification flow, resulting in a single, uniform proof certificate. In this session, I will discuss open issues in incorporating dual variables into algebraic reasoning. |
2021 |
Daniela Kaufmann Formale Verifikation von Multiplizierern mit Hilfe von Computeralgebra Workshop Kolloquium GI Dissertationspreis, online, 2021. @article{Kaufmann-GI21, title = {Formale Verifikation von Multiplizierern mit Hilfe von Computeralgebra}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2021/08/Kaufmann-GIKolloquium21.pdf, Slides https://www.dagstuhl.de/de/programm/kalender/evhp/?semnr=21193, Dagstuhl Seminar}, year = {2021}, date = {2021-06-16}, journal = {Kolloquium GI Dissertationspreis, online}, 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 = {article} } 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 AMulet 2.0 for Verifying Multiplier Circuits Conference 27th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), online, 2021. @conference{Kaufmann-TACAS21, title = {AMulet 2.0 for Verifying Multiplier Circuits}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2021/03/KaufmannBiere_TACAS21_slides.pdf, Slides https://danielakaufmann.at/wp-content/uploads/2021/03/KaufmannBiere_TACAS21_presentation.mp4, Presentation https://etaps.org/2021/tacas, Conference}, year = {2021}, date = {2021-03-31}, booktitle = {27th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), online}, 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. |
Daniela Kaufmann Combining SAT and Computer Algebra for Circuit Verification WorkshopInvited Beyond SAT Workshop at Simons Institute for the Theory of Computing, online, 2021. @conference{Kaufmann-BS21, title = {Combining SAT and Computer Algebra for Circuit Verification}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2021/02/Kaufmann-BeyondSAT21.pdf, Slides https://www.youtube.com/watch?v=OhHqpHUamCI&t=1s, Presentation https://simons.berkeley.edu/workshops/schedule/14087, Workshop}, year = {2021}, date = {2021-02-16}, booktitle = {Beyond SAT Workshop at Simons Institute for the Theory of Computing, online}, abstract = {Even more than 25 years after the Pentium FDIV bug, automated verification of arithmetic circuits, and most prominently gate-level integer multipliers, still imposes a challenge. Approaches which purely rely on SAT solving or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. In this talk, we will demonstrate a verification technique that is based on algebraic reasoning and is currently considered to be one of the most successful verification techniques for circuit verification. In this approach the circuit is modeled as a set of polynomial equations. For a correct circuit we need to show that the specification is implied by the polynomial representation of the given circuit. However parts of the multiplier, i.e., final stage adders, are hard to verify using only computer algebra. We will present a hybrid approach which combines SAT and computer algebra to tackle this issue.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Even more than 25 years after the Pentium FDIV bug, automated verification of arithmetic circuits, and most prominently gate-level integer multipliers, still imposes a challenge. Approaches which purely rely on SAT solving or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. In this talk, we will demonstrate a verification technique that is based on algebraic reasoning and is currently considered to be one of the most successful verification techniques for circuit verification. In this approach the circuit is modeled as a set of polynomial equations. For a correct circuit we need to show that the specification is implied by the polynomial representation of the given circuit. However parts of the multiplier, i.e., final stage adders, are hard to verify using only computer algebra. We will present a hybrid approach which combines SAT and computer algebra to tackle this issue. |
2020 |
Daniela Kaufmann, Mathias Fleury The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus Conference 20th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'20), online, 2020. @conference{talk-fmcad20, title = {The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus}, author = {Daniela Kaufmann and Mathias Fleury}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-FMCAD20.pdf, Slides https://www.youtube.com/watch?v=wCleCOcLpF4, Presentation https://fmcad.forsyte.at/FMCAD20/, Conference }, year = {2020}, date = {2020-09-25}, booktitle = {20th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'20)}, address = {online}, 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. |
Daniela Kaufmann Formal Verification of Integer Multiplier Circuits using Computer Algebra Keynote 14th Intl. Workshop on Boolean Problems (IWSBP), online, 2020. @conference{talk-iwsbp20, title = {Formal Verification of Integer Multiplier Circuits using Computer Algebra}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-IWSBP20.pdf, Slides http://www.informatik.uni-bremen.de/iwsbp, Workshop}, year = {2020}, date = {2020-09-23}, booktitle = {14th Intl. Workshop on Boolean Problems (IWSBP)}, address = {online}, 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 gate-level multipliers, impose a challenge for existing verification techniques. Approaches which purely rely on SAT solving or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. 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. However parts of the multiplier, i.e., 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. Complex final stage adders are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques. 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 order to validate verification results we show how proof certificates can be obtained as a by-product of verifying multiplier circuits in our reduction engine, which can be checked with our independent proof checker tool. }, 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 gate-level multipliers, impose a challenge for existing verification techniques. Approaches which purely rely on SAT solving or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. 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. However parts of the multiplier, i.e., 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. Complex final stage adders are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques. 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 order to validate verification results we show how proof certificates can be obtained as a by-product of verifying multiplier circuits in our reduction engine, which can be checked with our independent proof checker tool. |
Daniela Kaufmann Nullstellensatz-Proofs for Multiplier Verification Conference Computer Algebra in Scientific Computing (CASC'20), online, 2020. @conference{talk-casc20, title = {Nullstellensatz-Proofs for Multiplier Verification}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-CASC20.pdf, Slides http://www.casc-conference.org/2020/videos/4/01-KaufmannBiere.mp4, Presentation http://www.casc-conference.org/2020/index.html, Workshop}, year = {2020}, date = {2020-09-16}, booktitle = {Computer Algebra in Scientific Computing (CASC'20)}, address = {online}, 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 PhD Defense, Johannes Kepler University, Linz, Austria, 2020. @conference{talk-phdthesis20, title = {Formal Verification of Multiplier Circuits using Computer Algebra}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-Rigorosum20.pdf, Slides}, year = {2020}, date = {2020-04-21}, booktitle = {PhD Defense}, address = {Johannes Kepler University, Linz, Austria}, 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 = {conference} } 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 Fast Formal Verification of Multiplier Circuits using Computer Algebra Student Forum PhD Forum of Design, Automation and Test in Europe (DATE'20), online, 2020. @conference{talk-sfdate20, title = {Fast Formal Verification of Multiplier Circuits using Computer Algebra}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/PhDforum_KAUFMANN_slides.pdf, Slides https://danielakaufmann.at/wp-content/uploads/2020/11/PhDforum_KAUFMANN_presentation.mp4, Presentation https://danielakaufmann.at/wp-content/uploads/2020/11/PhDforum_KAUFMANN_poster.pdf, Poster https://www.date-conference.com/, Conference}, year = {2020}, date = {2020-04-06}, booktitle = {PhD Forum of Design, Automation and Test in Europe (DATE'20)}, address = {online}, 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.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } 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 From DRUP to PAC and Back Conference Design, Automation and Test in Europe (DATE'20), online, 2020. @conference{Talk-date20, title = {From DRUP to PAC and Back}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-DATE20.pdf, Slides https://danielakaufmann.at/wp-content/uploads/2020/11/Date_KFMN.mp4, Presentation https://danielakaufmann.at/wp-content/uploads/2020/11/poster.pdf, Poster https://www.date-conference.com/, Conference}, year = {2020}, date = {2020-03-09}, booktitle = { Design, Automation and Test in Europe (DATE'20)}, address = {online}, 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. |
2019 |
Daniela Kaufmann Combining SAT and Computer Algebra to Successfully Verify Large Multiplier Circuits Invited PLunch Talk, Carnegie Mellon University, Pittsburgh, PA, USA, 2019. @conference{talk-pittsburgh19, title = {Combining SAT and Computer Algebra to Successfully Verify Large Multiplier Circuits}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-Pittsburgh19.pdf, Slides https://csd.cmu.edu/calendar/programming-languages-lunch-talk, PLunch}, year = {2019}, date = {2019-12-03}, booktitle = {PLunch Talk}, address = {Carnegie Mellon University, Pittsburgh, PA, USA}, abstract = {Digital circuits are extensively used in computers and digital systems and it is extremely important to guarantee that these circuits are correct. 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 currently most effective approach relies on computer algebra. In this approach a word-level specification is reduced by a Gröbner basis which is implied by the gatelevel representation of the circuit. This reduction returns zero if and only if the circuit is correct. However parts of the multiplier, i.e., 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. Complex final stage address are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques. We rely 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 to verify not only large unsigned and signed multipliers much more efficiently, but also truncated multipliers.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Digital circuits are extensively used in computers and digital systems and it is extremely important to guarantee that these circuits are correct. 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 currently most effective approach relies on computer algebra. In this approach a word-level specification is reduced by a Gröbner basis which is implied by the gatelevel representation of the circuit. This reduction returns zero if and only if the circuit is correct. However parts of the multiplier, i.e., 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. Complex final stage address are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques. We rely 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 to verify not only large unsigned and signed multipliers much more efficiently, but also truncated multipliers. |
Daniela Kaufmann Combining SAT and Computer Algebra to successfully verify Large Multiplier Circuits Invited BARC Talk, University of Copenhagen, Copenhagen, Denmark, 2019. @conference{talk-cph19, title = {Combining SAT and Computer Algebra to successfully verify Large Multiplier Circuits}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-Copenhagen19.pdf, Slides https://barc.ku.dk/events/barc-talk-by-daniela-kaufmann/, BARC talks}, year = {2019}, date = {2019-11-21}, booktitle = {BARC Talk}, address = {University of Copenhagen, Copenhagen, Denmark}, abstract = {Fully automated verification of gate-level multiplier circuits remains an important problem and is still considered to be a challenge. The currently most effective approach relies on computer algebra. However parts of the multiplier, i.e., final stage adders, are a real challenge for the computer algebraic approach. In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers. Complex final stage adders are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques. Our 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.}, keywords = {}, pubstate = {published}, tppubtype = {conference} } Fully automated verification of gate-level multiplier circuits remains an important problem and is still considered to be a challenge. The currently most effective approach relies on computer algebra. However parts of the multiplier, i.e., final stage adders, are a real challenge for the computer algebraic approach. In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers. Complex final stage adders are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques. Our 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. |
Daniela Kaufmann Verifying Large Multipliers by Combining SAT and Computer Algebra Conference 19th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19), San Jose, CA, USA, 2019. @conference{talk-fmcad19, title = {Verifying Large Multipliers by Combining SAT and Computer Algebra}, author = {Daniela Kaufmann}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-FMCAD19.pdf, Slides https://fmcad.forsyte.at/FMCAD19/, Conference}, year = {2019}, date = {2019-10-24}, booktitle = {19th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19)}, address = {San Jose, CA, USA}, 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. |
2018 |
Daniela Ritirc (*) A Practical Polynomial Calculus for Arithmetic Circuit Verification Workshop 3rd Intl. Workshop on Satisfiability Checking and Symbolic Computation (SC2'18) at FLoC, Oxford, United Kingdom, 2018. @conference{talk-sc218, title = {A Practical Polynomial Calculus for Arithmetic Circuit Verification}, author = {Daniela Ritirc (*)}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Ritirc-SC218.pdf, Slides}, year = {2018}, date = {2018-08-15}, booktitle = {3rd Intl. Workshop on Satisfiability Checking and Symbolic Computation (SC2'18) at FLoC}, address = {Oxford, United Kingdom}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Daniela Ritirc (*) On the Problem of Arithmetic Circuit Verification Using Computer Algebra Invited Theory Reading Group Meeting, KTH Royal Institute of Technology, Stockholm, Sweden, 2018. @conference{talk-stockholm18, title = {On the Problem of Arithmetic Circuit Verification Using Computer Algebra}, author = {Daniela Ritirc (*)}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Ritirc-Stockholm18.pdf, Slides}, year = {2018}, date = {2018-04-18}, booktitle = {Theory Reading Group Meeting}, address = {KTH Royal Institute of Technology, Stockholm, Sweden}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
2017 |
Daniela Ritirc (*) Column-Wise Verification of Multipliers Using Computer Algebra Conference 17th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17), Vienna, Austria, 2017. @conference{Talk-fmcad17, title = {Column-Wise Verification of Multipliers Using Computer Algebra}, author = {Daniela Ritirc (*)}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Ritirc-FMCAD17.pdf, Slides}, year = {2017}, date = {2017-10-18}, booktitle = {17th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17)}, address = {Vienna, Austria}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Daniela Ritirc (*) Complexity of Circuit Ideal Membership Testing Workshop 2nd Intl. Workshop on Satisfiability Checking and Symbolic Computation (SC2'17), Kaiserslautern, Germany, 2017. @conference{Talk-sc217, title = {Complexity of Circuit Ideal Membership Testing}, author = {Daniela Ritirc (*)}, url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Ritirc-FMCAD17.pdf, Slides}, year = {2017}, date = {2017-07-13}, booktitle = {2nd Intl. Workshop on Satisfiability Checking and Symbolic Computation (SC2'17)}, address = {Kaiserslautern, Germany}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
(*) Before 10/2018 I published using my maiden name ‘Ritirc’.