{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T09:22:51Z","timestamp":1790932971429,"version":"4.1.0"},"reference-count":123,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:00:00Z","timestamp":1180656000000},"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":[[2007,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>The state of knowledge in how to specify sequential programs in object-oriented languages such as Java and C# and the state of the art in automated verification tools for such programs have made measurable progress in the last several years. This paper describes several remaining challenges and approaches to their solution.<\/jats:p>","DOI":"10.1007\/s00165-007-0026-7","type":"journal-article","created":{"date-parts":[[2007,4,5]],"date-time":"2007-04-05T09:50:27Z","timestamp":1175766627000},"page":"159-189","source":"Crossref","is-referenced-by-count":81,"title":["Specification and verification challenges for sequential object-oriented programs"],"prefix":"10.1145","volume":"19","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[{"name":"Dept. of Computer Science, Iowa State University, 229 Atanasoff Hall, 50011, Ames, IA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, One Microsoft Way, 98052, Redmond, WA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, ETH Zentrum RZ F2, 8092, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"issue":"3","key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/390017.808306","article-title":"GYPSY: a language for specification and implementation of verifiable programs","volume":"12","author":"Ambler AL","year":"1977","journal-title":"SIGPLAN Notices"},{"key":"e_1_2_1_2_3_2","first-page":"682","volume-title":"Theory and practice of software development (TAPSOFT), Vol 1214 of Lecture Notes in Computer Science","author":"Abadi M","year":"1997"},{"key":"e_1_2_1_2_4_2","first-page":"60","volume-title":"Foundations of object-oriented languages. REX School\/Workshop, Noordwijkerhout, The Netherlands, May\/June 1990, Vol 489 of Lecture Notes in Computer Science.","author":"America P","year":"1991"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Ball T Bounimova E Cook B Levin V Lichtenberg J McGarvey C Ondrusek B Rajamani SK Ustuner A (2006) Thorough static analysis of device drivers. In: EuroSys\u201906. ACM New York pp 73\u201385. doi:10.1145\/1217935.1217943","DOI":"10.1145\/1218063.1217943"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_2_8_2","first-page":"364","volume-title":"In: Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures, Vol 4111 of Lecture Notes in Computer Science","author":"Barnett M","year":"2006"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_2_10_2","unstructured":"Beckert B (2000) A dynamic logic for Java Card. In: Drossopoulou S Eisenbach S Jacobs B Leavens GT M\u00fcller P Poetzsch-Heffter A (eds) Workshop on formal techniques for Java Programs (FTfJP). Technical Report 269 FernUniversit\u00e4t Hagen"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11575467_24","volume-title":"Programming languages and systems: third Asian symposium (APLAS), Vol 3780 of Lecture Notes in Computer Science","author":"Benton N","year":"2005"},{"key":"e_1_2_1_2_12_2","first-page":"82","volume-title":"Program analysis for software tools and engineering (PASTE).","author":"Barnett M","year":"2005"},{"key":"e_1_2_1_2_13_2","first-page":"49","volume-title":"Construction and analysis of safe, secure, and interoperable smart devices (CASSIS 2004), Vol 3362 of Lecture Notes in Computer Science","author":"Barnett M","year":"2005"},{"key":"e_1_2_1_2_14_2","first-page":"255","volume-title":"Bytecode semantics, verification, analysis and transformation (BYTECODE), Vol 141(1) of Electronic Notes in Theoretical Computer Science","author":"Bannwart F","year":"2005"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.469460"},{"key":"e_1_2_1_2_16_2","first-page":"54","volume-title":"Mathematics of program construction (MPC), Vol 3125 of Lecture Notes in Computer Science","author":"Barnett M","year":"2004"},{"key":"e_1_2_1_2_17_2","first-page":"135","volume-title":"Foundations of software science and computation structures (FOSSACS), Vol 1578 of Lecture Notes in Computer Science","author":"Boer FSd","year":"1999"},{"key":"e_1_2_1_2_18_2","first-page":"422","volume-title":"Formal methods (FME), Vol 2805 of Lecture Notes in Computer Science","author":"Burdy L","year":"2003"},{"key":"e_1_2_1_2_19_2","unstructured":"Beckert B Sasse B (2001) Handling Java\u2019s abrupt termination in a sequent calculus for Dynamic Logic. In: Beckert B France R H\u00e4hnle R Jacobs B (eds) IJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development pp 5\u201314"},{"key":"e_1_2_1_2_20_2","unstructured":"B\u00fcchi M (2000) Safe language mechanisms for modularization and concurrency. Technical Report TUCS Dissertations No. 28 Turku Center for Computer Science May 2000"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/551462"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625280"},{"key":"e_1_2_1_2_23_2","unstructured":"B\u00fcchi M Weck W (1999) The greybox approach: when blackbox specifications hide too much. Technical Report 297 Turku Center for Computer Science August 1999. http:\/\/tinyurl.com\/ywmuzy."},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Clarke DG Drossopoulou S (2002) Ownership encapsulation and the disjointness of type and effect. In: Object-oriented programming systems languages and applications (OOPSLA) Vol 37(11) of SIGPLAN Notices. ACM New York pp 292\u2013310. doi:10.1145\/582419.582447","DOI":"10.1145\/583854.582447"},{"issue":"4","key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1145\/369264.369270","article-title":"Industrial experience with SPARK","volume":"20","author":"Chapman R","year":"2000","journal-title":"ACM SIGADA Ada Lett"},{"key":"e_1_2_1_2_26_2","first-page":"440","volume-title":"Formal methods (FME), Vol 2805 of Lecture Notes in Computer Science","author":"Chalin P","year":"2003"},{"key":"e_1_2_1_2_27_2","unstructured":"Charles J (2006) Adding native specifications to JML. In: Workshop on formal techniques for Java-like Programs (FTfJP) July 2006. http:\/\/www.disi.unige.it\/person\/AnconaD\/FTfJP06\/paper04.pdf"},{"key":"e_1_2_1_2_28_2","unstructured":"Cheon Y (2003) A runtime assertion checker for the Java Modeling Language. PhD dissertation Technical Report 03-09 Department of Computer Science Iowa State University April 2003. ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR03-09\/TR.pdf"},{"key":"e_1_2_1_2_29_2","unstructured":"Cheon Y Hayashi Y Leavens GT (2004) A thought on specification reflection. In: Callaos N Lesso W Sanchez B (eds) The 8th World multi-conference on systemics cybernetics and informatics (SCI) Vol II Computing Techniques pp 485\u2013490"},{"key":"e_1_2_1_2_30_2","first-page":"108","volume-title":"Construction and analysis of safe, secure, and interoperable smart devices (CASSIS 2004), Vol 3362 of Lecture Notes in Computer Science","author":"Cok DR","year":"2005"},{"key":"e_1_2_1_2_31_2","first-page":"296","volume-title":"Computer aided verification (CAV), Vol 3576 of Lecture Notes in Computer Science","author":"Cook B","year":"2005"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.649"},{"issue":"2","key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1016\/S0304-3975(02)00868-X","article-title":"Program logic and equivalence in the presence of garbage collection","volume":"298","author":"Calcagno C","year":"2003","journal-title":"Theor Comput Sci"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/91408"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2005.4.8.a4"},{"key":"e_1_2_1_2_36_2","first-page":"48","volume-title":"In: Object-oriented programming systems, languages, and applications (OOPSLA), Vol 33(10) of SIGPLAN Notices","author":"Clarke DG","year":"1998"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1145\/1133981.1134029","volume-title":"Proceedings of the ACM SIGPLAN 2006 conference on programming language design and implementation (PLDI)","author":"Cook B","year":"2006"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010218"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Dhara KK Leavens GT (1996) Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th international conference on software engineering March 1996 Berlin. IEEE Computer Society Press New York pp 258\u2013267. A corrected version is ISU CS TR #95-20c http:\/\/tinyurl.com\/s2krg. doi:10.1109\/ICSE.1996.493421","DOI":"10.1109\/ICSE.1996.493421"},{"key":"e_1_2_1_2_40_2","unstructured":"DeLine R Leino KRM (2005) Boogie PL: aA typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70 Microsoft Research. ftp:\/\/ftp.research.microsoft.com\/pub\/tr\/TR-2005-70.pdf"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2006.5.5.a3"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_2_1_2_44_2","unstructured":"C# language specification. ECMA Standard 334 June 2005"},{"key":"e_1_2_1_2_45_2","unstructured":"Eiffel analysis design and programming language. ECMA Standard 367 June 2005"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of algebraic specification 1: equations and initial semantics, Vol 6 of EATCS Monographs on Theoretical Computer Science","author":"Ehrig H","year":"1985"},{"key":"e_1_2_1_2_47_2","volume-title":"Formal specification and design, Vol 35 of Cambridge Tracts in Theoretical Computer Science","author":"Feijs LMG","year":"1992"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Flanagan C Leino KRM (2001) Houdini an annotation assistant for ESC\/Java. In: Oliveira JN Zave P (eds) FME 2001: formal methods for increasing software productivity Vol 2021 of Lecture Notes in Computer Science. Springer Heidelberg pp 500\u2013517. http:\/\/www.springerlink.com\/content\/nxukfdgg7623q3a9","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Flanagan C Leino KRM Lillibridge M Nelson G Saxe JB Stata R (2002) Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN conference on programming language design and implementation (PLDI) Vol 37(5) of SIGPLAN Notices. ACM New York pp 234\u2013245. doi:10.1145\/512529.512558","DOI":"10.1145\/543552.512558"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J-C March\u00e9 C (2004) Multi-prover verification of C programs. In: Formal methods and software engineering 6th international conference on formal engineering methods ICFEM 2004 Vol 3308 of Lecture Notes in Computer Science. Springer Heidelberg pp 15\u201329. http:\/\/www.springerlink.com\/content\/ejxv14xdjf5676u5","DOI":"10.1007\/978-3-540-30482-1_10"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Greenhouse A Boyland J (1999) An object-oriented effects system. In: European conference on object-oriented programming (ECOOP). Springer Heidelberg pp 205\u2013229. http:\/\/www.springerlink.com\/content\/tu309p114v1kbd8v","DOI":"10.1007\/3-540-48743-3_10"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00260922"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.5555\/151155"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.5555\/186897"},{"key":"e_1_2_1_2_55_2","unstructured":"Greenhouse A (2003) A programmer-oriented approach to safe concurrency. Technical Report CMU-CS-03-135 School of Computer Science Carnegie Mellon University May 2003. http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/2003\/CMU-CS-03-135.pdf"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"e_1_2_1_2_57_2","volume-title":"A logical approach to discrete math. texts and monographs in computer science","author":"Gries D","year":"1994"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8596-5","volume-title":"A practical theory of programming. texts and monographs in computer science","author":"Hehner ECR","year":"1993"},{"key":"e_1_2_1_2_60_2","unstructured":"Hehner ECR (2005) Specified blocks. Verified Software: Theories Tools Experiments (VSTTE) http:\/\/vstte.inf.ethz.ch\/Files\/ hehner.pdf October 2005"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Huisman M Jacobs B (2000) Java program verification via a Hoare logic with abrupt termination. In: Fundamental approaches to software engineering (FASE). Springer Heidelberg pp 284\u2013303. http:\/\/www.springerlink.com\/content\/fkrbjn1vg56ra052","DOI":"10.1007\/3-540-46428-X_20"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"Hudak P Jones SP Wadler P Boutel B Fairbairn J Fasel J Guzm\u00e1n MM Hammond K Hughes J Johnsson T Kieburtz D Nikhil R Partain W Peterson J (1992) Report on the programming language Haskell: a non-strict purely functional language version 1.2. ACM SIGPLAN Notices 27(5). doi:10.1145\/130697.130699","DOI":"10.1145\/130697.130699"},{"key":"e_1_2_1_2_63_2","unstructured":"Hoare T Misra J Shankar N (2005) Verified software: theories tools experiments (VSTTE 2005). http:\/\/vstte.ethz.ch October 2005. Sponsored by International Federation for Information Processing Technical Committee 2"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_2_1_2_67_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2003.07.005"},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","unstructured":"Jacobs B Kiniry J Warnier M (2003) Java program verification challenges. In: de Boer FS Bonsangue MM Graf S de Roever W-P (eds) FMCO 2002: formal methods for component objects proceedings Vol 2852 of Lecture Notes in Computer Science. Springer Heidelberg pp 202\u2013219","DOI":"10.1007\/978-3-540-39656-7_8"},{"key":"e_1_2_1_2_69_2","unstructured":"Jacobs B Meijer E Piessens F Schulte W (2005) Iterators revisited: proof rules and implementation. In: Workshop on formal techniques for Java-like Programs (FTfJP) July 2005. http:\/\/www.cs.ru.nl\/ftfjp\/2005\/Jacobs.pdf"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"publisher","DOI":"10.5555\/94062"},{"key":"e_1_2_1_2_71_2","unstructured":"Jones KD (1991) LM3: A larch interface language for Modula-3: a definition and introduction: Version 1.0. Technical Report 72 Digital Equipment Corporation Systems Research Center"},{"key":"e_1_2_1_2_72_2","doi-asserted-by":"crossref","unstructured":"Jacobs B Poll E (2001) A logic for the Java modeling language JML. In: Fundamental approaches to software engineering (FASE) Vol 2029 of Lecture Notes in Computer Science. Springer Heidelberg pp 284\u2013299. http:\/\/www.springerlink.com\/content\/17ul9mb1y0ja42eb","DOI":"10.1007\/3-540-45314-8_21"},{"key":"e_1_2_1_2_73_2","unstructured":"Jacobs B Piessens F (2006) Verification of programs with inspector methods. In: Workshop on Formal Techniques for Java-like Programs (FTfJP) July 2006. http:\/\/www.disi.unige.it\/person\/AnconaD\/FTfJP06\/paper09.pdf"},{"issue":"7","key":"e_1_2_1_2_74_2","first-page":"35","article-title":"Improving Eiffel assertions using quantified iterators","volume":"10","author":"Katrib M","year":"1997","journal-title":"J Object-Oriented Program"},{"key":"e_1_2_1_2_75_2","doi-asserted-by":"crossref","unstructured":"Kramer R (1998) iContract\u2014the Java TM design by contract TM tool. In: TOOLS 26: technology of object-oriented languages and systems August 1998. IEEE Computer Society Press New York pp 295\u2013307. doi:10.1109\/TOOLS.1998.711021","DOI":"10.1109\/TOOLS.1998.711021"},{"key":"e_1_2_1_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"e_1_2_1_2_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_2_78_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.015"},{"key":"e_1_2_1_2_79_2","first-page":"113","volume-title":"Foundations of component-based systems, Chap 6.","author":"Leavens GT","year":"2000"},{"key":"e_1_2_1_2_80_2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/11901433_2","volume-title":"Formal methods and software engineering: 8th international conference on formal engineering methods (ICFEM), Vol 4260 of Lecture Notes in Computer Science, New York.","author":"Leavens GT","year":"2006"},{"key":"e_1_2_1_2_81_2","unstructured":"Leino KRM (1995) Toward reliable modular programs. PhD Thesis California Institute of Technology. Available as Technical Report Caltech-CS-TR-95-03. http:\/\/caltechcstr.library.caltech.edu\/234\/00\/95-03.ps"},{"key":"e_1_2_1_2_82_2","unstructured":"Leino KRM (1997) Ecstatic: an object-oriented programming language with an axiomatic semantics. In: Pierce B (ed) Fourth international workshop on foundations of object-oriented languages (FOOL) January 1997. Available from: http:\/\/www.cis.upenn.edu\/ bcpierce\/FOOL\/"},{"key":"e_1_2_1_2_83_2","doi-asserted-by":"crossref","unstructured":"Leino KRM (1998) Data groups: specifying the modification of extended state. In: Object-oriented programming systems languages and applications (OOPSLA) Vol 33(10) of SIGPLAN Notices. ACM New York pp 144\u2013153. doi:10.1145\/286936.286953","DOI":"10.1145\/286942.286953"},{"key":"e_1_2_1_2_84_2","first-page":"491","volume-title":"European conference on object- oriented programming (ECOOP), Vol 3086 of Lecture Notes in Computer Science, June 2004","author":"Leino KRM","year":"2004"},{"key":"e_1_2_1_2_85_2","first-page":"26","volume-title":"Formal methods (FM), Vol 3582 of Lecture Notes in Computer Science, July 2005","author":"Leino KRM","year":"2005"},{"key":"e_1_2_1_2_86_2","first-page":"115","volume-title":"European symposium on programming (ESOP), Vol 3924 of Lecture Notes in Computer Science, March 2006.","author":"Leino KRM","year":"2006"},{"key":"e_1_2_1_2_87_2","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_1_2_88_2","unstructured":"Leavens GT Naumann DA (2006) Behavioral subtyping specification inheritance and modular reasoning. Technical Report 06-20a Department of Computer Science Iowa State University Ames August 2006. ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR06-20\/TR.pdf"},{"key":"e_1_2_1_2_89_2","unstructured":"Leavens GT Poll E Clifton C Cheon Y Ruby C Cok DR M\u00fcller P Kiniry J Chalin P (2006) JML reference manual. Department of Computer Science Iowa State University. Available from http:\/\/www.jmlspecs.org January 2006"},{"key":"#cr-split#-e_1_2_1_2_90_2.1","doi-asserted-by":"crossref","unstructured":"Leino KRM Poetzsch-Heffter A Zhou Y (2002) Using data groups to specify and check side effects. In: Proceedings of the 2002 ACM SIGPLAN conference on programming language design and implementation (PLDI) Vol 37","DOI":"10.1145\/512529.512559"},{"key":"#cr-split#-e_1_2_1_2_90_2.2","doi-asserted-by":"crossref","unstructured":"(5) of SIGPLAN Notices May 2002. ACM New York pp 246-257. doi:10.1145\/512529.512559","DOI":"10.1145\/512529.512559"},{"key":"e_1_2_1_2_91_2","unstructured":"Leino KRM Saxe JB Stata R (1999) Checking Java programs via guarded commands. In: Jacobs B Leavens GT M\u00fcller P Poetzsch-Heffter A (eds) Formal techniques for Java Programs (FTfJP) Technical Report 251. FernUniversit\u00e4t Hagen May 1999. Also available as Technical Note 1999-002 Compaq Systems Research Center"},{"key":"e_1_2_1_2_92_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-9685-7","volume-title":"Programming with specifications: an introduction to Anna, a language for specifying Ada programs. Texts and Monographs in Computer Science","author":"Luckham D","year":"1990"},{"key":"e_1_2_1_2_93_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.230345"},{"key":"e_1_2_1_2_94_2","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_2_95_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178658"},{"key":"e_1_2_1_2_96_2","doi-asserted-by":"publisher","DOI":"10.5555\/129093"},{"key":"e_1_2_1_2_97_2","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_2_1_2_98_2","unstructured":"Miragliotta M (2004) Specification model library for the interactive program prover Jive . Student project ETH Zurich. Available from: http:\/\/www.sct.inf.ethz.ch\/projects\/student_docs\/Marcello_Miragliotta\/M arcello_Miragliotta_paper.pdf"},{"key":"e_1_2_1_2_99_2","volume-title":"Programming from specifications","author":"Morgan C","year":"1994","edition":"2"},{"key":"e_1_2_1_2_100_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.713"},{"key":"e_1_2_1_2_101_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"e_1_2_1_2_102_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2003.07.006"},{"key":"e_1_2_1_2_103_2","volume-title":"Modular specification and verification of object-oriented programs, Vol 2262 of Lecture Notes in Computer Science","author":"M\u00fcller P","year":"2002"},{"key":"e_1_2_1_2_104_2","doi-asserted-by":"crossref","unstructured":"Nimmer JW Ernst MD (2001) Static verification of dynamically detected program invariants: integrating Daikon and ESC\/Java. In: Proceedings of RV\u201901 first workshop on runtime verification July 2001. Elsevier Amsterdam. doi:10.1016\/S1571-0661(04)00256-7","DOI":"10.1016\/S1571-0661(04)00256-7"},{"key":"e_1_2_1_2_105_2","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1145\/964001.964024","volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), January 2004","author":"O\u2019Hearn PW","year":"2004"},{"key":"e_1_2_1_2_106_2","first-page":"247","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), January 2005","author":"Parkinson M","year":"2005"},{"key":"e_1_2_1_2_107_2","first-page":"162","volume-title":"European symposium on programming languages and systems (ESOP), Vol 1576 of Lecture Notes in Computer Science","author":"Poetzsch-Heffter A","year":"1999"},{"key":"e_1_2_1_2_108_2","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: IEEE symposium on logic in computer science. IEEE New York pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_2_109_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.341844"},{"key":"e_1_2_1_2_110_2","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/978-3-540-39993-3_15","volume-title":"From object-orientation to formal methods, essays in memory of Ole\u2013Johan Dahl, Vol 2635 of Lecture Notes in Computer Science.","author":"Soundarajan N","year":"2004"},{"key":"e_1_2_1_2_111_2","unstructured":"Shaner S (2006) Semantics for model programs in JML. Master\u2019s Thesis Iowa State University (expected)"},{"key":"e_1_2_1_2_112_2","volume-title":"The Z notation: a reference manual. international series in computer science","author":"Spivey JM","year":"1992","edition":"2"},{"key":"e_1_2_1_2_113_2","unstructured":"von Oheimb D (2001) Analyzing Java in Isabelle\/HOL: formalization type safety and Hoare logic. PhD Thesis Technische Universit\u00e4t M\u00fcnchen. http:\/\/www4.in.tum.de\/ oheimb\/diss\/"},{"key":"e_1_2_1_2_114_2","doi-asserted-by":"crossref","unstructured":"von Oheimb D Nipkow T (2002) Hoare logic for NanoJava: auxiliary variables side effects and virtual methods revisited. In: Eriksson L-H Lindsay PA (eds) Formal methods\u2014getting IT Right (FME\u201902) Vol 2391 of Lecture Notes in Computer Science. Springer Heidelberg pp 89\u2013105. http:\/\/www.springerlink.com\/content\/bp1vtfr9ha3kl3t5","DOI":"10.1007\/3-540-45614-7_6"},{"key":"e_1_2_1_2_115_2","doi-asserted-by":"crossref","unstructured":"von Praun C Gross TR (2003) Static conflict analysis for multi-threaded object-oriented programs. In: Proceedings of the ACM SIGPLAN 2003 conference on programming language design and implementation (PLDI) June 2003. ACM New York pp 115\u2013128. doi:10.1145\/781131.781145","DOI":"10.1145\/780822.781145"},{"key":"e_1_2_1_2_116_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90011-4"},{"key":"e_1_2_1_2_117_2","unstructured":"Wahls T Baker AL Leavens GT (1994) The direct execution of SPECS-C++: a model-based specification language for C++ classes. Technical Report 94-02b Department of Computer Science Iowa State University March 1994. ftp:\/\/ftp.cs.iastate.edu\/pub\/ techreports\/TR94-02\/TR.ps.Z"},{"key":"e_1_2_1_2_118_2","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-1-4471-3552-4_11","volume-title":"Object orientation in Z, workshops in computing, Chap 11","author":"Wills A","year":"1992"},{"key":"e_1_2_1_2_119_2","doi-asserted-by":"publisher","DOI":"10.1145\/9758.10500"},{"key":"e_1_2_1_2_120_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_2_1_2_121_2","doi-asserted-by":"crossref","unstructured":"Wilson T Maharaj S Clark RG (2005) Omnibus verification policies: a flexible configurable approach to assertion-based software verification. In: Aichernig BK Beckert B (eds) Third IEEE international conference on software engineering and formal methods (SEFM) September 2005. IEEE Comput Soc New York pp 150\u2013159. doi:10.1109\/SEFM.2005.29","DOI":"10.1109\/SEFM.2005.29"},{"key":"e_1_2_1_2_122_2","first-page":"351","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), January 2005","author":"Xie Y","year":"2005"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0026-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0026-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0026-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T10:49:16Z","timestamp":1641466156000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0026-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6]]},"references-count":123,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,6]]}},"alternative-id":["10.1007\/s00165-007-0026-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0026-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6]]}}}