Usability of AutoProof: a case study of software verification
This addresses usability challenges in software verification tools for developers, but it is incremental as it focuses on a specific case study.
The study evaluated the usability of the AutoProof verification tool on the Tokeneer benchmark, finding it effective in verifying real software and automatically discharging nearly two-thirds of verification conditions, while highlighting needs for better documentation and tool improvements.
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.