Advertisement

Boogie Meets Regions: A Verification Experience Report

  • Anindya Banerjee
  • Mike Barnett
  • David A. Naumann
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)

Abstract

We use region logic specifications to verify several programs exhbiting the classic hard problem for object-oriented systems: the framing of heap updates. We use BoogiePL and its associated SMT solver, Z3, to prove both implementations and client code.

Keywords

Experience Report Proof Obligation Separation Logic Region Logic Dynamic Frame 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: POPL, Extended version available as KSU CIS-TR-2005-1 (2006)Google Scholar
  2. 2.
    Amtoft, T., Hatcliff, J., Rodriguez, E., Robby, H.J., Greve, D.: Specification and checking of software contracts for conditional information flow. In: Cuellar, J., Maibaum, T.S.E. (eds.) FM 2008. LNCS, vol. 5014. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  3. 3.
    Banerjee, A., Barnett, M., Naumann, D.A.: Boogie meets regions: a verification experience report (extended version). Technical Report MSR-TR-2008-79, Microsoft Research (2008)Google Scholar
  4. 4.
    Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: ECOOP (2008)Google Scholar
  5. 5.
    Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)Google Scholar
  6. 6.
    Barnett, M., De Line, R., Jacobs, B., Fähndrich, M., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# programming system: Challenges and directions. In: Verified Software: Theories, Tools, and Experiments (VSTTE) (2005)Google Scholar
  7. 7.
    Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE (2005)Google Scholar
  8. 8.
    Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)Google Scholar
  9. 9.
    Beckert, B., Trentelman, K.: Second-order principles in specification languages for object-oriented programs. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 154–168. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    Bierman, G., Parkinson, M.: Separation logic and abstraction. In: POPL, pp. 247–258 (2005)Google Scholar
  11. 11.
    Darvas, Á., Müller, P.: Reasoning about method calls in interface specifications. Journal of Object Technology 5(5), 59–85 (2006)Google Scholar
  12. 12.
    de Moura, L., Bjørner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183–198. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    De Line, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (March 2005)Google Scholar
  14. 14.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)CrossRefMathSciNetGoogle Scholar
  15. 15.
    Hehner, E.C.R.: Predicative programming part I. Commun. ACM 27, 134–143 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Hoare, C.A.R.: Proofs of correctness of data representations. Acta Inf 1, 271–281 (1972)zbMATHCrossRefGoogle Scholar
  17. 17.
    Kassios, I.T.: Dynamic framing: Support for framing, dependencies and sharing without restriction. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Leavens, G.T., Naumann, D.A., Rosenberg, S.: Preliminary definition of core JML. Technical Report CS Report 2006-07, Stevens Institute of Technology (2006)Google Scholar
  19. 19.
    Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  20. 20.
    Naumann, D.A.: An admissible second order frame rule in region logic. Technical Report CS Report 2008-02, Stevens Institute of Technology (2008)Google Scholar
  21. 21.
    O’Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: POPL, pp. 268–280 (2004)Google Scholar
  22. 22.
    Parkinson, M.: Class invariants: the end of the road. In: International Workshop on Aliasing, Confinement and Ownership (2007)Google Scholar
  23. 23.
    Schulte, W.: Building a verifying compiler for C. Presentation at Dagstuhl Seminar 08061 for Types, Logics and Semantics of State (2008)Google Scholar
  24. 24.
    Smans, J., Jacobs, B., Piessens, F., Schulte, W.: An automatic verifier for Java-like programs based on dynamic frames. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Anindya Banerjee
    • 1
  • Mike Barnett
    • 2
  • David A. Naumann
    • 3
  1. 1.Kansas State UniversityManhattanUSA
  2. 2.Microsoft ResearchRedmondUSA
  3. 3.Stevens Institute of TechnologyHobokenUSA

Personalised recommendations