AutoProof Tutorial


AutoProof is an auto-active verifier for the Eiffel programming language; it proves functional correctness of Eiffel programs annotated with contracts. The goal of this tutorial is to show how to verify Eiffel programs with AutoProof through hands-on exercises.


The tutorial is available as a PDF document. The exercises can either be done locally on your machine using EVE or using the online version of AutoProof.

To use AutoProof locally you can install the latest EVE build on your machine and download the examples and exercises from this page. Although it is possible to do the verification exercises online, some options are not available on the web.

Note: on Linux, Mono is used to run Boogie. On Ubuntu you can install the package mono-complete.

Material for Download

Material for the Web