AutoProof is an auto-active (AutoProof tries to achieve an intermediate degree of automation in the continuum that goes from automatic to interactive) 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 Auto-Proof through hands-on exercises.

Each of the following sections describes in detail the use of AutoProof based on increasingly complex examples. Each example is used throughout one section to explain some of the concepts behind AutoProof and how they are used to verify programs. Each section also has hands-on exercises with verification tasks for one or more programs.

The old online version is available.