### 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.

### License

BSD License

### Topics

- Computer science/Algorithms

### Session PAC_Checker

- PAC_More_Poly
- Finite_Map_Multiset
- WB_Sort
- More_Loops
- PAC_Specification
- PAC_Map_Rel
- PAC_Checker_Specification
- PAC_Polynomials
- PAC_Polynomials_Term
- PAC_Polynomials_Operations
- PAC_Misc
- PAC_Checker
- PAC_Checker_Relation
- PAC_Assoc_Map_Rel
- PAC_Checker_Init
- PAC_Version
- PAC_Checker_Synthesis
- PAC_Checker_MLton

### Depends on

- Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
- Executable Multivariate Polynomials
- The Imperative Refinement Framework

## Cite

×

PAC_Checker-AFP

    @article{PAC_Checker-AFP,
      author  = {Mathias Fleury and Daniela Kaufmann},
      title   = {Practical Algebraic Calculus Checker},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/PAC_Checker.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Aug 31, 2020 : Isabelle2020