The PAC Checkers, Pacheck and Pastèque
This page provides access to the source code, benchmarks, and experiments.
The goal of Pacheck and Pastèque is to provide a checker for PAC proofs with extensions. The former provides an efficient implementation, while the latter provides maximal trust as it verified using the proof assistant Isabelle/HOL.
2021: Pacheck 2.0 and Pastèque 2.0 are released here.
For Pacheck, ensure GMP (on linux, use your package manager) is installed and use ``./configure.sh && make''.
For Pasteque, ensure MLton is installed and use ``make''.
A small set of examples is available here
[ KaufmannFleuryBiere-FMCAD20-data.tar.xz ] experimental data (21.8 MB)