Boogie Meets Regions: A Verification Experience Report

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. 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)

   Chapter  Google Scholar 

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. Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: ECOOP (2008)

   Google Scholar 

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. 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. Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE (2005)

   Google Scholar 

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. 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)

   Chapter  Google Scholar 

10. Bierman, G., Parkinson, M.: Separation logic and abstraction. In: POPL, pp. 247–258 (2005)

    Google Scholar 

11. Darvas, Á., Müller, P.: Reasoning about method calls in interface specifications. Journal of Object Technology 5(5), 59–85 (2006)

    Google Scholar 

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)

    Chapter  Google Scholar 

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. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)

    Article  MathSciNet  Google Scholar 

15. Hehner, E.C.R.: Predicative programming part I. Commun. ACM 27, 134–143 (1984)

    Article  MATH  MathSciNet  Google Scholar 

16. Hoare, C.A.R.: Proofs of correctness of data representations. Acta Inf 1, 271–281 (1972)

    Article  MATH  Google Scholar 

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)

    Chapter  Google Scholar 

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. Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)

    MATH  Google Scholar 

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. O’Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: POPL, pp. 268–280 (2004)

    Google Scholar 

22. Parkinson, M.: Class invariants: the end of the road. In: International Workshop on Aliasing, Confinement and Ownership (2007)

    Google Scholar 

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. 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)

    Chapter  Google Scholar 

Download references