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.
Here is a set of benchmarks obtained with our tools
- Caduceus benchmarks: in Why syntax, in SMT syntax
- Caduceus benchmarks, with -separation -exp all options: in Why syntax, in
- Why benchmarks: in Why
syntax, in SMT syntax
- Krakatoa benchmarks: in Why
syntax, in SMT syntax
The Ergo theorem prover
The Why/Krakatoa/Caduceus premits some translations between prover
- The standalone simplify2why tool translates a file in
the Simplify syntax to Why syntax
- The why tool itself, when invoked with option
--smtlib --encoding sstrat, translates Why syntax
into SMTLIB 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
Possible encodings are selected by --encoding [mode] where
| 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
| sstrat||encodes types using some types + strat :
Expressions are syntactically typed by adding the
sort information directly in term.
There are basically two cases
- A term that is not of sort INT is translated into
a stratified tree
(e.g. l of sort t becomes
- For functional and predicative symbols of sort INT,
a special treatment is applied on.
Polymorphic symbols are instantiated with respect to
the context they are applied on
(e.g. append : a' list × a' list -> a' list leads to
append_int and append_float
if int_list and float_list are in
Such encoding exploits the multi-sorted logic
for encoding polymorphism.
There are basically three cases
- For a term that is not of sort INT and
which is not used in a INT context, the translation
of the outermost symbol is the same as in strat.
- For a term of sort INT and which is used in an INT
context, the outermost term is not modified.
- For a term of sort INT in a polymorphic context and
a term of an instantiated sort which is used in an INT context
a special treatment is provided.
Aims at expanding the definition predicates instead of adding an
equivalence formulae. Needs one parameter:
- all : Expansion is done in both theory and goal.
- goal : Expansion is restricted to the goal.
Consequently, definitions are added in theory.