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.

翻译：全功能程序验证是一个不可判定的——因此本质上困难的——任务，它无法自动求解，通常需要用户交互与指导。现有验证器要么以自动活性化方式工作，要求用户在源代码中编写注解，却无法检查证明状态或在失败尝试时进行干预；要么允许在逻辑编码层级进行交互，但该层级低于用户提供的规约。我们提出一种新颖的交互概念，允许用户在源代码与规约级别上检查并交互于证明状态，从而最小化表示之间的心理差距。我们以Java验证引擎KeY的插件形式实现了该概念，并通过用户研究表明，该原型可帮助用户理解证明状态并定位源代码或规约中的缺陷。