Why Benchmarks

The Why/Krakatoa/Caduceus platform allows to perform deductive verification of C or Java programs. Verification conditions are generated, which have to be discharged by theorem provers.

This page collects sets of goals generated, which can serve as benchmarks for theorem provers. Benchmarks are available both in the SMT-LIB syntax, and in our own syntax Why, which can itself be translated into many other theorem provers.

Benchmarks

Here is a set of benchmarks obtained with our tools

The Ergo theorem prover

Translation tools

The Why/Krakatoa/Caduceus premits some translations between prover syntax:

More generally, the why command-line tool, when invoked with options for specific prover, translates Why syntax into the syntax for this prover. Since Why syntax allows polymorphics sorts, an encoding is usually required.

Available provers are
--simplify Simplify prover, erasing types by default
--smtlib SMT syntax
--coq Coq proof assistant
--pvs PVS
--hol-light HOL Light prover
--mizar Mizar
--harvey haRVey
--isabelle Isabelle/HOL
--hol4 HOL4
--cvcl CVC Lite
--zenon Zenon
--gappa Gappa

Possible encodings are selected by --encoding [mode] where modes are:
none does not encode types into terms for untyped provers
pred encodes types with predicates (may not be used for SMTLIB provers)
strat encodes types into terms (may not be used for SMTLIB provers)
rec encodes types with typing axioms (may not be used for SMTLIB provers)
mono encodes types using monomorphisation, i.e. instantiates polymorphic symbols according to the context they are applied on
sstratencodes types using some types + strat :

Polymorphism Encodings

Miscellaneous Options