A New Interaction Concept for Interactive and Autoactive Program Verification
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911661025132544 |
|---|---|
| author | Pfeifer, Wolfram Ulbrich, Mattias Drodt, Daniel |
| author_facet | Pfeifer, Wolfram Ulbrich, Mattias Drodt, Daniel |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_06972 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A New Interaction Concept for Interactive and Autoactive Program Verification Pfeifer, Wolfram Ulbrich, Mattias Drodt, Daniel Programming Languages Logic in Computer Science D.2.4; F.3.1 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. |
| title | A New Interaction Concept for Interactive and Autoactive Program Verification |
| topic | Programming Languages Logic in Computer Science D.2.4; F.3.1 |
| url | https://arxiv.org/abs/2605.06972 |