{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:30:46Z","timestamp":1707521446562},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2010,5,1]],"date-time":"2010-05-01T00:00:00Z","timestamp":1272672000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2010,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Framing in the presence of data abstraction is a challenging and important problem in the verification of object-oriented programs Leavens et\u00a0al. (Formal Aspects Comput (FACS) 19:159\u2013189, 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.<\/jats:p>","DOI":"10.1007\/s00165-010-0148-1","type":"journal-article","created":{"date-parts":[[2010,2,19]],"date-time":"2010-02-19T14:48:29Z","timestamp":1266590909000},"page":"423-457","source":"Crossref","is-referenced-by-count":7,"title":["Automatic verification of Java programs with dynamic frames"],"prefix":"10.1145","volume":"22","author":[{"given":"Jan","family":"Smans","sequence":"first","affiliation":[{"name":"Katholieke Universiteit, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[{"name":"Katholieke Universiteit, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[{"name":"Katholieke Universiteit, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfram","family":"Schulte","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Banerjee A Barnett M Naumann DA (2008) Boogie meets regions: a verification experience report. In: VSTTE"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Berdine J Calcagno C O\u2019Hearn PW (2005) Symbolic execution with separation logic. In: APLAS","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Barnett M Leino KRM Schulte W (2004) The Spec# programming system: an overview. In CASSIS","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.469460"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Barnett M Naumann DA (2004) Friends need a bit more: maintaining invariants over shared state. In: Mathematics of program construction","DOI":"10.1007\/978-3-540-27764-4_5"},{"key":"e_1_2_1_2_7_2","unstructured":"Banerjee A Naumann DA Rosenberg S (2008) Regional logic for local reasoning about global invariants. In: European Conference on Object-oriented Programming (ECOOP)"},{"key":"e_1_2_1_2_8_2","unstructured":"Barnett M Naumann DA Schulte W Sun Qi (2004) 99.44% pure: useful abstractions in specifications. In: Formal techniques for Java-like programs (FTFJP)"},{"key":"e_1_2_1_2_9_2","unstructured":"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"},{"key":"e_1_2_1_2_10_2","unstructured":"Drossopoulou S Eisenbach S (1997) The Java type system is sound\u2014probably. In: European conference on object-oriented programming (ECOOP)"},{"key":"e_1_2_1_2_11_2","unstructured":"Dovland J Johnsen EB Owe O Steffen M (2008) Lazy behavioral subtyping. In: Formal methods (FM) vol 5014"},{"key":"e_1_2_1_2_12_2","unstructured":"Darvas \u00c1 Leino KRM (2007) Practical reasoning about invocations and implementations of pure methods. In: Fundamental approaches to software engineering (FASE)"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Darvas \u00c1 M\u00fcller P (2006) Reasoning about method calls in interface specifications. J Obj Technol (JOT) (in press)","DOI":"10.5381\/jot.2006.5.5.a3"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"de Moura L Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Conference on tools and algorithms for the construction and analysis of systems (TACAS)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Distefano D Parkinson M (2008) jStar: towards practical verification for Java. In: Conference on object oriented programming: systems languages and applications (OOPSLA)","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/320384.320395"},{"issue":"5","key":"e_1_2_1_2_17_2","first-page":"13","article-title":"Inspector methods for state abstraction","volume":"6","author":"Jacobs B","year":"2007","journal-title":"J Obj Technol (JOT)"},{"key":"e_1_2_1_2_18_2","unstructured":"Jacobs B Piessens F (2008) The VeriFast program verifier. Technical report 520 Department of Computer Science Katholieke Universiteit Leuven"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Kassios YT (2006) Dynamic frames: support for framing dependencies and sharing without restrictions. In: Formal methods (FM)","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_1_2_20_2","unstructured":"Kassios YT (2006) A Theory of object oriented refinement PhD thesis. University of Toronto"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Leavens GT (2006) JML\u2019s rich inherited specifications for behavioral subtypes. In: International conference on formal engineering methods (ICFEM)","DOI":"10.1007\/11901433_2"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Leino KRM (1998) Data groups: specifying the modification of extended state. In: Conference on object oriented programming: systems languages and applications (OOPSLA)","DOI":"10.1145\/286936.286953"},{"key":"e_1_2_1_2_23_2","unstructured":"Leino KRM (2008) Specification and verification of object-oriented software. Marktoberdorf International Summer School\u2014lecture notes"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0026-7"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Leino KRM M\u00fcller P (2004) Object invariants in dynamic contexts. In: European conference on object-oriented programming (ECOOP)","DOI":"10.1007\/978-3-540-24851-4_22"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Leino KRM M\u00fcller P (2006) A verification methodology for model fields. In: European Symposium on Programming (ESOP)","DOI":"10.1007\/11693024_9"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Leino KRM Middelkoop R (2009) Proving consistency of pure methods and model fields. In: Fundamental approaches to software engineering (FASE)","DOI":"10.1007\/978-3-642-00593-0_16"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_1_2_29_2","unstructured":"Leavens GT Poll E Clifton C Cheon Y Ruby C Cok D M\u00fcller P Kiniry J Chalin P (2007) JML reference manual"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/512529.512559"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Leino KRM Schulte W (2007) Using history invariants to verify observers. In: European Symposium on Programming (ESOP)","DOI":"10.1007\/978-3-540-71316-6_7"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/PL00003926"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"M\u00fcller P (2002) Modular specification and verification of object-oriented programs Lecture Notes in Computer Science volume 2262. Springer Berlin","DOI":"10.1007\/3-540-45651-1"},{"key":"e_1_2_1_2_35_2","unstructured":"Parkinson M (2005) Local Reasoning for Java. PhD thesis University of Cambridge Cambridge"},{"key":"e_1_2_1_2_36_2","unstructured":"Parkinson M (2007) Class invariants: The end of the road? In: International workshop on aliasing confinement and ownership in object-oriented programming (IWACO)"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Parkinson M Bierman G (2005) Separation logic and abstraction. In: Principles of programming languages (POPL)","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Parkinson M Bierman G (2008) Separation logic abstraction and inheritance. In: Principles of programming languages (POPL)","DOI":"10.1145\/1328438.1328451"},{"key":"e_1_2_1_2_39_2","unstructured":"Rudich A Darvas \u00c1 M\u00fcller P (2008) Checking well-formedness of pure-method specifications. In: Formal methods (FM)"},{"key":"e_1_2_1_2_40_2","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Symposium on logic in Computer Science (LICS)"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Summers AJ Drossopoulou S M\u00fcller P (2009) The need for flexible object invariants. In: International workshop on aliasing confinement and ownership in object-oriented programming (IWACO)","DOI":"10.1145\/1562154.1562160"},{"key":"e_1_2_1_2_42_2","unstructured":"Smans J Jacobs B Piessens F (2008) Implicit dynamic frames. In: Formal techniques for Java-like programs (FTFJP)"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Smans J Jacobs B Piessens F (2009) Implicit dynamic frames: combining dynamic frames and separation logic. In: European conference on object-oriented programming (ECOOP)","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/978-3-540-78743-3_19"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-010-0148-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-010-0148-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-010-0148-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:52:28Z","timestamp":1641484348000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-010-0148-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["10.1007\/s00165-010-0148-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-010-0148-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5]]}}}