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 :
Reports
Complete list of metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-01907894
Contributor : Claude Marché <>
Submitted on : Monday, October 29, 2018 - 3:57:43 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Wednesday, January 30, 2019 - 4:46:21 PM

File

RR-9219.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01907894, version 1

Citation

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

Share

Metrics

Record views

87

Files downloads

70