Automatic verification of Java programs with dynamic frames
Tóm tắt
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)