Practical Algebraic Calculus Checker

Mathias Fleury 🌐 and Daniela Kaufmann 🌐

August 31, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session PAC_Checker