The AutoProof Verifier: Usability by Non-Experts and on Standard Code
This work addresses usability issues in formal verification tools for programmers with limited formal methods experience, but it is incremental as it focuses on evaluating an existing tool rather than introducing new methods.
The paper tackled the problem of formal verification tools being difficult for non-experts to use by evaluating AutoProof's usability in two contexts: with graduate students verifying sorting algorithms and on undergraduate programming assignments, reporting experiences and lessons learned.
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.