Practical Algebraic Calculus Checker

Title:	Practical Algebraic Calculus Checker
Authors:	Mathias Fleury and Daniela Kaufmann
Submission date:	2020-08-31
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 (PAC). 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.
BibTeX:	@article{PAC_Checker-AFP, author = {Mathias Fleury and Daniela Kaufmann}, title = {Practical Algebraic Calculus Checker}, journal = {Archive of Formal Proofs}, month = aug, year = 2020, note = {\url{http://isa-afp.org/entries/PAC_Checker.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Nested_Multisets_Ordinals, Polynomials
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.