AutoProof Manual

Overview

This manual describes how to use AutoProof. AutoProof is an auto-active verifier for the Eiffel programming language that can prove functional correctness of Eiffel programs annotated with contracts. AutoProof is available as part of the Eiffel Verification Environment (EVE) or via an online version.