Elimination of Ghost Variables in Program Logics

  • Martin Hofmann
  • Mariela Pavlova
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4912)


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.


Program Logic Smart Card Operational Semantic Program Variable Proof Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cataño, N., Huisman, M.: Formal specification of Gemplus’ electronic purse case study using ESC/Java. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 272–289. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Jacobs, B., Marché, C., Rauch, N.: Formal verification of a commercial smart card applet with multiple tools. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, Springer, Heidelberg (2004)Google Scholar
  3. 3.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: Proceeding of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, Berlin, Germany, pp. 234–245. ACM Press, New York (2002)CrossRefGoogle Scholar
  4. 4.
    Guttag, J.V., Horning, J.J. (eds.): Larch: Languages and Tools for Formal Specification. In: Garland, S.J., Jones, K.D., Modet, A., Wing, J.M. (eds.) Texts and Monographs in Computer Science, Springer, Heidelberg (1993)Google Scholar
  5. 5.
    Barnett, M., Leino, K., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 151–171. Springer, Heidelberg (2005)Google Scholar
  6. 6.
    Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL 1997), Paris, pp. 106–119 (1997)Google Scholar
  7. 7.
    Appel, A.W.: Foundational proof-carrying code. In: Proc. IEEE Symp. Logic in Computer Science (LICS 2001) (2001)Google Scholar
  8. 8.
    Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile resource guarantees for smart devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 1–26. Springer, Heidelberg (2005)Google Scholar
  9. 9.
    Barthe, G., Beringer, L., Crégut, P., Grégoire, B., Hofmann, M., Müller, P., Poll, E., Puebla, G., Stark, I., Vétillard, E.: Mobius: Mobility, ubiquity, security. objectives and progress report. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, Springer, Heidelberg (2007)CrossRefGoogle Scholar
  10. 10.
    Barnett, M., Deline, R., Fähndrich, M., Rustan, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)Google Scholar
  11. 11.
    Pavlova, M., Barthe, G., Burdy, L., Huisman, M., Lanet, J.L.: Enforcing high-level security properties for applets. In: Paradinas, P., Quisquater, J.J. (eds.) Proceedings of CARDIS 2004, Toulouse, France, Kluwer Academic Publishers, Dordrecht (2004)Google Scholar
  12. 12.
    Burdy, L., Requet, A., Lanet, J.L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)Google Scholar
  13. 13.
    Jones, C.: Systematic Software Development Using VDM. Prentice Hall, Englewood Cliffs (1990)zbMATHGoogle Scholar
  14. 14.
    Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects of Computing 11(5), 541–566 (1999)zbMATHCrossRefGoogle Scholar
  15. 15.
    Reynolds, J.C.: The craft of programming. Prentice Hall (1981); Out of print. Available as PDF from John Reynolds’ home pageGoogle Scholar
  16. 16.
    Beckert, B., Mostowski, W.: A program logic for handling java card’s transaction mechanism. In: Pezzé, M. (ed.) ETAPS 2003 and FASE 2003. LNCS, vol. 2621, pp. 246–260. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  17. 17.
    Leavens, G.T., et al.: Jml reference manualGoogle Scholar
  18. 18.
    Beckert, B., Schlager, S.: A sequent calculus for first-order dynamic logic with trace modalities. LNCS, vol. 2083, p. 626 (2001)Google Scholar
  19. 19.
    Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)Google Scholar
  20. 20.
    Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs i. Acta Inf. 6, 319–340 (1976)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Martin Hofmann
    • 1
  • Mariela Pavlova
    • 2
  1. 1.Institut für Informatik LMU MünchenGermany
  2. 2.Trusted Labs, Sophia-AntipolisFrance

Personalised recommendations