Deductive Verification via Ghost Debugging

Martin Clochard 1, 2 Andrei Paskevich 1 Claude Marché 1
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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

https://hal.inria.fr/hal-01907894
Contributor : Claude Marché <>
Submitted on : Monday, October 29, 2018 - 3:57:43 PM
Last modification on : Tuesday, March 5, 2019 - 9:30:11 AM
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

76

Files downloads

57