A New Interaction Concept for Interactive and Autoactive Program Verification

TL;DR

This paper introduces a new user interaction concept for program verification that enables inspection and interaction at the source code level, improving user understanding and defect detection.

Contribution

The paper presents a novel interaction approach integrated into the KeY verification engine, bridging the gap between proof state and source code for better usability.

Findings

User study shows improved understanding of proof states.

Prototype helps users identify defects more effectively.

Interaction at source code level reduces mental overhead.

Abstract

Fully functional program verification is an undecidable$\unicode{x2014}$and, hence, inherently difficult$\unicode{x2014}$task, that is not automatically solvable but typically requires user interaction and guidance. Existing verifiers either work autoactively, requiring the user to write annotations in source code, without the possibility to inspect the proof state or intervene in case of an unsuccessful attempt, or allow interactions on a logical encoding that is on a lower level than the user-provided specifications. We present a novel interaction concept which allows the user to inspect and interact with the proof state on source code and specification level. This minimizes the mental gap between the representations. We provide an implementation of the concept as a plugin for the Java verification engine KeY, and show with a user study that this prototype can be beneficial for users to understand the proof state and find defects in source code or specifications.