Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

8-2015

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.

Discipline

Theory and Algorithms

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings 2nd International Workshop on Formal Integrated Development Environment (F-IDE 2015): Oslo, Norway, June 22

Issue

187

First Page

42

Last Page

55

Identifier

10.4204/EPTCS.187.4

Publisher

Open Publishing Association

City or Country

Waterloo, NSW

Additional URL

https://doi.org/10.4204/EPTCS.187.4

Download

Share

COinS