iVer and Ballet
iVer and Ballet are an effort to verifiy properties of Eiffel classes, more specifically the partial and total correctness. In the context of Eiffel, we want to prove classes with respect to their contracts.
The introduction of formal methods into software development relies on the ability of the method to support the developer in his daily struggle for reliable and bug-free software.
Ballet is a tool to translate standard Eiffel classes into BoogiePL text. BoogiePL is a programming language developed at Microsoft Research and the core of the verification technologie behind Spec#, called Boogie. Boogie itself relies on the fully automatic prover Simplify to discharge its proof-obligations.
Ballet can be used as a stand-alone command line application or as a Eiffel library.
Publicationsno publications yet
Downloadsno downloads yet