Deductive Verification via the Debug Adapter Protocol

Gidon Ernst
(LMU Munich)
Johannes Blau
(LMU Munich)
Toby Murray
(University of Melbourne)

We propose a conceptual integration of deductive program verification into existing user interfaces for software debugging. This integration is well-represented in the "Debug Adapter Protocol", a widely-used and generic technology to integrate debugging of programs into development environments. Commands like step-forward and step-in are backed by steps of a symbolic structural operational semantics, and the different paths through a program are readily represented by multiple running threads of the debug target inside the user interface. Thus, existing IDEs can be leveraged for deductive verification debugging with relatively little effort. We have implemented this scheme for SecC, an auto-active program verifier for C, and discuss its integration into Visual Studio Code.

In José Proença and Andrei Paskevich: Proceedings of the 6th Workshop on Formal Integrated Development Environment (F-IDE 2021), Held online, 24-25th May 2021, Electronic Proceedings in Theoretical Computer Science 338, pp. 89–96.
Published: 6th August 2021.

ArXived at: http://dx.doi.org/10.4204/EPTCS.338.11 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org