AutoProof
=========

[AutoProof](http://se.inf.ethz.ch/research/autoproof/) is an auto-active verifier for the Eiffel programming language; it proves functional correctness of Eiffel programs annotated with contracts.

This repository contains the sources for a [tutorial on AutoProof](http://se.inf.ethz.ch/research/autoproof/tutorial/) and for an [online repository of examples](http://se.inf.ethz.ch/research/autoproof/repo/) verified with AutoProof. You find these resources at the research page of the Chair of Software Engineering of ETH Zurich.