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.

News

2021: Pacheck 2.0 and Pastèque 2.0 are released here.

2020: First release of Pacheck (available here) and Pastèque (available here).

Compilation

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

Examples

A small set of examples is available here

Experimental Data

[ KaufmannFleuryBiere-FMCAD20-data.tar.xz ] experimental data (21.8 MB)