Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Practical Algebraic Calculus C...


view this post on Zulip 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: Dec 05 2021 at 23:19 UTC