Deductive Verification with Ghost Monitors

Martin Clochard 1 Claude Marché 2 Andrei Paskevich 2
2 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 new approach to deductive program verification based on auxiliary programs called ghost monitors. This technique is useful when the syntactic structure of the target program is not well suited for verification, for example, when an essentially recursive algorithm is implemented in an iterative fashion. Our approach consists in implementing, specifying, and verifying an auxiliary program that monitors the execution of the target program, in such a way that the correct-ness of the monitor entails the correctness of the target. This technique is also applicable when we want to establish relational properties between two target programs written in different languages and having different syntactic structure. The ghost monitor maintains the necessary data and invariants to facilitate the proof. It can be implemented and verified in any suitable framework, which does not have to be related to the language of the target programs. We introduce one such framework, with an original extension that allows us to specify and prove fine-grained properties about infinite behaviors of target programs. The proof of correctness of our approach relies on a particular flavor of transfinite games. This proof is formalized and verified using the Why3 tool.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

https://hal.inria.fr/hal-01926659
Contributor : Claude Marché <>
Submitted on : Monday, November 19, 2018 - 1:43:22 PM
Last modification on : Friday, April 19, 2019 - 4:55:11 PM
Long-term archiving on : Wednesday, February 20, 2019 - 2:27:19 PM

File

article.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01926659, version 1

Citation

Martin Clochard, Claude Marché, Andrei Paskevich. Deductive Verification with Ghost Monitors. 2018. ⟨hal-01926659⟩

Share

Metrics

Record views

69

Files downloads

150