{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T08:21:44Z","timestamp":1782289304175,"version":"3.54.5"},"reference-count":269,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,6,1]],"date-time":"2012-06-01T00:00:00Z","timestamp":1338508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004965","name":"Sixth Framework Programme","doi-asserted-by":"publisher","award":["IST-2005-015905 MOBIUS"],"award-info":[{"award-number":["IST-2005-015905 MOBIUS"]}],"id":[{"id":"10.13039\/501100004965","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/F019394"],"award-info":[{"award-number":["EP\/F019394"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS 08-08913, CCF 0916350, and CCF 0916715"],"award-info":[{"award-number":["CNS 08-08913, CCF 0916350, and CCF 0916715"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CRI-0454348"],"award-info":[{"award-number":["CRI-0454348"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CNS 08-08913, CCF 0916350, and CCF 0916715"],"award-info":[{"award-number":["CNS 08-08913, CCF 0916350, and CCF 0916715"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2012,6]]},"abstract":"<jats:p>Behavioral interface specification languages provide formal code-level annotations, such as preconditions, postconditions, invariants, and assertions that allow programmers to express the intended behavior of program modules. Such specifications are useful for precisely documenting program behavior, for guiding implementation, and for facilitating agreement between teams of programmers in modular development of software. When used in conjunction with automated analysis and program verification tools, such specifications can support detection of common code vulnerabilities, capture of light-weight application-specific semantic properties, generation of test cases and test oracles, and full formal program verification. This article surveys behavioral interface specification languages with a focus toward automatic program verification and with a view towards aiding the Verified Software Initiative\u2014a fifteen-year, cooperative, international project directed at the scientific challenges of large-scale software verification.<\/jats:p>","DOI":"10.1145\/2187671.2187678","type":"journal-article","created":{"date-parts":[[2012,6,15]],"date-time":"2012-06-15T15:31:37Z","timestamp":1339774297000},"page":"1-58","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":108,"title":["Behavioral interface specification languages"],"prefix":"10.1145","volume":"44","author":[{"given":"John","family":"Hatcliff","sequence":"first","affiliation":[{"name":"Kansas State University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[{"name":"University of Central Florida"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Parkinson","sequence":"additional","affiliation":[{"name":"Microsoft Research Cambridge"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,6,14]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Abadi M. and Lamport L. 1988. The existence of refinement mappings. Tech. rep. 29 Digital Equipment Corporation Systems Research Center Palo Alto CA. Abadi M. and Lamport L. 1988. The existence of refinement mappings. Tech. rep. 29 Digital Equipment Corporation Systems Research Center Palo Alto CA."},{"key":"e_1_2_1_2_1","volume-title":"The B-Book: Assigning Programs to Meanings","author":"Abrial J.-R.","unstructured":"Abrial , J.-R. 1996. The B-Book: Assigning Programs to Meanings . Cambridge University Press , Cambridge, U.K. Abrial, J.-R. 1996. The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge, U.K."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 16th European Conference, Object-Oriented Programming (ECOOP'02)","volume":"2374","author":"Aldrich J.","unstructured":"Aldrich , J. , Chambers , C. , and Notkin , D . 2002. Architectural reasoning in ArchJava . In Proceedings of the 16th European Conference, Object-Oriented Programming (ECOOP'02) , B. Magnusson, Ed. Lecture Notes in Computer Science , vol. 2374 . Springer-Verlag, Berlin, 334--367. Aldrich, J., Chambers, C., and Notkin, D. 2002. Architectural reasoning in ArchJava. In Proceedings of the 16th European Conference, Object-Oriented Programming (ECOOP'02), B. Magnusson, Ed. Lecture Notes in Computer Science, vol. 2374. Springer-Verlag, Berlin, 334--367."},{"key":"e_1_2_1_4_1","volume-title":"UML in a Nutshell. O'Reilly","author":"Alhir S. S.","unstructured":"Alhir , S. S. 1998. UML in a Nutshell. O'Reilly , Sebastapol, CA . Alhir, S. S. 1998. UML in a Nutshell. O'Reilly, Sebastapol, CA."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 5th Annual Sympostum on Logic in Computer Science. IEEE Computer Society Press","author":"Alur R.","unstructured":"Alur , R. , Courcoubetts , C. , and Dill , D . 1990. Model checking for real-time systems . In Proceedings of the 5th Annual Sympostum on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA, 414--425. Alur, R., Courcoubetts, C., and Dill, D. 1990. Model checking for real-time systems. In Proceedings of the 5th Annual Sympostum on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 414--425."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/800022.808306"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/646147.679032"},{"key":"e_1_2_1_9_1","volume-title":"International Standard ISO\/IEC 13817-1","author":"Andrews D. J.","unstructured":"Andrews , D. J. 1996. Information technology programming languages, their environments and system software interfaces: Vienna Development Method--specification language -- part 1: Base language . International Standard ISO\/IEC 13817-1 , International Standards Organization . Andrews, D. J. 1996. Information technology programming languages, their environments and system software interfaces: Vienna Development Method--specification language -- part 1: Base language. International Standard ISO\/IEC 13817-1, International Standards Organization."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_1_11_1","volume-title":"Formal Description of Programming Concepts, E. J. Neuhold and M. Paul, Eds, IFIP State-of-the-Art Reports","author":"Apt K. R.","unstructured":"Apt , K. R. and 0lderog, E. 1991. Introduction to program verification . In Formal Description of Programming Concepts, E. J. Neuhold and M. Paul, Eds, IFIP State-of-the-Art Reports . Springer-Verlag , New York, NY , 363--429. Apt, K. R. and 0lderog, E. 1991. Introduction to program verification. In Formal Description of Programming Concepts, E. J. Neuhold and M. Paul, Eds, IFIP State-of-the-Art Reports. Springer-Verlag, New York, NY, 363--429."},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Apt K. R. and Olderog E. 1997. Verification of Sequential and Concurrent Programs 2nd ed. Graduate Texts in Computer Science Series. Springer-Verlag New York NY. Apt K. R. and Olderog E. 1997. Verification of Sequential and Concurrent Programs 2nd ed. Graduate Texts in Computer Science Series. Springer-Verlag New York NY.","DOI":"10.1007\/978-1-4757-2714-2"},{"key":"e_1_2_1_13_1","volume-title":"Unified Process: Practical Object-Oriented Analysis and Design","author":"Arlow J.","year":"2005","unstructured":"Arlow , J. and Neustadt , I . 2005 . UML 2 and the Unified Process: Practical Object-Oriented Analysis and Design 2 nd ed. Addison-Wesley , Indianoplis, IN. Arlow, J. and Neustadt, I. 2005. UML 2 and the Unified Process: Practical Object-Oriented Analysis and Design 2nd ed. Addison-Wesley, Indianoplis, IN.","edition":"2"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650070034"},{"key":"e_1_2_1_15_1","volume-title":"Mathematical Center Tracts","volume":"131","author":"Back R. J. R.","year":"1980","unstructured":"Back , R. J. R. 1980 . Correctness Preserving Program Refinements: Proof Theory and Applications . Mathematical Center Tracts , vol. 131 . Mathematical Centre, Amsterdam. Back, R. J. R. 1980. Correctness Preserving Program Refinements: Proof Theory and Applications. Mathematical Center Tracts, vol. 131. Mathematical Centre, Amsterdam."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01887198"},{"key":"e_1_2_1_17_1","volume-title":"Computer Aided Verification. Lecture Notes in Computer Science","volume":"2102","author":"Ball T.","unstructured":"Ball , T. and Rajamani , S. K . 2001. The SLAM toolkit . In Computer Aided Verification. Lecture Notes in Computer Science , vol. 2102 . Springer-Verlag, Berlin, 260--264. Ball, T. and Rajamani, S. K. 2001. The SLAM toolkit. In Computer Aided Verification. Lecture Notes in Computer Science, vol. 2102. Springer-Verlag, Berlin, 260--264."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_16"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_17"},{"key":"e_1_2_1_20_1","volume-title":"High Integrity Ada: The SPARK Approach","author":"Barnes J.","unstructured":"Barnes , J. 1997. High Integrity Ada: The SPARK Approach . Addison Wesley Longman, Inc. , Reading, MA . Barnes, J. 1997. High Integrity Ada: The SPARK Approach. Addison Wesley Longman, Inc., Reading, MA."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_24_1","unstructured":"Barnett M. Schulte D. A. N. W. and Sun Q. 2004. 99.44&percnt; pure: Useful abstractions in specification. In Formal Techniques for Java-like Programs (FTfJP) E. Poll Ed. Radbod University Nijmegen 11--19. http:\/\/www.cs.ru.nl\/ftfjp\/2004\/Purity.pdf. Barnett M. Schulte D. A. N. W. and Sun Q. 2004. 99.44&percnt; pure: Useful abstractions in specification. In Formal Techniques for Java-like Programs (FTfJP) E. Poll Ed. Radbod University Nijmegen 11--19. http:\/\/www.cs.ru.nl\/ftfjp\/2004\/Purity.pdf."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(02)00041-9"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07)","volume":"4590","author":"Barrett C.","unstructured":"Barrett , C. and Tinelli , C . 2007. CVC3 . In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07) , W. Damm and H. Hermanns, Eds. Lecture Notes in Computer Science , vol. 4590 . Springer-Verlag, Berlin, 298--302. Barrett, C. and Tinelli, C. 2007. CVC3. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07), W. Damm and H. Hermanns, Eds. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, 298--302."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264250"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the Workshop on Runtime Verification held in conjunction with the 13th Conference on Computer Aided Verification (CAV'01)","author":"Bartetzko D.","unstructured":"Bartetzko , D. , Fischer , C. , Moller , M. , and Wehrheim , H . 2001. Jass - Java with assertions . In Proceedings of the Workshop on Runtime Verification held in conjunction with the 13th Conference on Computer Aided Verification (CAV'01) . Published in Electronic Notes in Theoretical Computer Science, K. Havelund and G. Rosu, Eds., 55, 2. Bartetzko, D., Fischer, C., Moller, M., and Wehrheim, H. 2001. Jass - Java with assertions. In Proceedings of the Workshop on Runtime Verification held in conjunction with the 13th Conference on Computer Aided Verification (CAV'01). Published in Electronic Notes in Theoretical Computer Science, K. Havelund and G. Rosu, Eds., 55, 2."},{"key":"e_1_2_1_29_1","volume-title":"ACSL: ANSI\/ISO C Specification Language, version 1.4. ANSI","author":"Baudin P.","year":"2009","unstructured":"Baudin , P. , Filli\u00e2tre , J.-C. , March\u00e9 , C. , Monate , B. , Moy , Y. , and Prevosto , V . 2009 . ACSL: ANSI\/ISO C Specification Language, version 1.4. ANSI . http:\/\/frama-c.cea.fr\/acsl.html. Baudin, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., and Prevosto, V. 2009. ACSL: ANSI\/ISO C Specification Language, version 1.4. ANSI. http:\/\/frama-c.cea.fr\/acsl.html."},{"key":"e_1_2_1_30_1","volume-title":"Verification of Object-Oriented Software: The KeY Approach. Lecture Notes in Computer Science","volume":"4334","author":"Beckert B.","unstructured":"Beckert , B. , H\u00e4hnle , R. , and Schmitt , P. H . 2007 . Verification of Object-Oriented Software: The KeY Approach. Lecture Notes in Computer Science , vol. 4334 . Springer-Verlag, Berlin. Beckert, B., H\u00e4hnle, R., and Schmitt, P. H. 2007. Verification of Object-Oriented Software: The KeY Approach. Lecture Notes in Computer Science, vol. 4334. Springer-Verlag, Berlin."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_1_32_1","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","author":"Berry G.","unstructured":"Berry , G. 2000. The foundations of Esterel . In Proof, Language and Interaction: Essays in Honour of Robin Milner , G. Plotkin, C. Stirling, and M. Tofte, Eds. The MIT Press , Cambridge, MA . Berry, G. 2000. The foundations of Esterel. In Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling, and M. Tofte, Eds. The MIT Press, Cambridge, MA."},{"key":"e_1_2_1_33_1","volume-title":"Eds","author":"Bidoit M.","year":"1991","unstructured":"Bidoit , M. , Kreowski , H.-J. , Lescanne , P. , Orejas , F. , and Sannella , D. , Eds . 1991 . Algebraic System Specification and Development: A Survey and Annotated Bibliography. Lecture Notes in Computer Science, vol. 501 . Springer-Verlag , Berlin. Bidoit, M., Kreowski, H.-J., Lescanne, P., Orejas, F., and Sannella, D., Eds. 1991. Algebraic System Specification and Development: A Survey and Annotated Bibliography. Lecture Notes in Computer Science, vol. 501. Springer-Verlag, Berlin."},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner D. and Henson M. C. 2008. Logics of Specification Languages. Springer-Verlag Berlin. Bj\u00f8rner D. and Henson M. C. 2008. Logics of Specification Languages. Springer-Verlag Berlin.","DOI":"10.1007\/978-3-540-74107-7"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Blanchet B. Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. Monniaux D. and Rival X. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation: Complexity Analysis Transformation T. A. Mogensen D. A. Schmidt and I. H. Sudborough Eds. Lecture Notes in Computer Science vol. 2566. Springer-Verlag 85--108. Blanchet B. Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. Monniaux D. and Rival X. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation: Complexity Analysis Transformation T. A. Mogensen D. A. Schmidt and I. H. Sudborough Eds. Lecture Notes in Computer Science vol. 2566. Springer-Verlag 85--108.","DOI":"10.1007\/3-540-36377-7_5"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E. and St\u00e4rk R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag Berlin. B\u00f6rger E. and St\u00e4rk R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag Berlin.","DOI":"10.1007\/978-3-642-18216-7"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.469460"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_2_1_39_1","volume-title":"Static Analysis (SAS)","author":"Boyland J.","unstructured":"Boyland , J. 2003. Checking interference with fractional permissions . In Static Analysis (SAS) , R. Cousot, Ed. Lecture Notes in Computer Science, vol. 2694 . Springer-Verlag , Berlin, 55--72. Boyland, J. 2003. Checking interference with fractional permissions. In Static Analysis (SAS), R. Cousot, Ed. Lecture Notes in Computer Science, vol. 2694. Springer-Verlag, Berlin, 55--72."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90007-7"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/567532.567546"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.203096"},{"key":"e_1_2_1_45_1","volume-title":"FME 2002: Formal Methods-Getting IT Right, L. H. Eriksson and P. A. Lindsay, Eds. Lecture Notes in Computer Science vol., 2391","author":"Cata\u00f1o N.","unstructured":"Cata\u00f1o , N. and Huisman , M . 2002. Formal specification of Gemplus's electronic purse case study . In FME 2002: Formal Methods-Getting IT Right, L. H. Eriksson and P. A. Lindsay, Eds. Lecture Notes in Computer Science vol., 2391 . Springer-Verlag, Berlin, 272--289. Cata\u00f1o, N. and Huisman, M. 2002. Formal specification of Gemplus's electronic purse case study. In FME 2002: Formal Methods-Getting IT Right, L. H. Eriksson and P. A. Lindsay, Eds. Lecture Notes in Computer Science vol., 2391. Springer-Verlag, Berlin, 272--289."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.26"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.9"},{"key":"e_1_2_1_48_1","first-page":"6","article-title":"Structural specification-based testing: Automated support and experimental evaluation. In Software Engineering -- ESEC\/FSE '99, O. Nierstrasz and M. Lemoine, Eds. Lecture Notes in Computer Science, vol. 1687. Springer-Verlag, 285--302","volume":"24","author":"Chang J.","year":"1999","unstructured":"Chang , J. and Richardson , D. J. 1999 . Structural specification-based testing: Automated support and experimental evaluation. In Software Engineering -- ESEC\/FSE '99, O. Nierstrasz and M. Lemoine, Eds. Lecture Notes in Computer Science, vol. 1687. Springer-Verlag, 285--302 . Also ACM SIGSOFT Softw. Engineer. Notes , 24 , 6 . Chang, J. and Richardson, D. J. 1999. Structural specification-based testing: Automated support and experimental evaluation. In Software Engineering -- ESEC\/FSE '99, O. Nierstrasz and M. Lemoine, Eds. Lecture Notes in Computer Science, vol. 1687. Springer-Verlag, 285--302. Also ACM SIGSOFT Softw. Engineer. Notes, 24, 6.","journal-title":"Also ACM SIGSOFT Softw. Engineer. Notes"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/369264.369270"},{"key":"e_1_2_1_50_1","unstructured":"Chen Y. and Cheng B. H. C. 2000. A semantic foundation for specification matching. In Foundations of Component-Based Systems G. T. Leavens and M. Sitaraman Eds. Cambridge University Press New York NY 91--109. Chen Y. and Cheng B. H. C. 2000. A semantic foundation for specification matching. In Foundations of Component-Based Systems G. T. Leavens and M. Sitaraman Eds. Cambridge University Press New York NY 91--109."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/196092.195325"},{"key":"e_1_2_1_52_1","volume-title":"Proceedings of the International Conference on Software Engineering Research and Practice (SERP '02)","author":"Cheon Y.","unstructured":"Cheon , Y. and Leavens , G. T . 2002. A runtime assertion checker for the Java Modeling Language (JML) . In Proceedings of the International Conference on Software Engineering Research and Practice (SERP '02) , H. R. Arabnia and Y. Mun, Eds. CSREA Press, 322--328. Cheon, Y. and Leavens, G. T. 2002. A runtime assertion checker for the Java Modeling Language (JML). In Proceedings of the International Conference on Software Engineering Research and Practice (SERP '02), H. R. Arabnia and Y. Mun, Eds. CSREA Press, 322--328."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1085130.1085150"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.v35:6"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328452"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_58_1","unstructured":"Clarke M. J. Grumberg O. and Peled D. A. 1999. Model Checking. The MIT Press Cambridge MA. Clarke M. J. Grumberg O. and Peled D. A. 1999. Model Checking. The MIT Press Cambridge MA."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127900"},{"key":"e_1_2_1_60_1","series-title":"Lecture Notes in Computer Science","volume-title":"Casl Reference Manual","author":"Co","unstructured":"Co FI (The Common Framework Initiative). 2004. Casl Reference Manual . Lecture Notes in Computer Science , vol. 2960 (IFIP Series). Springer-Verlag , Berlin. CoFI (The Common Framework Initiative). 2004. Casl Reference Manual. Lecture Notes in Computer Science, vol. 2960 (IFIP Series). Springer-Verlag, Berlin."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_42"},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the 7th International Workshop on Specification and Verification of Component-Based Systems (SAVCBS'08)","author":"Cok D.","unstructured":"Cok , D. and Leavens , G. T . 2008. Extensions of the theory of observational purity and a practical design for JML . In Proceedings of the 7th International Workshop on Specification and Verification of Component-Based Systems (SAVCBS'08) . Tech. Rep. CS-TR-08-07. School of EECS, University of Central Florida, Orlando, FL, 43--50. Cok, D. and Leavens, G. T. 2008. Extensions of the theory of observational purity and a practical design for JML. In Proceedings of the 7th International Workshop on Specification and Verification of Component-Based Systems (SAVCBS'08). Tech. Rep. CS-TR-08-07. School of EECS, University of Central Florida, Orlando, FL, 43--50."},{"key":"e_1_2_1_64_1","volume-title":"Proceedings of the ECOOP Workshop FTfJP'2004 Formal Techniques for Java-like Programs, E. Poll, Ed","author":"Cok D. R.","year":"2004","unstructured":"Cok , D. R. 2004 . Reasoning with specifications containing method calls in JML and first-order provers . In Proceedings of the ECOOP Workshop FTfJP'2004 Formal Techniques for Java-like Programs, E. Poll, Ed . Rabound University, Nijmegen, 41--48. Cok, D. R. 2004. Reasoning with specifications containing method calls in JML and first-order provers. In Proceedings of the ECOOP Workshop FTfJP'2004 Formal Techniques for Java-like Programs, E. Poll, Ed. Rabound University, Nijmegen, 41--48."},{"key":"e_1_2_1_65_1","volume-title":"Cleveland, W., et al.","author":"Constable R. L.","year":"1986","unstructured":"Constable , R. L. , Allen , S. , h. Bromely , Cleveland, W., et al. 1986 . Implementing Mathematics with the Nuprl Development System. Prentice-Hall , Inc., Englewood Cliffs, NJ. Constable, R. L., Allen, S., h. Bromely, Cleveland, W., et al. 1986. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Inc., Englewood Cliffs, NJ."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_67_1","volume-title":"Handbook of Theoretical Computer Science","author":"Cousot P.","unstructured":"Cousot , P. 1990. Methods and logics for proving programs . In Handbook of Theoretical Computer Science , J. van Leewen, Ed. Vol. B : Formal Models and Semantics. The MIT Press , New York, NY, 841--993. Cousot, P. 1990. Methods and logics for proving programs. In Handbook of Theoretical Computer Science, J. van Leewen, Ed. Vol. B: Formal Models and Semantics. The MIT Press, New York, NY, 841--993."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010218"},{"key":"e_1_2_1_70_1","volume-title":"10th International Conference, A. L. Matthew B. Dwyer, Ed. Lecture Notes in Computer Science","volume":"4422","author":"Darvas","unstructured":"Darvas , \u00c1. and Leino, K. R. M. 2007. Practical reasoning about invocations and implementations of pure methods. In Fundamental Approaches to Software Engineering , 10th International Conference, A. L. Matthew B. Dwyer, Ed. Lecture Notes in Computer Science , vol. 4422 . Springer-Verlag, Berlin, 336--351. Darvas, \u00c1. and Leino, K. R. M. 2007. Practical reasoning about invocations and implementations of pure methods. In Fundamental Approaches to Software Engineering, 10th International Conference, A. L. Matthew B. Dwyer, Ed. Lecture Notes in Computer Science, vol. 4422. Springer-Verlag, Berlin, 336--351."},{"key":"e_1_2_1_71_1","doi-asserted-by":"crossref","unstructured":"Darvas \u00c1. and M\u00fcller P. 2005. Reasoning about method calls in JML specifications. In Formal Techniques for Java-like Programs. ETH Zurich Switzerland. Darvas \u00c1. and M\u00fcller P. 2005. Reasoning about method calls in JML specifications. In Formal Techniques for Java-like Programs. ETH Zurich Switzerland.","DOI":"10.5381\/jot.2006.5.5.a3"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2006.5.5.a3"},{"key":"e_1_2_1_73_1","volume-title":"Lecture Notes in Computer Science","volume":"4963","author":"de Moura L.","unstructured":"de Moura , L. and Bj\u00f8rner , N . 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis (TACAS) . Lecture Notes in Computer Science , vol. 4963 . Springer-Verlag, Berlin, 337--340. de Moura, L. and Bj\u00f8rner, N. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis (TACAS). Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, 337--340."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2006.26"},{"key":"e_1_2_1_75_1","unstructured":"Detlefs D. L. Leino K. R. M. Nelson G. and Saxe J. B. 1998. Extended static checking. SRC Research rep. 159 Compaq Systems Research Center Palo Alto CA. Detlefs D. L. Leino K. R. M. Nelson G. and Saxe J. B. 1998. Extended static checking. SRC Research rep. 159 Compaq Systems Research Center Palo Alto CA."},{"key":"e_1_2_1_76_1","volume-title":"Proceedings of the 18th International Conference on Software Engineering. IEEE Computer Society Press","author":"Dhara K. K.","unstructured":"Dhara , K. K. and Leavens , G. T . 1996. Forcing behavioral subtyping through specification inheritance . In Proceedings of the 18th International Conference on Software Engineering. IEEE Computer Society Press , Los Alamitos, CA, 258--267. A corrected version is ISU CS TR &num;95-20c, http:\/\/tinyurl.com\/s2krg. Dhara, K. K. and Leavens, G. T. 1996. Forcing behavioral subtyping through specification inheritance. In Proceedings of the 18th International Conference on Software Engineering. IEEE Computer Society Press, Los Alamitos, CA, 258--267. A corrected version is ISU CS TR &num;95-20c, http:\/\/tinyurl.com\/s2krg."},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2005.4.8.a1"},{"key":"e_1_2_1_78_1","volume-title":"A Discipline of Programming","author":"Dijkstra E. W.","unstructured":"Dijkstra , E. W. 1976. A Discipline of Programming . Prentice-Hall, Inc. , Englewood Cliffs, NJ . Dijkstra, E. W. 1976. A Discipline of Programming. Prentice-Hall, Inc., Englewood Cliffs, NJ."},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134409"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_18"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/190679.190682"},{"key":"e_1_2_1_84_1","unstructured":"Eiffel. 2005. Eiffel analysis design and programming language. ECMA Standard 367. Eiffel. 2005. Eiffel analysis design and programming language. ECMA Standard 367."},{"key":"e_1_2_1_85_1","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E. A.","unstructured":"Emerson , E. A. 1990. Temporal and modal logic . In Handbook of Theoretical Computer Science , J. van Leeuwen, Ed. Vol. B. The MIT Press , Cambridge, MA , 995--1072. Emerson, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Vol. B. The MIT Press, Cambridge, MA, 995--1072."},{"key":"e_1_2_1_86_1","volume-title":"Proceedings of the ICSE Workshop on Dynamic Analysis, (WODA'03)","author":"Ernst M. D.","year":"2003","unstructured":"Ernst , M. D. 2003 . Static and dynamic analysis: Synergy and duality . In Proceedings of the ICSE Workshop on Dynamic Analysis, (WODA'03) . New Mexico State University, NM, 24--27. Ernst, M. D. 2003. Static and dynamic analysis: Synergy and duality. In Proceedings of the ICSE Workshop on Dynamic Analysis, (WODA'03). New Mexico State University, NM, 24--27."},{"key":"e_1_2_1_87_1","volume-title":"Proceedings of the ECOOP International Workshop on Aliasing, Confinement and Ownership (IWACO'03)","author":"F\u00e4hndrich M.","unstructured":"F\u00e4hndrich , M. and Leino , K. R. M. 2003. Heap monotonic typestates . In Proceedings of the ECOOP International Workshop on Aliasing, Confinement and Ownership (IWACO'03) . K. U. Leuven, Leuven. F\u00e4hndrich, M. and Leino, K. R. M. 2003. Heap monotonic typestates. In Proceedings of the ECOOP International Workshop on Aliasing, Confinement and Ownership (IWACO'03). K. U. Leuven, Leuven."},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297052"},{"key":"e_1_2_1_89_1","volume-title":"Proceedings of the 6th International Conference on Formal Engineering Methods (ICFEM'04)","volume":"3308","author":"Filli\u00e2tre J.-C.","unstructured":"Filli\u00e2tre , J.-C. and March\u00e9 , C . 2004. Multi-prover verification of C programs . In Proceedings of the 6th International Conference on Formal Engineering Methods (ICFEM'04) . Lecture Notes in Computer Science , vol. 3308 . Springer-Verlag, Berlin, 15--29. Filli\u00e2tre, J.-C. and March\u00e9, C. 2004. Multi-prover verification of C programs. In Proceedings of the 6th International Conference on Formal Engineering Methods (ICFEM'04). Lecture Notes in Computer Science, vol. 3308. Springer-Verlag, Berlin, 15--29."},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504283"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_2_1_92_1","volume-title":"Logics of Specification Languages","author":"Fitzgerald J.","unstructured":"Fitzgerald , J. 2008. The typed logic of partial functions and the Vienna Development Method . In Logics of Specification Languages , Springer-Verlag , Berlin , 453--487. Fitzgerald, J. 2008. The typed logic of partial functions and the Vienna Development Method. In Logics of Specification Languages, Springer-Verlag, Berlin, 453--487."},{"key":"e_1_2_1_93_1","volume-title":"Modelling Systems: Practical Tools in Software Development","author":"Fitzgerald J.","year":"1998","unstructured":"Fitzgerald , J. and Larsen , P. G . 1998 . Modelling Systems: Practical Tools in Software Development . Cambridge Press, Cambridge , U.K. Fitzgerald, J. and Larsen, P. G. 1998. Modelling Systems: Practical Tools in Software Development. Cambridge Press, Cambridge, U.K."},{"key":"e_1_2_1_94_1","unstructured":"Fitzgerald J. S. Larsen P. G. Mukherjee P. Plat N. and Verhoef M. 2005. Validated Designs for Object-Oriented Systems. Springer-Verlag London. Fitzgerald J. S. Larsen P. G. Mukherjee P. Plat N. and Verhoef M. 2005. Validated Designs for Object-Oriented Systems. Springer-Verlag London."},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_98_1","volume-title":"Addison-Wesley Publishing Co","author":"Francez N.","unstructured":"Francez , N. 1992. Program Verification . Addison-Wesley Publishing Co ., Cambridge, U.K. Francez, N. 1992. Program Verification. Addison-Wesley Publishing Co., Cambridge, U.K."},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667062.1667063"},{"key":"e_1_2_1_100_1","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"Gamma E.","year":"1995","unstructured":"Gamma , E. , Helm , R. , Johnson , R. , and Vlissides , J . 1995 . Design Patterns: Elements of Reusable Object-Oriented Software . Addison-Wesley , Reading, MA . Gamma, E., Helm, R., Johnson, R., and Vlissides, J. 1995. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading, MA."},{"key":"e_1_2_1_101_1","volume-title":"Acme: Architectural description of component-based systems. In Foundations of Component-Based Systems","author":"Garlan D.","year":"2000","unstructured":"Garlan , D. , Monroe , R. T. , and Wile , D . 2000 . Acme: Architectural description of component-based systems. In Foundations of Component-Based Systems , G. T. Leavens and M. Sitaraman, Eds. Cambridge University Press , New York, NY , 47--67. Garlan, D., Monroe, R. T., and Wile, D. 2000. Acme: Architectural description of component-based systems. In Foundations of Component-Based Systems, G. T. Leavens and M. Sitaraman, Eds. Cambridge University Press, New York, NY, 47--67."},{"key":"e_1_2_1_102_1","volume-title":"Current Trends in Programming Methodology","volume":"4","author":"Goguen J. A.","unstructured":"Goguen , J. A. , Thatcher , J. W. , and Wagner , E. G . 1978. An initial algebra approach to the specification, correctness and implementation of abstract data types . In Current Trends in Programming Methodology , vol. 4 , R. T. Yeh, Ed. V Prentice-Hall, Inc., Englewood Cliffs, NJ., 80--149. Goguen, J. A., Thatcher, J. W., and Wagner, E. G. 1978. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Current Trends in Programming Methodology, vol. 4, R. T. Yeh, Ed. V Prentice-Hall, Inc., Englewood Cliffs, NJ., 80--149."},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361230"},{"key":"e_1_2_1_104_1","volume-title":"A complete axiomatic system for proving assertions about recursive and non-recursive programs. Tech. rep. 75","author":"Gorelick G. A.","unstructured":"Gorelick , G. A. 1975. A complete axiomatic system for proving assertions about recursive and non-recursive programs. Tech. rep. 75 , University of Toronto , Toronto, Canada . Gorelick, G. A. 1975. A complete axiomatic system for proving assertions about recursive and non-recursive programs. Tech. rep. 75, University of Toronto, Toronto, Canada."},{"key":"e_1_2_1_105_1","doi-asserted-by":"crossref","unstructured":"Gries D. and Schneider F. B. 1995. Avoiding the undefined by underspecification. In Computer Science Today: Recent Trends and Developments J. van Leeuwen Ed. Lecture Notes in Computer Science no. 1000. Springer-Verlag New York NY 366--373. Gries D. and Schneider F. B. 1995. Avoiding the undefined by underspecification. In Computer Science Today: Recent Trends and Developments J. van Leeuwen Ed. Lecture Notes in Computer Science no. 1000. Springer-Verlag New York NY 366--373.","DOI":"10.1007\/BFb0015254"},{"key":"e_1_2_1_106_1","volume-title":"Proceedings of the Workshop on Software Model Checking.","author":"Grieskamp W.","unstructured":"Grieskamp , W. , Tillmann , N. , and Schulte , W . 2005. XRT - exploring runtime for .NET - architecture and applications . In Proceedings of the Workshop on Software Model Checking. Grieskamp, W., Tillmann, N., and Schulte, W. 2005. XRT - exploring runtime for .NET - architecture and applications. In Proceedings of the Workshop on Software Model Checking."},{"key":"e_1_2_1_107_1","volume-title":"Proceedings of the 1st International Workshop on Larch, U. Martin and J. M. Wing, Eds. Springer-Verlag","author":"Guaspari D.","unstructured":"Guaspari , D. , Marceau , C. , and Polak , W . 1992. Formal verification of Ada programs . In Proceedings of the 1st International Workshop on Larch, U. Martin and J. M. Wing, Eds. Springer-Verlag , New York, NY, 104--141. Guaspari, D., Marceau, C., and Polak, W. 1992. Formal verification of Ada programs. In Proceedings of the 1st International Workshop on Larch, U. Martin and J. M. Wing, Eds. Springer-Verlag, New York, NY, 104--141."},{"key":"e_1_2_1_108_1","first-page":"264","article-title":"Evolving algebras: A tutorial introduction","volume":"43","author":"Gurevich Y.","year":"1991","unstructured":"Gurevich , Y. 1991 . Evolving algebras: A tutorial introduction . Bullet. EATCS 43 , 264 -- 284 . Gurevich, Y. 1991. Evolving algebras: A tutorial introduction. Bullet. EATCS 43, 264--284.","journal-title":"Bullet. EATCS"},{"key":"e_1_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.5555\/14170.14171"},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.5555\/151155"},{"key":"e_1_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.231756"},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.159839"},{"key":"e_1_2_1_113_1","volume-title":"Logics of Specification Languages","author":"Hansen M. R.","unstructured":"Hansen , M. R. 2008. Duration calculus . In Logics of Specification Languages , Springer-Verlag , Berlin , 299--347. Hansen, M. R. 2008. Duration calculus. In Logics of Specification Languages, Springer-Verlag, Berlin, 299--347."},{"key":"e_1_2_1_114_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_115_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.54292"},{"key":"e_1_2_1_116_1","volume-title":"1993. Specification Case Studies","author":"Hayes I.","unstructured":"Hayes , I. , Ed. 1993. Specification Case Studies , 2 nd ed. International Series in Computer Science. Prentice-Hall , Inc., London, U.K. Hayes, I., Ed. 1993. Specification Case Studies, 2nd ed. International Series in Computer Science. Prentice-Hall, Inc., London, U.K.","edition":"2"},{"key":"e_1_2_1_117_1","volume-title":"Mathematics of Program Construction","author":"Hehner E. C. R.","unstructured":"Hehner , E. C. R. 1989. Termination is timing . In Mathematics of Program Construction , J. L. A. van de Snepscheut, Ed. Lecture Notes in Computer Science, vol. 375 . Springer-Verlag , Berlin, 36--47. Hehner, E. C. R. 1989. Termination is timing. In Mathematics of Program Construction, J. L. A. van de Snepscheut, Ed. Lecture Notes in Computer Science, vol. 375. Springer-Verlag, Berlin, 36--47."},{"key":"e_1_2_1_118_1","volume-title":"A Practical Theory of Programming. Texts and Monographs in Computer Science","author":"Hehner E. C. R.","unstructured":"Hehner , E. C. R. 1993. A Practical Theory of Programming. Texts and Monographs in Computer Science . Springer-Verlag , New York, NY . http:\/\/www.cs.utoronto.ca\/~hehner\/aPToP. Hehner, E. C. R. 1993. A Practical Theory of Programming. Texts and Monographs in Computer Science. Springer-Verlag, New York, NY. http:\/\/www.cs.utoronto.ca\/~hehner\/aPToP."},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050017"},{"key":"e_1_2_1_120_1","unstructured":"Hehner E. C. R. 2005. Specified blocks. Verified Software: Theories Tools Experiments (VSTTE). http:\/\/tinyurl.com\/2a7kf2. Hehner E. C. R. 2005. Specified blocks. Verified Software: Theories Tools Experiments (VSTTE). http:\/\/tinyurl.com\/2a7kf2."},{"key":"e_1_2_1_121_1","volume-title":"Proceedings of the 11th IEEE International Conference on Requirements Engineering (RE'03)","author":"Heimdahl M. P. E.","unstructured":"Heimdahl , M. P. E. , Whalen , M. W. , and Thompson , J. M . 2003. NIMBUS: A tool for specification centered development . In Proceedings of the 11th IEEE International Conference on Requirements Engineering (RE'03) . IEEE Computer Society, Los Alamitos, CA, 349. Heimdahl, M. P. E., Whalen, M. W., and Thompson, J. M. 2003. NIMBUS: A tool for specification centered development. In Proceedings of the 11th IEEE International Conference on Requirements Engineering (RE'03). IEEE Computer Society, Los Alamitos, CA, 349."},{"key":"e_1_2_1_122_1","volume-title":"Proceedings of the 15th IEEE International Requirements Engineering Conference (RE'07)","author":"Heitmeyer C.","unstructured":"Heitmeyer , C. , Jeffords , R. , Bharadwaj , R. , and Archer , M . 2007. Re theory meets software practice: Lessons from the software development trenches . In Proceedings of the 15th IEEE International Requirements Engineering Conference (RE'07) . IEEE, Los Alamitos, California, 265--268. Heitmeyer, C., Jeffords, R., Bharadwaj, R., and Archer, M. 2007. Re theory meets software practice: Lessons from the software development trenches. In Proceedings of the 15th IEEE International Requirements Engineering Conference (RE'07). IEEE, Los Alamitos, California, 265--268."},{"key":"e_1_2_1_123_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.730543"},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_126_1","doi-asserted-by":"publisher","DOI":"10.1145\/1459352.1459354"},{"key":"e_1_2_1_127_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_128_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059696"},{"key":"e_1_2_1_129_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_130_1","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","unstructured":"Hoare , C. A. R. 1985. Communicating Sequential Processes . Prentice-Hall, Inc. , Englewood Cliffs, NJ . Hoare, C. A. R. 1985. Communicating Sequential Processes. Prentice-Hall, Inc., Englewood Cliffs, NJ."},{"key":"e_1_2_1_131_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_5"},{"key":"e_1_2_1_132_1","unstructured":"Hoare C. A. R. and He J. 1998. Unifying Theories of Programming. Prentice-Hall International Englewood Cliffs NJ. Hoare C. A. R. and He J. 1998. Unifying Theories of Programming. Prentice-Hall International Englewood Cliffs NJ."},{"key":"e_1_2_1_133_1","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_2_1_134_1","unstructured":"Hoare T. Leavens G. T. Misra J. and Shankar N. 2007. The verified software initiative: A manifesto. http:\/\/qpq.csl.sri.com\/vsr\/manifesto.pdf. Hoare T. Leavens G. T. Misra J. and Shankar N. 2007. The verified software initiative: A manifesto. http:\/\/qpq.csl.sri.com\/vsr\/manifesto.pdf."},{"key":"e_1_2_1_135_1","volume-title":"Design and validation of computer protocols","author":"Holzmann G. J.","unstructured":"Holzmann , G. J. 1991. Design and validation of computer protocols . Prentice-Hall, Englewood Cliffs , NJ. Holzmann, G. J. 1991. Design and validation of computer protocols. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_136_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_137_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"1783","author":"Huisman M.","unstructured":"Huisman , M. and Jacobs , B . 2000. Java program verification via a Hoare logic with abrupt termination. In Fundamental Approaches to Software Engineering (FASE 2000), T. Maibaum , Ed. Lecture Notes in Computer Science , vol. 1783 . Springer-Verlag, Berlin, 284--303. Huisman, M. and Jacobs, B. 2000. Java program verification via a Hoare logic with abrupt termination. In Fundamental Approaches to Software Engineering (FASE 2000), T. Maibaum, Ed. Lecture Notes in Computer Science, vol. 1783. Springer-Verlag, Berlin, 284--303."},{"key":"e_1_2_1_138_1","doi-asserted-by":"publisher","DOI":"10.1145\/226241.226249"},{"key":"e_1_2_1_139_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson D.","year":"2006","unstructured":"Jackson , D. 2006 . Software Abstractions: Logic, Language, and Analysis . MIT Press, Cambridge , MA. Jackson, D. 2006. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_140_1","doi-asserted-by":"crossref","unstructured":"Jacky J. Veanes M. Campbell C. and Schulte W. 2008. Model-Based Software Testing and Analysis with C&num;. Cambridge University Press Cambridge U.K. Jacky J. Veanes M. Campbell C. and Schulte W. 2008. Model-Based Software Testing and Analysis with C&num;. Cambridge University Press Cambridge U.K.","DOI":"10.1017\/CBO9780511619540"},{"key":"e_1_2_1_141_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2007.36"},{"key":"e_1_2_1_142_1","unstructured":"Jacobs B. and Piessens F. 2008. The VeriFast program verifier. Tech. rep. CW-520 Department of Computer Science Katholieke Universiteit Leuven. Jacobs B. and Piessens F. 2008. The VeriFast program verifier. Tech. rep. CW-520 Department of Computer Science Katholieke Universiteit Leuven."},{"key":"e_1_2_1_143_1","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452045"},{"key":"e_1_2_1_144_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_145_1","volume-title":"Systematic Software Development Using VDM","author":"Jones C. B.","unstructured":"Jones , C. B. 1990. Systematic Software Development Using VDM , 2 nd ed. International Series in Computer Science. Prentice Hall , Englewood Cliffs, NJ. Jones, C. B. 1990. Systematic Software Development Using VDM, 2nd ed. International Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ.","edition":"2"},{"key":"e_1_2_1_146_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00042-B"},{"key":"e_1_2_1_147_1","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.2003.1203057"},{"key":"e_1_2_1_148_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.002"},{"key":"e_1_2_1_149_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_1_150_1","volume-title":"Proceedings of the 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03)","volume":"2619","author":"Khurshid S.","unstructured":"Khurshid , S. , P\u0103s\u0103reanu , C. S. , and Visser , W . 2003. Generalized symbolic execution for model checking and testing . In Proceedings of the 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03) , H. Garavel and J. Hatcliff, Eds. Lecture Notes in Computer Science , vol. 2619 . 553--568. Khurshid, S., P\u0103s\u0103reanu, C. S., and Visser, W. 2003. Generalized symbolic execution for model checking and testing. In Proceedings of the 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03), H. Garavel and J. Hatcliff, Eds. Lecture Notes in Computer Science, vol. 2619. 553--568."},{"key":"e_1_2_1_151_1","volume-title":"Real-time Euclid: A language for reliable real-time systems. In Real-Time Systems: Abstractions, Languages, and Design Methodologies","author":"Kligerman E.","year":"1992","unstructured":"Kligerman , E. and Stoyenko , A . 1992 . Real-time Euclid: A language for reliable real-time systems. In Real-Time Systems: Abstractions, Languages, and Design Methodologies , K. M. Kavi, Ed. IEEE Computer Society Press , Los Alamitos , California, 455--463. Kligerman, E. and Stoyenko, A. 1992. Real-time Euclid: A language for reliable real-time systems. In Real-Time Systems: Abstractions, Languages, and Design Methodologies, K. M. Kavi, Ed. IEEE Computer Society Press, Los Alamitos, California, 455--463."},{"key":"e_1_2_1_152_1","doi-asserted-by":"crossref","unstructured":"Kozen D. and Tiuryn J. 1990. Logics of programs. In Handbook of Theoretical Computer Science vol. B: Formal Models and Semantics. J. van Leewen Ed. The MIT Press New York NY 789--840. Kozen D. and Tiuryn J. 1990. Logics of programs. In Handbook of Theoretical Computer Science vol. B: Formal Models and Semantics. J. van Leewen Ed. The MIT Press New York NY 789--840.","DOI":"10.1016\/B978-0-444-88074-1.50019-6"},{"key":"e_1_2_1_153_1","volume-title":"Concurrency: State Models & Java Programs","author":"Kramer J.","year":"2006","unstructured":"Kramer , J. and Magee , J . 2006 . Concurrency: State Models & Java Programs , 2 nd Edition. Worldwide Series in Computer Science. John Wiley and Sons , Hoboken, NJ. Kramer, J. and Magee, J. 2006. Concurrency: State Models & Java Programs, 2nd Edition. Worldwide Series in Computer Science. John Wiley and Sons, Hoboken, NJ.","edition":"2"},{"key":"e_1_2_1_154_1","doi-asserted-by":"publisher","DOI":"10.1145\/63238.63240"},{"key":"e_1_2_1_155_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_156_1","doi-asserted-by":"publisher","DOI":"10.1145\/954666.971189"},{"key":"e_1_2_1_157_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_158_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_2"},{"key":"e_1_2_1_159_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_160_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.015"},{"key":"e_1_2_1_161_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.44"},{"key":"e_1_2_1_162_1","unstructured":"Leavens G. T. and Naumann D. A. 2006. Behavioral subtyping specification inheritance and modular reasoning. Tech. rep. 06-20b Department of Computer Science Iowa State University Ames IA. Leavens G. T. and Naumann D. A. 2006. Behavioral subtyping specification inheritance and modular reasoning. Tech. rep. 06-20b Department of Computer Science Iowa State University Ames IA."},{"key":"e_1_2_1_163_1","unstructured":"Leavens G. T. Poll E. Clifton C. Cheon Y. Ruby C. Cok D. R. M\u00fcller P. Kiniry J. Chalin P. and Zimmerman D. M. 2009. JML Reference Manual. http:\/\/www.jmlspecs.org. Leavens G. T. Poll E. Clifton C. Cheon Y. Ruby C. Cok D. R. M\u00fcller P. Kiniry J. Chalin P. and Zimmerman D. M. 2009. JML Reference Manual. http:\/\/www.jmlspecs.org."},{"key":"e_1_2_1_164_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178658"},{"key":"e_1_2_1_165_1","volume-title":"Proceedings of the 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'97)","volume":"1214","author":"Leavens G. T.","unstructured":"Leavens , G. T. and Wing , J. M . 1997. Protective interface specifications . In Proceedings of the 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'97) , M. Bidoit and M. Dauchet, Eds. Lecture Notes in Computer Science , vol. 1214 . Springer-Verlag, New York, NY, 520--534. Leavens, G. T. and Wing, J. M. 1997. Protective interface specifications. In Proceedings of the 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'97), M. Bidoit and M. Dauchet, Eds. Lecture Notes in Computer Science, vol. 1214. Springer-Verlag, New York, NY, 520--534."},{"key":"e_1_2_1_166_1","unstructured":"Leino K. R. M. 1995. Toward reliable modular programs. Ph.D. dissertation California Institute of Technology. Tech. rep. Caltech-CS-TR-95-03. Leino K. R. M. 1995. Toward reliable modular programs. Ph.D. dissertation California Institute of Technology. Tech. rep. Caltech-CS-TR-95-03."},{"key":"e_1_2_1_167_1","doi-asserted-by":"publisher","DOI":"10.1145\/286942.286953"},{"key":"e_1_2_1_168_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_1_169_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming (ECOOP), M. Odersky, Ed. Lecture Notes in Computer Science","volume":"3086","author":"Leino K. R. M.","unstructured":"Leino , K. R. M. and M\u00fcller , P . 2004. Object invariants in dynamic contexts . In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), M. Odersky, Ed. Lecture Notes in Computer Science , vol. 3086 . Springer-Verlag, Berlin, 491--516. Leino, K. R. M. and M\u00fcller, P. 2004. Object invariants in dynamic contexts. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), M. Odersky, Ed. Lecture Notes in Computer Science, vol. 3086. Springer-Verlag, Berlin, 491--516."},{"key":"e_1_2_1_170_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_9"},{"key":"e_1_2_1_171_1","volume-title":"Proceedings of the 17th European Symposium on Programming, Languages and Systems (ESOP), S. Drossopoulou, Ed. Lecture Notes in Computer Science","volume":"4960","author":"Leino K. R. M.","unstructured":"Leino , K. R. M. and M\u00fcller , P . 2008. Verification of equivalent-results methods . In Proceedings of the 17th European Symposium on Programming, Languages and Systems (ESOP), S. Drossopoulou, Ed. Lecture Notes in Computer Science , vol. 4960 . Springer-Verlag, Berlin, 307--321. Leino, K. R. M. and M\u00fcller, P. 2008. Verification of equivalent-results methods. In Proceedings of the 17th European Symposium on Programming, Languages and Systems (ESOP), S. Drossopoulou, Ed. Lecture Notes in Computer Science, vol. 4960. Springer-Verlag, Berlin, 307--321."},{"key":"e_1_2_1_172_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_2_1_173_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_7"},{"key":"e_1_2_1_174_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_17"},{"key":"e_1_2_1_175_1","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_1_176_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512559"},{"key":"e_1_2_1_177_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_2_1_178_1","unstructured":"Leino K. R. M. Saxe J. B. and Stata R. 1999. Checking Java programs via guarded commands. In Formal Techniques for Java Programs (FTfJP) B. Jacobs G. T. Leavens P. M\u00fcller and A. Poetzsch-Heffter Eds. Tech. rep. 251. FernUniversit\u00e4t Hagen Hagen Germany. Also available as Tech. note 1999-002 Compaq Systems Research Center. Leino K. R. M. Saxe J. B. and Stata R. 1999. Checking Java programs via guarded commands. In Formal Techniques for Java Programs (FTfJP) B. Jacobs G. T. Leavens P. M\u00fcller and A. Poetzsch-Heffter Eds. Tech. rep. 251. FernUniversit\u00e4t Hagen Hagen Germany. Also available as Tech. note 1999-002 Compaq Systems Research Center."},{"key":"e_1_2_1_179_1","doi-asserted-by":"publisher","DOI":"10.5555\/1030033.1030055"},{"key":"e_1_2_1_180_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"4421","author":"Leino K. R. M.","unstructured":"Leino , K. R. M. and Schulte , W . 2007. Using history invariants to verify observers. In Programming Languages and Systems (ESOP), R. D. Nicola , Ed. Lecture Notes in Computer Science , vol. 4421 . Springer-Verlag, Berlin, 80--94. Leino, K. R. M. and Schulte, W. 2007. Using history invariants to verify observers. In Programming Languages and Systems (ESOP), R. D. Nicola, Ed. Lecture Notes in Computer Science, vol. 4421. Springer-Verlag, Berlin, 80--94."},{"key":"e_1_2_1_181_1","doi-asserted-by":"publisher","DOI":"10.1145\/1342211.1342225"},{"key":"e_1_2_1_182_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_183_1","doi-asserted-by":"crossref","unstructured":"Leveson N. G. Heimdahl M. P. E. and Reese J. D. 1999. Designing specification languages for process control systems: Lessons learned and steps to the future. In Proceedings of the European Software Engineering Conference held jointly with the ACM SIGSOFT International Imposium on Foundations of Software Engineering O. Nierstrasz and M. Lemoine Eds. Lecture Notes in Computer Science vol. 1687. Springer-Verlag Berlin 127--145. Also ACM SIGSOFT Softw. Eng. Notes 24 6. Leveson N. G. Heimdahl M. P. E. and Reese J. D. 1999. Designing specification languages for process control systems: Lessons learned and steps to the future. In Proceedings of the European Software Engineering Conference held jointly with the ACM SIGSOFT International Imposium on Foundations of Software Engineering O. Nierstrasz and M. Lemoine Eds. Lecture Notes in Computer Science vol. 1687. Springer-Verlag Berlin 127--145. Also ACM SIGSOFT Softw. Eng. Notes 24 6.","DOI":"10.1145\/318774.318937"},{"key":"e_1_2_1_184_1","doi-asserted-by":"crossref","unstructured":"Lhotka R. 2008. Expert C&num; 2008 Business Objects. Apress New York NY. Lhotka R. 2008. Expert C&num; 2008 Business Objects. Apress New York NY.","DOI":"10.1007\/978-1-4302-1639-1"},{"key":"e_1_2_1_185_1","doi-asserted-by":"publisher","DOI":"10.1145\/62139.62141"},{"key":"e_1_2_1_186_1","unstructured":"Liskov B. and Guttag J. 1986. Abstraction and Specification in Program Development. The MIT Press Cambridge MA. Liskov B. and Guttag J. 1986. Abstraction and Specification in Program Development. The MIT Press Cambridge MA."},{"key":"e_1_2_1_187_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_188_1","doi-asserted-by":"crossref","unstructured":"Loeckx J. and Sieber K. 1987. The Foundations of Program Verification 2nd Edition. John Wiley and Sons New York NY. Loeckx J. and Sieber K. 1987. The Foundations of Program Verification 2nd Edition. John Wiley and Sons New York NY.","DOI":"10.1007\/978-3-322-96753-4"},{"key":"e_1_2_1_189_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming (ECOOP), E. Ernst, Ed. Lecture Notes in Computer Science","volume":"4609","author":"Lu Y.","unstructured":"Lu , Y. , Potter , J. , and Xue , J . 2007. Validity invariants and effects . In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), E. Ernst, Ed. Lecture Notes in Computer Science , vol. 4609 . Springer-Verlag, Berlin, 202--226. Lu, Y., Potter, J., and Xue, J. 2007. Validity invariants and effects. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), E. Ernst, Ed. Lecture Notes in Computer Science, vol. 4609. Springer-Verlag, Berlin, 202--226."},{"key":"e_1_2_1_190_1","volume-title":"A Language for Specifying Ada Programs. Texts and Monographs in Computer Science","author":"Luckham D.","unstructured":"Luckham , D. 1990. Programming with Specifications: An Introduction to Anna , A Language for Specifying Ada Programs. Texts and Monographs in Computer Science . Springer-Verlag, New York , NY. Luckham, D. 1990. Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs. Texts and Monographs in Computer Science. Springer-Verlag, New York, NY."},{"key":"e_1_2_1_191_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.230345"},{"key":"e_1_2_1_192_1","doi-asserted-by":"publisher","DOI":"10.1007\/11423348_11"},{"key":"e_1_2_1_193_1","unstructured":"Manasse M. S. and Nelson C. G. 1984. Correct compilation of control structures. Tech. rep. AT&T Bell Laboratories. Manasse M. S. and Nelson C. G. 1984. Correct compilation of control structures. Tech. rep. AT&T Bell Laboratories."},{"key":"e_1_2_1_194_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag New York NY. Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag New York NY.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_195_1","volume-title":"Odyssey Research Associates","author":"Marceau C.","unstructured":"Marceau , C. 1994. Penelope reference manual, version 3-3. Tech. rep. TM-94-0040 , Odyssey Research Associates , Inc., Ithaca, NY. Marceau, C. 1994. Penelope reference manual, version 3-3. Tech. rep. TM-94-0040, Odyssey Research Associates, Inc., Ithaca, NY."},{"key":"e_1_2_1_196_1","unstructured":"March\u00e9 C. 2009. The Krakatoa tool for deductive verification of Java programs. Winter School on Object-Oriented Verification Viinistu Estonia. http:\/\/krakatoa.lri.fr\/ws\/. March\u00e9 C. 2009. The Krakatoa tool for deductive verification of Java programs. Winter School on Object-Oriented Verification Viinistu Estonia. http:\/\/krakatoa.lri.fr\/ws\/."},{"key":"e_1_2_1_197_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_12"},{"key":"e_1_2_1_198_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2003.07.006"},{"key":"e_1_2_1_199_1","volume-title":"Mathematical Logic and Programming Languages","author":"Martin-L\u00f6f P.","unstructured":"Martin-L\u00f6f , P. 1985. Constructive mathematics and computer programming . In Mathematical Logic and Programming Languages . Prentice-Hall, Inc. , Englewood Cliffs, NJ ., 167--184. Martin-L\u00f6f, P. 1985. Constructive mathematics and computer programming. In Mathematical Logic and Programming Languages. Prentice-Hall, Inc., Englewood Cliffs, NJ., 167--184."},{"key":"e_1_2_1_200_1","volume-title":"Code Complete: A Practical Handbook of Software Construction","author":"McConnell S.","year":"1993","unstructured":"McConnell , S. 1993 . Code Complete: A Practical Handbook of Software Construction . Microsoft Press , Buffalo, NY . McConnell, S. 1993. Code Complete: A Practical Handbook of Software Construction. Microsoft Press, Buffalo, NY."},{"key":"e_1_2_1_201_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73577"},{"key":"e_1_2_1_202_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_203_1","volume-title":"Object-Oriented Software Construction","author":"Meyer B.","unstructured":"Meyer , B. 1997. Object-Oriented Software Construction , 2 nd ed. Prentice Hall, New York , NY. Meyer, B. 1997. Object-Oriented Software Construction, 2nd ed. Prentice Hall, New York, NY.","edition":"2"},{"key":"e_1_2_1_204_1","doi-asserted-by":"publisher","DOI":"10.1145\/322123.322134"},{"key":"e_1_2_1_205_1","volume-title":"Handbook of Theoretical Computer Science","author":"Milner R.","unstructured":"Milner , R. 1990. Operational and algebraic semantics of concurrent processes . In Handbook of Theoretical Computer Science , vol. B: Formal Models and Semantics. J. van Leewen, Ed. The MIT Press, New York, NY, 1201-- 1242 . Milner, R. 1990. Operational and algebraic semantics of concurrent processes. In Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics. J. van Leewen, Ed. The MIT Press, New York, NY, 1201--1242."},{"key":"e_1_2_1_206_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_207_1","series-title":"The Object-Oriented Series","volume-title":"Object-oriented specification in VDM++","author":"Mitra S.","unstructured":"Mitra , S. 1994. Object-oriented specification in VDM++ . In Object-Oriented Specification Case Studies, K. Lano and H. Haughton, Eds. The Object-Oriented Series . Prentice-Hall , New York, NY , 130--136. Mitra, S. 1994. Object-oriented specification in VDM++. In Object-Oriented Specification Case Studies, K. Lano and H. Haughton, Eds. The Object-Oriented Series. Prentice-Hall, New York, NY, 130--136."},{"key":"e_1_2_1_208_1","volume-title":"Programming from Specifications","author":"Morgan C.","unstructured":"Morgan , C. 1990. Programming from Specifications . Prentice Hall International, Hempstead , U.K. Morgan, C. 1990. Programming from Specifications. Prentice Hall International, Hempstead, U.K."},{"key":"e_1_2_1_209_1","volume-title":"Programming from Specifications","author":"Morgan C.","unstructured":"Morgan , C. 1994. Programming from Specifications , 2 nd Edition. Prentice Hall International, Hempstead , U.K. Morgan, C. 1994. Programming from Specifications, 2nd Edition. Prentice Hall International, Hempstead, U.K.","edition":"2"},{"key":"e_1_2_1_210_1","volume-title":"Eds","author":"Morgan C.","year":"1994","unstructured":"Morgan , C. and Vickers , T. , Eds . 1994 . On the Refinement Calculus. Formal Approaches of Computing and Information Technology Series. Springer-Verlag , New York, NY. Morgan, C. and Vickers, T., Eds. 1994. On the Refinement Calculus. Formal Approaches of Computing and Information Technology Series. Springer-Verlag, New York, NY."},{"key":"e_1_2_1_211_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380100402"},{"key":"e_1_2_1_212_1","doi-asserted-by":"crossref","unstructured":"Mossakowski T. Haxthausen A. E. Sanella D. and Tarlecki A. 2008. Casl\u2014The Common Algebraic Specification Language. In Logics of Specification Languages Springer-Verlag Berlin 241--298. Mossakowski T. Haxthausen A. E. Sanella D. and Tarlecki A. 2008. Casl\u2014The Common Algebraic Specification Language. In Logics of Specification Languages Springer-Verlag Berlin 241--298.","DOI":"10.1007\/978-3-540-74107-7_5"},{"key":"e_1_2_1_213_1","series-title":"Lecture Notes in Computer Science","volume-title":"Modular Specification and Verification of Object-Oriented Programs","author":"M\u00fcller P.","unstructured":"M\u00fcller , P. 2002. Modular Specification and Verification of Object-Oriented Programs . Lecture Notes in Computer Science , vol. 2262 . Springer-Verlag , Berlin . M\u00fcller, P. 2002. Modular Specification and Verification of Object-Oriented Programs. Lecture Notes in Computer Science, vol. 2262. Springer-Verlag, Berlin."},{"key":"e_1_2_1_214_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.713"},{"key":"e_1_2_1_215_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"e_1_2_1_216_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00215-5"},{"key":"e_1_2_1_217_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.02.004"},{"key":"e_1_2_1_218_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234745"},{"key":"e_1_2_1_219_1","volume-title":"The Common Object Request Broker: Architecture and Specification, 1.1 ed","author":"Object Management Group","unstructured":"Object Management Group . 1992. The Common Object Request Broker: Architecture and Specification, 1.1 ed . Object Management Group, Inc. , Framingham, MA . Object Management Group. 1992. The Common Object Request Broker: Architecture and Specification, 1.1 ed. Object Management Group, Inc., Framingham, MA."},{"key":"e_1_2_1_220_1","doi-asserted-by":"publisher","DOI":"10.1145\/190679.190681"},{"key":"e_1_2_1_221_1","volume-title":"Proceedings of the Workshop on Computer Science Logic. Lecture Notes in Computer Science","volume":"2142","author":"O'Hearn P.","unstructured":"O'Hearn , P. , Reynolds , J. , and Yang , H . 2001. Local reasoning about programs that alter data structures . In Proceedings of the Workshop on Computer Science Logic. Lecture Notes in Computer Science , vol. 2142 . Springer-Verlag, Berlin, 1--19. O'Hearn, P., Reynolds, J., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Proceedings of the Workshop on Computer Science Logic. Lecture Notes in Computer Science, vol. 2142. Springer-Verlag, Berlin, 1--19."},{"key":"e_1_2_1_222_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_223_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_2_1_224_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90009-9"},{"key":"e_1_2_1_225_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.03.082"},{"key":"e_1_2_1_226_1","unstructured":"OMG. 2006. Object constraint language specification version 2.0. http:\/\/tinyurl.com\/k7rfm. OMG. 2006. Object constraint language specification version 2.0. http:\/\/tinyurl.com\/k7rfm."},{"key":"e_1_2_1_227_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.33"},{"key":"e_1_2_1_228_1","volume-title":"Axiomatic Proof Techniques for Parallel Programs. Outstanding Dissertations in the Computer Sciences","author":"Owicki S. S.","unstructured":"Owicki , S. S. 1975. Axiomatic Proof Techniques for Parallel Programs. Outstanding Dissertations in the Computer Sciences . Garland Publishing, New York , NY. Owicki, S. S. 1975. Axiomatic Proof Techniques for Parallel Programs. Outstanding Dissertations in the Computer Sciences. Garland Publishing, New York, NY."},{"key":"e_1_2_1_229_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_1_230_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328451"},{"key":"e_1_2_1_231_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.52"},{"key":"e_1_2_1_233_1","doi-asserted-by":"publisher","DOI":"10.1145\/361598.361623"},{"key":"e_1_2_1_234_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.241769"},{"key":"e_1_2_1_235_1","doi-asserted-by":"publisher","DOI":"10.1145\/356914.356917"},{"key":"e_1_2_1_236_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168630"},{"key":"e_1_2_1_237_1","doi-asserted-by":"publisher","DOI":"10.1145\/356698.356702"},{"key":"e_1_2_1_238_1","volume-title":"Petri Net Theory and the Modeling of Systems","author":"Peterson J. L.","unstructured":"Peterson , J. L. 1981. Petri Net Theory and the Modeling of Systems . Prentice Hall, Englewood Cliffs , NJ. Peterson, J. L. 1981. Petri Net Theory and the Modeling of Systems. Prentice Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_239_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_2_1_240_1","unstructured":"Pilkiewicz A. and Pottier F. 2009. The essence of monotonic state. http:\/\/gallium.inria.fr\/~fpottier\/publis\/pilkiewicz-pottier-monotonicity-2009.pdf. Pilkiewicz A. and Pottier F. 2009. The essence of monotonic state. http:\/\/gallium.inria.fr\/~fpottier\/publis\/pilkiewicz-pottier-monotonicity-2009.pdf."},{"key":"e_1_2_1_241_1","volume-title":"Specification and verification of object-oriented programs. Habilitation thesis","author":"Poetzsch-Heffter A.","unstructured":"Poetzsch-Heffter , A. 1997. Specification and verification of object-oriented programs. Habilitation thesis , Technical University of Munich , Munich, Germany . Poetzsch-Heffter, A. 1997. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, Munich, Germany."},{"key":"e_1_2_1_242_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP'99)","volume":"1576","author":"Poetzsch-Heffter A.","unstructured":"Poetzsch-Heffter , A. and M\u00fcller , P . 1999. A programming logic for sequential Java . In Proceedings of the European Symposium on Programming (ESOP'99) , S. D. Swierstra, Ed. Lecture Notes in Computer Science , vol. 1576 . Springer-Verlag, Berlin, 162--176. Poetzsch-Heffter, A. and M\u00fcller, P. 1999. A programming logic for sequential Java. In Proceedings of the European Symposium on Programming (ESOP'99), S. D. Swierstra, Ed. Lecture Notes in Computer Science, vol. 1576. Springer-Verlag, Berlin, 162--176."},{"key":"e_1_2_1_243_1","volume-title":"Proceedings of the Oxford-Microsoft Symposium in Honor of Sir Tony Hoare.","author":"Reynolds J.","year":"2000","unstructured":"Reynolds , J. 2000 . Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science , Proceedings of the Oxford-Microsoft Symposium in Honor of Sir Tony Hoare. Reynolds, J. 2000. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, Proceedings of the Oxford-Microsoft Symposium in Honor of Sir Tony Hoare."},{"key":"e_1_2_1_244_1","volume-title":"The Craft of Programming","author":"Reynolds J. C.","unstructured":"Reynolds , J. C. 1981. The Craft of Programming . Prentice-Hall International, Englewood Cliffs , NJ. Reynolds, J. C. 1981. The Craft of Programming. Prentice-Hall International, Englewood Cliffs, NJ."},{"key":"e_1_2_1_245_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_246_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_24"},{"key":"e_1_2_1_247_1","volume-title":"A Classical Mind: Essays in Honour of C. A. R. Hoare","author":"Roscoe A. W.","unstructured":"Roscoe , A. W. 1994. Model-checking CSP . In A Classical Mind: Essays in Honour of C. A. R. Hoare . Prentice Hall International Ltd ., Hertfordshire, U.K., 353--378. Roscoe, A. W. 1994. Model-checking CSP. In A Classical Mind: Essays in Honour of C. A. R. Hoare. Prentice Hall International Ltd., Hertfordshire, U.K., 353--378."},{"key":"e_1_2_1_248_1","doi-asserted-by":"publisher","DOI":"10.1145\/353171.353186"},{"key":"e_1_2_1_249_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_7"},{"key":"e_1_2_1_250_1","unstructured":"Rumbaugh J. Jacobson I. and Booch G. 1999. The Unified Modeling Language Refrence Manual. Object Technology Series. Addison Wesley Longman Reading MA. Rumbaugh J. Jacobson I. and Booch G. 1999. The Unified Modeling Language Refrence Manual. Object Technology Series. Addison Wesley Longman Reading MA."},{"key":"e_1_2_1_251_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_14"},{"key":"e_1_2_1_252_1","series-title":"Foundations of Computing Series","volume-title":"The Structure of Typed Programming Languages","author":"Schmidt D. A.","unstructured":"Schmidt , D. A. 1994. The Structure of Typed Programming Languages . Foundations of Computing Series . The MIT Press , Cambridge, MA . Schmidt, D. A. 1994. The Structure of Typed Programming Languages. Foundations of Computing Series. The MIT Press, Cambridge, MA."},{"key":"e_1_2_1_253_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_1_254_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297053"},{"key":"e_1_2_1_255_1","unstructured":"Smans J. Jacobs B. and Piessens F. 2008a. Implicit dynamic frames. In Formal Techniques for Java-like Programs M. Huisman Ed. Radboud University Nijmegen 1--12. Tech. rep. ICIS-R08013 Radboud University Nijmegen. Smans J. Jacobs B. and Piessens F. 2008a. Implicit dynamic frames. In Formal Techniques for Java-like Programs M. Huisman Ed. Radboud University Nijmegen 1--12. Tech. rep. ICIS-R08013 Radboud University Nijmegen."},{"key":"e_1_2_1_256_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68863-1_14"},{"key":"e_1_2_1_257_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_2_1_258_1","volume-title":"Lecture Notes in Computer Science","volume":"4961","author":"Smans J.","unstructured":"Smans , J. , Jacobs , B. , Piessens , F. , and Schulte , W . 2008. An automatic verifier for Java-like programs based on dynamic frames. In Fundamental Approaches to Software Engineering . Lecture Notes in Computer Science , vol. 4961 . Springer-Verlag, Berlin, 261--275. Smans, J., Jacobs, B., Piessens, F., and Schulte, W. 2008. An automatic verifier for Java-like programs based on dynamic frames. In Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science, vol. 4961. Springer-Verlag, Berlin, 261--275."},{"key":"e_1_2_1_259_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1989.0006"},{"key":"e_1_2_1_260_1","volume-title":"Real-Time Systems: Abstractions, Languages, and Design Methodologies","author":"Stoyenko A.","unstructured":"Stoyenko , A. 1992. The evolution and state-of-the-art of real-time languages . In Real-Time Systems: Abstractions, Languages, and Design Methodologies , K. M. Kavi, Ed. IEEE Computer Society Press , Los Alamitos , California, 394--416. Stoyenko, A. 1992. The evolution and state-of-the-art of real-time languages. In Real-Time Systems: Abstractions, Languages, and Design Methodologies, K. M. Kavi, Ed. IEEE Computer Society Press, Los Alamitos, California, 394--416."},{"key":"e_1_2_1_261_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337184"},{"key":"e_1_2_1_262_1","unstructured":"von Oheimb D. 2001. Analyzing Java in Isabelle\/HOL: Formalization type safety and Hoare logic. Ph.D. disssetation Technische Universit\u00e4t M\u00fcnchen. von Oheimb D. 2001. Analyzing Java in Isabelle\/HOL: Formalization type safety and Hoare logic. Ph.D. disssetation Technische Universit\u00e4t M\u00fcnchen."},{"key":"e_1_2_1_263_1","unstructured":"Walrath K. Campione M. Huml A. and Zakhour S. 2004. The JFC Swing Tutorial: A Guide to Constructing GUIs. Prentice Hall Upper Saddle River NJ. Walrath K. Campione M. Huml A. and Zakhour S. 2004. The JFC Swing Tutorial: A Guide to Constructing GUIs. Prentice Hall Upper Saddle River NJ."},{"key":"e_1_2_1_264_1","unstructured":"Warmer J. and Kleppe A. 1999. The Object Constraint Language: Precise Modeling with UML. Addison Wesley Longman Reading MA. Warmer J. and Kleppe A. 1999. The Object Constraint Language: Precise Modeling with UML. Addison Wesley Longman Reading MA."},{"key":"e_1_2_1_265_1","doi-asserted-by":"publisher","DOI":"10.1145\/9758.10500"},{"key":"e_1_2_1_266_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_2_1_267_1","series-title":"Foundations of Computer Science Series","volume-title":"The Formal Semantics of Programming Languages","author":"Winskel G.","unstructured":"Winskel , G. 1993. The Formal Semantics of Programming Languages . Foundations of Computer Science Series . The MIT Press , Cambridge, MA . Winskel, G. 1993. The Formal Semantics of Programming Languages. Foundations of Computer Science Series. The MIT Press, Cambridge, MA."},{"key":"e_1_2_1_268_1","volume-title":"Handbook of Theoretical Computer Science","author":"Wirsing M.","unstructured":"Wirsing , M. 1990. Algebraic specification . In Handbook of Theoretical Computer Science , vol. B: Formal Models and Semantics, J. van Leewen, Ed. The MIT Press, New York, NY, 675-- 788 . Wirsing, M. 1990. Algebraic specification. In Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, J. van Leewen, Ed. The MIT Press, New York, NY, 675--788."},{"key":"e_1_2_1_269_1","doi-asserted-by":"crossref","unstructured":"Woodcock J. Saaltink M. and Freitas L. 2009. Unifying theories of undefinedness. In Summer School Marktoberdorf 2008: Engineering Methods and Tools for Software Safety and Security. NATO ASI Series F. IOS Press Amsterdam. Forthcoming. Woodcock J. Saaltink M. and Freitas L. 2009. Unifying theories of undefinedness. In Summer School Marktoberdorf 2008: Engineering Methods and Tools for Software Safety and Security. NATO ASI Series F. IOS Press Amsterdam. Forthcoming.","DOI":"10.3233\/978-1-58603-976-9-311"},{"key":"e_1_2_1_270_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211617"},{"key":"e_1_2_1_271_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2187671.2187678","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2187671.2187678","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:33Z","timestamp":1750241193000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2187671.2187678"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":269,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["10.1145\/2187671.2187678"],"URL":"https:\/\/doi.org\/10.1145\/2187671.2187678","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6]]},"assertion":[{"value":"2010-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-06-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}