AutoProof

AutoProof is a verifier of object-oriented programs that uses Boogie as a back-end. AutoProof is an ongoing development of the Chair of Software Engineering at SIT, based on an earlier implementation at ETH Zurich.

AutoProof online

You can use AutoProof in your browser without downloading anything. This version is limited to single-class projects.

AutoProof as a GitHub action

You can make AutoProof action part of your GitHub project continuous development pipeline.

Docker image with AutoProof

You can pull a Docker image with a full-fledged Linux-based distribution of AutoProof.

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!

Documentation

• Tutorial: the tutorial gets you started with AutoProof.
• Manual: the manual offers a more systematic description of AutoProof.

Current contributors

The following people are currently working on AutoProof (alphabetically):

• Alexander Kogtenkov
• Alexandr Naumchev
• Alisa Arkadova
• Bertrand Meyer
• Li Huang

Former contributors

The following people have initially developed AutoProof:

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

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 that 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.