AutoProof

AutoProof is an auto-active verifier for functional properties of the Eiffel programming language. It uses the Boogie verifier as a back-end.

AutoProof 2015

Resources and documentation specific to the version of AutoProof presented in the TACAS 2015 and FM 2015 papers are available on a separate page.

Online interface and download

AutoProof is available via a web-interface and is integrated in the open-source Eiffel Verification Environment (EVE), which can be downloaded for free.

Documentation

The following documentation is available:

• Tutorial: the tutorial will get you started with AutoProof.
• Manual: the manual offers a more systematic description of AutoProof.
• Class reference: interface description of MML, array and list classes.
• Software repository: a suite of benchmark problems implemented in Eiffel and verified with AutoProof.

Project members

Current

• Martin Nordio
• Carlo A. Furia
• Bertrand Meyer

Former

• Julian Tschannen
• Nadia Polikarpova

Publications

2015

• 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. [PDF] [BIB]

  This paper details the results of the successful verification of a container library with AutoProof. The library can be verified with 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]

  This paper presents AutoProof's interface, design, and implementation features, and demonstrates AutoProof's performance on a rich collection of benchmark problems. The benchmark problems are 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]

2014

• 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]

  This paper describes a flexible technique for framing and collaborative class invariants. An extended version of the paper and the source code of the problems are available online.

• 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 describes how AutoProof fares in solving the verification challenges posed at FM 2012. Note that the current version of AutoProof already removes some of the limitations described in this paper.

2013

• 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 the two-step verification approach. With this approach, a failed verification is followed by a second verification step using function call inlining and loop unrolling. In case the second verification step succeeds, the verification is more likely to be in need of an improved specification rather then an improved implementation.

2012

• 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 prove object-oriented programs with Eiffel-style exceptions, polymorphism and agents (function objects). The content here subsumes previous publications.

2011

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

  See Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach.

2010

• 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] [Springer-Online]

  See Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach.

2009

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