Automatic verification of Java programs with dynamic frames
Tóm tắt
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.
Từ khóa
Tài liệu tham khảo
Banerjee A Barnett M Naumann DA (2008) Boogie meets regions: a verification experience report. In: VSTTE
Barnett M Naumann DA (2004) Friends need a bit more: maintaining invariants over shared state. In: Mathematics of program construction
Banerjee A Naumann DA Rosenberg S (2008) Regional logic for local reasoning about global invariants. In: European Conference on Object-oriented Programming (ECOOP)
Barnett M Naumann DA Schulte W Sun Qi (2004) 99.44% pure: useful abstractions in specifications. In: Formal techniques for Java-like programs (FTFJP)
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
Drossopoulou S Eisenbach S (1997) The Java type system is sound—probably. In: European conference on object-oriented programming (ECOOP)
Dovland J Johnsen EB Owe O Steffen M (2008) Lazy behavioral subtyping. In: Formal methods (FM) vol 5014
Darvas Á Leino KRM (2007) Practical reasoning about invocations and implementations of pure methods. In: Fundamental approaches to software engineering (FASE)
Darvas Á Müller P (2006) Reasoning about method calls in interface specifications. J Obj Technol (JOT) (in press)
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)
Distefano D Parkinson M (2008) jStar: towards practical verification for Java. In: Conference on object oriented programming: systems languages and applications (OOPSLA)
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)
Jacobs B, 2007, Inspector methods for state abstraction, J Obj Technol (JOT), 6, 13
Jacobs B Piessens F (2008) The VeriFast program verifier. Technical report 520 Department of Computer Science Katholieke Universiteit Leuven
Kassios YT (2006) Dynamic frames: support for framing dependencies and sharing without restrictions. In: Formal methods (FM)
Kassios YT (2006) A Theory of object oriented refinement PhD thesis. University of Toronto
Leavens GT (2006) JML’s rich inherited specifications for behavioral subtypes. In: International conference on formal engineering methods (ICFEM)
Leino KRM (1998) Data groups: specifying the modification of extended state. In: Conference on object oriented programming: systems languages and applications (OOPSLA)
Leino KRM (2008) Specification and verification of object-oriented software. Marktoberdorf International Summer School—lecture notes
Leino KRM Müller P (2004) Object invariants in dynamic contexts. In: European conference on object-oriented programming (ECOOP)
Leino KRM Müller P (2006) A verification methodology for model fields. In: European Symposium on Programming (ESOP)
Leino KRM Middelkoop R (2009) Proving consistency of pure methods and model fields. In: Fundamental approaches to software engineering (FASE)
Leavens GT Poll E Clifton C Cheon Y Ruby C Cok D Müller P Kiniry J Chalin P (2007) JML reference manual
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)
Leino KRM Schulte W (2007) Using history invariants to verify observers. In: European Symposium on Programming (ESOP)
Müller P (2002) Modular specification and verification of object-oriented programs Lecture Notes in Computer Science volume 2262. Springer Berlin
Parkinson M (2005) Local Reasoning for Java. PhD thesis University of Cambridge Cambridge
Parkinson M (2007) Class invariants: The end of the road? In: International workshop on aliasing confinement and ownership in object-oriented programming (IWACO)
Parkinson M Bierman G (2005) Separation logic and abstraction. In: Principles of programming languages (POPL)
Parkinson M Bierman G (2008) Separation logic abstraction and inheritance. In: Principles of programming languages (POPL)
Rudich A Darvas Á Müller P (2008) Checking well-formedness of pure-method specifications. In: Formal methods (FM)
Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Symposium on logic in Computer Science (LICS)
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)
Smans J Jacobs B Piessens F (2008) Implicit dynamic frames. In: Formal techniques for Java-like programs (FTFJP)
Smans J Jacobs B Piessens F (2009) Implicit dynamic frames: combining dynamic frames and separation logic. In: European conference on object-oriented programming (ECOOP)