Daniela Kaufmann, Mathias Fleury, Armin Biere,
"The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus"
, in Alexander Ivrii, Ofer Strichman: Proc. Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'20), Serie Conference Series: Formal Methods in Computer-Aided Design, Vol. 01, TU Wien Akademic Press, 9-2020, ISBN: 978-3-85448-042-6
Original Titel:
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'20)
Original Kurzfassung:
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.
Sprache der Kurzfassung:
Englisch
Veröffentlicher:
TU Wien Akademic Press
Serie:
Conference Series: Formal Methods in Computer-Aided Design