Links und Funktionen

You are here: Home / Publikationen / Elimination of Ghost Variables in Program Logics


Martin Hofmann and Mariela Pavlova (2007)

Elimination of Ghost Variables in Program Logics

In: Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, ed. by Gilles Barthe and Cédric Fournet, vol. 4912, pp. 1-20, Springer. Lecture Notes in Computer Science (ISBN: 978-3-540-78662-7).

Ghost variables are assignable variables that appear in program annotations but do not correspond to physical entities. They are used to facilitate specification and verification, e.g., by$~$ using a ghost variable to count the number of iterations of a loop, and also to express extra-functional behaviours. In this paper we give a formal model of ghost variables and show how$~$ they can be eliminated from specifications and proofs in a compositional and automatic way. Thus, with the results of this paper ghost variables can be seen as a specification pattern$~$ rather than a primitive notion.

Document Actions