EVE
What is EVE
Eve is a development environment integrating formal verification with the standard tools offered by programming environments for object-oriented development (editor, compiler, debugger, ...).
Eve is built on top of EiffelStudio, the main IDE for Eiffel developers.
Demo video
Click the image for a demo video.
The integration of tools in Eve
The implementation of Eve continues to evolve as a result of ongoing efforts to integrate more verification techniques and new verification tools. The currently available implementation focuses on the combination of two well-known techniques:
- Static verification based on Hoare-style proofs; this is currently implemented in Eve through the AutoProof tool.
- Dynamic analysis based on random testing; this is currently implemented through the AutoTest tool.
Eve includes the results of other verification projects of the Chair of Software Engineering (such as AutoFix and AutoInfer), but these are currently available only by explicit invocation, while the integration of AutoTest and AutoProof is fully automatic and seamless.
How to install Eve
You can download the latest build for your platform (currently only for Windows 64bit and Linux 64bit). If no build exists for your platform, you can compile Eve yourself following the instructions on the development wiki to install Eve.
Eve is distributed under the terms of the GNU General Public License, with the exception of the third-party verification engines it depends on, which are distributed with their respective licenses.
The AutoProof component in the current implementation of Eve depends, in particular, on the Microsoft Boogie verifier; to use this component you must agree to Microsoft's distribution terms. Boogie's precompiled binary works only under Windows, but you can use Wine to run it under a GNU/Linux environment by following these instructions (courtesy of Daniel Kroeni).