  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.
