Skip to Main content Skip to Navigation

Deductive Verification via Ghost Debugging

Abstract : We present a verification approach based on auxiliary programs, which we call ghost debuggers. This approach leads to notable verification gains when the structure of the program does not match the execution structure, notably when that latter structure is recursive. We present a theoretical foundation of our approach over a flavor of transfinite games, which let us specify and prove fine-grained properties about infinite behaviors of programs. By making use of the game structure, we also show that our approach can be applied to relational properties like simulation between programs. Our approach is backed by a mechanized development in the Why3 tool, which formally proves sound the Hoare-style logic backbone of our approach.
Document type :
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Monday, October 29, 2018 - 3:57:43 PM
Last modification on : Saturday, June 25, 2022 - 10:33:54 PM
Long-term archiving on: : Wednesday, January 30, 2019 - 4:46:21 PM


Files produced by the author(s)


  • HAL Id : hal-01907894, version 1


Martin Clochard, Andrei Paskevich, Claude Marché. Deductive Verification via Ghost Debugging. [Research Report] RR-9219, Inria Saclay Ile de France. 2018. ⟨hal-01907894⟩



Record views


Files downloads