Practical Algebraic Calculus Checker (Q7361855)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry PAC_Checker
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Practical Algebraic Calculus Checker |
AFP entry PAC_Checker |
Statements
31 August 2020
0 references
Mathias Fleury
0 references
Daniela Kaufmann
0 references
Practical Algebraic Calculus Checker (English)
0 references
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.
0 references
