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 SMTLIB 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
 Caduceus benchmarks: in Why syntax, in SMT syntax
 Caduceus benchmarks, with separation exp all options: in Why syntax, in
SMT syntax
 Why benchmarks: in Why
syntax, in SMT syntax
 Krakatoa benchmarks: in Why
syntax, in SMT syntax
The Ergo theorem prover
Translation tools
The Why/Krakatoa/Caduceus premits some translations between prover
syntax:
 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 commandline 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
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

sstrat  encodes types using some types + strat :

Polymorphism Encodings
 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
sort(t,l)).
 For functional and predicative symbols of sort INT,
a special treatment is applied on.
 mono
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
the context).
 sstrat
Such encoding exploits the multisorted 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.
Miscellaneous Options
 exp
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.