Advertisement

Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Automatic verification of Java programs with dynamic frames

Abstract

Framing in the presence of data abstraction is a challenging and important problem in the verification of object-oriented programs Leavens et al. (Formal Aspects Comput (FACS) 19:159–189, 2007). The dynamic frames approach is a promising solution to this problem. However, the approach is formalized in the context of an idealized logical framework. In particular, it is not clear the solution is suitable for use within a program verifier for a Java-like language based on verification condition generation and automated, first-order theorem proving. In this paper, we demonstrate that the dynamic frames approach can be integrated into an automatic verifier based on verification condition generation and automated theorem proving. The approach has been proven sound and has been implemented in a verifier prototype. The prototype has been used to prove correctness of several programming patterns considered challenging in related work.

This is a preview of subscription content, log in to check access.

References

  1. BBN08

    Banerjee A, Barnett M, Naumann DA (2008) Boogie meets regions: a verification experience report. In: VSTTE

  2. BCO05

    Berdine J, Calcagno C, O’Hearn PW (2005) Symbolic execution with separation logic. In: APLAS

  3. BDF+04

    Barnett M, DeLine R, Fahndrich M, Leino KRM, Schulte W (2004) Verification of object-oriented programs with invariants. J Obj Technol 3(6): 27–56

  4. BLS04

    Barnett M, Leino KRM, Schulte W (2004) The Spec# programming system: an overview. In CASSIS

  5. BMR95

    Borgida A, Mylopoulos J, Reiter R (1995) On the frame problem in procedure specifications. IEEE Trans Softw Eng (TSE), 21(10): 785–798

  6. BN04

    Barnett M, Naumann DA (2004) Friends need a bit more: maintaining invariants over shared state. In: Mathematics of program construction

  7. BNR08

    Banerjee A, Naumann DA, Rosenberg S (2008) Regional logic for local reasoning about global invariants. In: European Conference on Object-oriented Programming (ECOOP)

  8. BNSS04

    Barnett M, Naumann DA, Schulte W, Sun Qi (2004) 99.44% pure: useful abstractions in specifications. In: Formal techniques for Java-like programs (FTFJP)

  9. BPP03

    Bierman G, Parkinson M, Pitts A (2003) An imperative core calculus for Java and Java with effects. Technical report 563, University of Cambridge Computer Laboratory

  10. DE97

    Drossopoulou S, Eisenbach S (1997) The Java type system is sound—probably. In: European conference on object-oriented programming (ECOOP)

  11. DJOS08

    Dovland J, Johnsen EB, Owe O, Steffen M (2008) Lazy behavioral subtyping. In: Formal methods (FM), vol 5014

  12. DL07

    Darvas Á, Leino KRM (2007) Practical reasoning about invocations and implementations of pure methods. In: Fundamental approaches to software engineering (FASE)

  13. DM06

    Darvas Á, Müller P (2006) Reasoning about method calls in interface specifications. J Obj Technol (JOT) (in press)

  14. dMB08

    de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Conference on tools and algorithms for the construction and analysis of systems (TACAS)

  15. DP08

    Distefano D, Parkinson M (2008) jStar: towards practical verification for Java. In: Conference on object oriented programming: systems, languages, and applications (OOPSLA)

  16. IPW99

    Igarashi A, Pierce B, Wadler P (1999) Featherweight Java: a minimal core calculus for Java and J. In: Conference on object oriented programming: systems, languages, and applications (OOPSLA)

  17. JP07

    Jacobs B, Piessens F (2007) Inspector methods for state abstraction. J Obj Technol (JOT) 6(5): 13

  18. JP08

    Jacobs B, Piessens F (2008) The VeriFast program verifier. Technical report 520, Department of Computer Science, Katholieke Universiteit Leuven

  19. Kas06a

    Kassios YT (2006) Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Formal methods (FM)

  20. Kas06b

    Kassios YT (2006) A Theory of object oriented refinement, PhD thesis. University of Toronto

  21. Lea06

    Leavens GT (2006) JML’s rich, inherited specifications for behavioral subtypes. In: International conference on formal engineering methods (ICFEM)

  22. Lei98

    Leino KRM (1998) Data groups: specifying the modification of extended state. In: Conference on object oriented programming: systems, languages, and applications (OOPSLA)

  23. Lei08

    Leino KRM (2008) Specification and verification of object-oriented software. Marktoberdorf International Summer School—lecture notes

  24. LLM07

    Leavens GT, Leino KRM, Müller P (2007) Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput (FACS) 19(2): 159–189

  25. LM04

    Leino KRM, Müller P (2004) Object invariants in dynamic contexts. In: European conference on object-oriented programming (ECOOP)

  26. LM06

    Leino KRM, Müller P (2006) A verification methodology for model fields. In: European Symposium on Programming (ESOP)

  27. LM09

    Leino KRM, Middelkoop R (2009) Proving consistency of pure methods and model fields. In: Fundamental approaches to software engineering (FASE)

  28. LN02

    Leino KRM, Nelson G (2002) Data abstraction and information hiding. ACM Trans Progr Lang Syst (TOPLAS) 24(5): 491–553

  29. LPC+07

    Leavens GT, Poll E, Clifton C, Cheon Y, Ruby C, Cok D, Müller P, Kiniry J, Chalin P (2007) JML reference manual

  30. LPHZ02

    Leino KRM, Poetzsch-Heffter A, Zhou Y (2002) Using data groups to specify and check side effects. In: Conference on programming language design and implementation (PLDI)

  31. LS07

    Leino KRM, Schulte W (2007) Using history invariants to verify observers. In: European Symposium on Programming (ESOP)

  32. LW94

    Liskov BH, Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst (TOPLAS) 16(6): 1811–1841

  33. LW98

    Leavens GT, Wing JM (1998) Protective interface specifications. Formal Aspects Comput (FACS) 10(1): 59–75

  34. Mül02

    Müller P (2002) Modular specification and verification of object-oriented programs, Lecture Notes in Computer Science, volume 2262. Springer, Berlin

  35. Par05

    Parkinson M (2005) Local Reasoning for Java. PhD thesis, University of Cambridge, Cambridge

  36. Par07

    Parkinson M (2007) Class invariants: The end of the road? In: International workshop on aliasing, confinement and ownership in object-oriented programming (IWACO)

  37. PB05

    Parkinson M, Bierman G (2005) Separation logic and abstraction. In: Principles of programming languages (POPL)

  38. PB08

    Parkinson M, Bierman G (2008) Separation logic, abstraction and inheritance. In: Principles of programming languages (POPL)

  39. RADM08

    Rudich A, Darvas Á, Müller P (2008) Checking well-formedness of pure-method specifications. In: Formal methods (FM)

  40. Rey02

    Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Symposium on logic in Computer Science (LICS)

  41. SDM09

    Summers AJ, Drossopoulou S, Müller P (2009) The need for flexible object invariants. In: International workshop on aliasing, confinement and ownership in object-oriented programming (IWACO)

  42. SJP08

    Smans J, Jacobs B, Piessens F (2008) Implicit dynamic frames. In: Formal techniques for Java-like programs (FTFJP)

  43. SJP09

    Smans J, Jacobs B, Piessens F (2009) Implicit dynamic frames: combining dynamic frames and separation logic. In: European conference on object-oriented programming (ECOOP)

  44. SJPS08

    Smans J, Jacobs B, Piessens F, Schulte W (2008) An automatic verifier for Java-like programs based on dynamic frames. In: Fundamental approaches to software engineering (FASE)

Download references

Author information

Correspondence to Jan Smans.

Additional information

J.L. Fiadeiro, P. Inverardi and T.S.E. Maibaum

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Smans, J., Jacobs, B., Piessens, F. et al. Automatic verification of Java programs with dynamic frames. Form Asp Comp 22, 423–457 (2010). https://doi.org/10.1007/s00165-010-0148-1

Download citation

Keywords

  • Program verification
  • Dynamic frames
  • Frame problem
  • Data abstraction