Deductive Verification via the Debug Adapter Protocol

TL;DR

This paper introduces a method to integrate deductive program verification into existing debugging interfaces using the Debug Adapter Protocol, enabling verification debugging within familiar IDEs like Visual Studio Code.

Contribution

It presents a novel approach to combine deductive verification with standard debugging tools through the Debug Adapter Protocol, demonstrated with an implementation for SecC in Visual Studio Code.

Findings

Seamless integration of deductive verification into IDEs.

Implementation of verification commands using symbolic semantics.

Enhanced debugging capabilities for program verification.

Abstract

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.