Scalable Fine-Grained Proofs for Formula Processing

Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine

We provide here the binary, options and experimental data for our CADE paper and the companion report.


The tarball containing the source code of veriT used in our experiments is available here. The command line parameters of veriT used in each of the configurations described in the paper are:

The benchmarks can be found here, divided according to the categories in SMT-LIB.

Our experiments were conducted on servers equipped with two Intel Xeon E5-2630 v3 processors, with eight cores per processor, and 126 GB of memory. The time limit was set to 30 s.


The experimental data for each configuration: