AutoProof

AutoProof is an auto-active verifier for object-oriented programs written in the Eiffel programming language. It uses Boogie as a back-end.

This page documents AutoProof 2015: the version of AutoProof presented in the TACAS 2015 and FM 2015 papers listed below. AutoProof 2015 offers a stable set of features; it is made available here for future reference. Henceforth, we refer to AutoProof 2015 simply as AutoProof.

Try AutoProof online

You can use AutoProof on ComCom in your browser without downloading anything. AutoProof on Comcom is limited to single-class projects.

Download AutoProof

AutoProof is a component of the open-source Eiffel Verification Environment (EVE). To use all features of AutoProof you can download a pre-compiled version of EVE (see file INSTALL for the simple installation instructions).

Documentation

• Tutorial: the tutorial gets you started with AutoProof.
• Manual: the manual offers a more systematic description of AutoProof.
• Class reference: API documentation of library classes used to annotate programs for AutoProof, including the Mathematical Modeling Library (MML), as well as array and list classes for simpler specifications.

Gallery of verified programs

A software repository collects a suite of benchmark problems implemented in Eiffel and verified with AutoProof. You can run verification online and see the results!

Contributors

The following people took part in the AutoProof project:

• Julian Tschannen
• Nadia Polikarpova
• Carlo A. Furia
• Martin Nordio
• Bertrand Meyer

AutoProof Source code

The source code of EVE (with AutoProof) is also available; it is distributed under GPL v. 2. AutoProof was written by Julian Tschannen and Nadia Polikarpova.

Publications

• A Fully Verified Container Library
  Nadia Polikarpova, Julian Tschannen, and Carlo A. Furia
  In Proceedings of 20th International Symposium on Formal Methods (FM 15), 2015. (Best paper award at FM 2015.) [PDF] [BIB]

  EiffelBase 2 is a container library which we successfully verified against full functional correctness specifications using AutoProof. This paper describes these results, which constitute the largest verification challenge succesfully tackled using AutoProof. EiffelBase 2 is available online, where it can be verified through AutoProof's online interface.

• AutoProof: Auto-active Functional Verification of Object-oriented Programs
  Julian Tschannen, Carlo A. Furia, Martin Nordio and Nadia Polikarpova
  In Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 15), 2015. [PDF] [BIB]

  A tool paper presenting AutoProof's interface, design, and implementation features. It also discusses AutoProof's performance on a collection of benchmark problems (the benchmark problems are also available online).

• The AutoProof Verifier: Usability by Non-Experts and on Standard Code
  Carlo A. Furia, Christopher M. Poskitt, and Julian Tschannen
  In Proceedings of 2nd Workshop on Formal Integrated Development Environment (F-IDE 2015), 2015. [PDF] [BIB]

  An overview of the challenges faced by serious non-expert users (namely, students of a course on software verification) using AutoProof.

• Flexible Invariants Through Semantic Collaboration
  Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, and Bertrand Meyer
  In Proceedings of 19th International Symposium on Formal Methods (FM 14), 2014. [PDF] [BIB]

  Reasoning about programs manipulating objects in the heap requires a flexible methodology to specify how objects depend on each other to maintain global consistency. This paper describes Semantic Collaboration, the methodology implemented in AutoProof that can successfully be applied to a variety of idiomatic object-oriented patterns. An extended version of this paper, with the source code of the benchmark problems discussed there, is available in a different repository.

• AutoProof Meets Some Verification Challenges
  Julian Tschannen, Carlo A. Furia, and Martin Nordio
  In International Journal on Software Tools for Technology Transfer (STTT), Special Section on Program Verification, 2014. [PDF] [BIB]

  This paper discusses how an earlier version of AutoProof fared in solving the challenges of the VerifyThis verification competition at FM 2012. Note that AutoProof 2015 does not have several of the limitations described in this paper.

• Program Checking With Less Hassle
  Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
  In Proceedings of Verified Software: Theories, Tools and Experiments (VSTTE), 2013. [PDF] [BIB]

  This paper describes two-step verification: a technique to debug failed verification attempts based on using call inlining and loop unrolling to help identify shortcomings in the specification rather than in the implementation that make verification fail.

• Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach
  Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
  In Tools for Practical Software Verification - LASER 2011, International Summer School, 2012. [PDF] [BIB]

  This paper describes techniques to encode in Boogie the semantics of advanced object-oriented features including Eiffel-style exceptions, polymorphism, and function objects (called agents in Eiffel).

• Verifying Eiffel Programs with Boogie
  Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
  Presented at BOOGIE 2011. [PDF] [BIB]

  This is a preliminary version of the paper Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach.

• Reasoning about Function Objects
  Martin Nordio, Cristiano Calcagno, Bertrand Meyer, Peter Müller, and Julian Tschannen
  In Proceedings of the 48th International Conference on Objects, Models, Components and Patterns (TOOLS-EUROPE 2010). [PDF] [BIB]

  This presents some ideas about verifying function objects that are extended in the paper Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach.

• Automatic Verification of Eiffel Programs
  Julian Tschannen
  Master's Thesis, ETH Zürich, Chair of Software Engineering, 2009. [PDF]

This thesis presents the first implementation of AutoProof. As a description of AutoProof and of its underlying techniques it is superseded by later publications.