The Spirit of Ghost Code

Abstract : In the context of deductive program verification, ghost code is part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without any observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, a rigorous definition and treatment of ghost code is surprisingly subtle and few formalizations exist. In this article, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the proce- dure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-00873187
Contributor : Léon Gondelman <>
Submitted on : Wednesday, May 14, 2014 - 4:28:27 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Thursday, August 14, 2014 - 12:01:30 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00873187, version 3

Collections

Citation

Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich. The Spirit of Ghost Code. CAV 2014, Computer Aided Verification - 26th International Conference, Jul 2014, Vienna Summer Logic 2014, Austria. ⟨hal-00873187v3⟩

Share

Metrics

Record views

1147

Files downloads

971