The AutoProof Verifier: Usability by Non-Experts and on Standard Code

TL;DR

This paper evaluates AutoProof's usability for non-experts, including students and standard code, highlighting challenges and lessons learned to improve formal verification tools' accessibility.

Contribution

It provides empirical insights into AutoProof's usability in educational settings and offers suggestions for enhancing verification tools for non-expert users.

Findings

AutoProof can verify real-world code with non-experts' input.

Usability challenges include complexity and learning curve.

Lessons learned inform future verification tool development.

Abstract

Formal verification tools are often developed by experts for experts; as a result, their usability by programmers with little formal methods experience may be severely limited. In this paper, we discuss this general phenomenon with reference to AutoProof: a tool that can verify the full functional correctness of object-oriented software. In particular, we present our experiences of using AutoProof in two contrasting contexts representative of non-expert usage. First, we discuss its usability by students in a graduate course on software verification, who were tasked with verifying implementations of various sorting algorithms. Second, we evaluate its usability in verifying code developed for programming assignments of an undergraduate course. The first scenario represents usability by serious non-experts; the second represents usability on "standard code", developed without full functional verification in mind. We report our experiences and lessons learnt, from which we derive some general suggestions for furthering the development of verification tools with respect to improving their usability.