Email Gateway (Aug 31 2020 at 13:01): Email Gateway (Aug 31 2020 at 13:01):From: Manuel Eberl <eberlm@in.tum.de>
Practical Algebraic Calculus Checker
by Mathias Fleury and Daniela Kaufmann
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.
https://www.isa-afp.org/entries/PAC_Checker.html
Enjoy,
Manuel
Last updated: Jan 04 2025 at 20:18 UTC