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

• 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 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

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

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.