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
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.
iVer
| iVer is a small editor and IDE that allows editing of Eiffel code, while a fully automatic prover based on Ballet, Boogie and Simplify. |
|
News
- 2006-02-21: first version of the homepage