Usability of AutoProof: a case study of software verification

TL;DR

This paper evaluates the usability of AutoProof, a software verification tool, using the Tokeneer benchmark, highlighting its strengths in verification efficiency and identifying areas for usability improvements.

Contribution

It provides a case study on AutoProof's usability, demonstrating its verification capabilities and pinpointing specific usability and documentation issues.

Findings

AutoProof effectively verifies real software.

Nearly two thirds of verification conditions are automatically discharged.

Identifies need for better documentation and tool improvements.

Abstract

Many verification tools come out of academic projects, whose natural constraints do not typically lead to a strong focus on usability. For widespread use, however, usability is essential. Using a well-known benchmark, the Tokeneer problem, we evaluate the usability of a recent and promising verification tool: AutoProof. The results show the efficacy of the tool in verifying a real piece of software and automatically discharging nearly two thirds of verification conditions. At the same time, the case study shows the demand for improved documentation and emphasizes the need for improvement in the tool itself and in the Eiffel IDE.