{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:45:42Z","timestamp":1772163942210,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,10,21]],"date-time":"2007-10-21T00:00:00Z","timestamp":1192924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2007,10,21]]},"DOI":"10.1145\/1297027.1297053","type":"proceedings-article","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T09:30:20Z","timestamp":1195119020000},"page":"351-368","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Modular verification of higher-order methods with mandatory calls specified by model programs"],"prefix":"10.1145","author":[{"given":"Steve M.","family":"Shaner","sequence":"first","affiliation":[{"name":"Iowa State University, Ames, IA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[{"name":"Iowa State University, Ames, IA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David A.","family":"Naumann","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, Hoboken, NJ"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,10,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"P.\n       \n      America\n    .\n      \n  \n   \n  Designing an object-oriented programming language with behavioural subtyping. In J. W. de Bakker W. P. de Roever and G. Rozenberg editors Foundations of Object-Oriented Languages REX School\/Workshop Noordwijkerhout The\n   Netherlands May\/June \n  1990 volume \n  489\n   of \n  Lecture Notes in Computer Science pages \n  60\n  --\n  90\n  . \n  Springer-Verlag New York NY 1991.   P. America. Designing an object-oriented programming language with behavioural subtyping. In J. W. de Bakker W. P. de Roever and G. Rozenberg editors Foundations of Object-Oriented Languages REX School\/Workshop Noordwijkerhout The Netherlands May\/June 1990 volume 489 of Lecture Notes in Computer Science pages 60--90. Springer-Verlag New York NY 1991.","DOI":"10.1007\/BFb0019440"},{"key":"e_1_3_2_1_2_1","volume-title":"Graduate Texts in Computer Science. Springer-Verlag","author":"Back R.-J.","year":"1998"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101821.1101824"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(02)00041-9"},{"key":"e_1_3_2_1_6_1","volume-title":"Springer-Verlag","author":"Beckert B.","year":"2007"},{"key":"e_1_3_2_1_8_1","volume-title":"Workshop on Foundations of Component-Based Systems","author":"B\u00fcchi M.","year":"1997"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.879810"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1123058.1123068"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264295"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"F. S.\n       \n      de Boer\n    .\n      \n  \n   \n  A WP-calculus for OO. In W. Thomas editor Foundations of Software Science and Computation Structures (FOSSACS) volume \n  1578\n   of \n  Lecture Notes in Computer Science pages \n  135\n  --\n  149\n  . \n  Springer-Verlag 1999\n     F. S. de Boer. A WP-calculus for OO. In W. Thomas editor Foundations of Software Science and Computation Structures (FOSSACS) volume 1578 of Lecture Notes in Computer Science pages 135--149. Springer-Verlag 1999","DOI":"10.1007\/3-540-49019-1_10"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/227726.227772"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264436"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_18_1","volume-title":"Mass.","author":"Gamma E.","year":"1995"},{"key":"e_1_3_2_1_19_1","volume-title":"Experiments (VSTTE)","author":"Hehner E. C. R.","year":"2005"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059696"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320395"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_2"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0026-7"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.44"},{"key":"e_1_3_2_1_29_1","unstructured":"G. T. Leavens E. Poll C. Clifton Y. Cheon C. Ruby D. R. Cok P. M\u00fcller J. Kiniry and P. Chalin. JML Reference Manual. Department of Computer Science Iowa State University. Available from http:\/\/www.jmlspecs.org Feb. 2007.  G. T. Leavens E. Poll C. Clifton Y. Cheon C. Ruby D. R. Cok P. M\u00fcller J. Kiniry and P. Chalin. JML Reference Manual. Department of Computer Science Iowa State University. Available from http:\/\/www.jmlspecs.org Feb. 2007."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178658"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286953"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(88)90062-7"},{"key":"e_1_3_2_1_34_1","volume-title":"Prentice Hall International","author":"Morgan C.","year":"1994"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"P.\n       \n      M\u00fcller\n    .\n      \n  \n   \n  Modular Specification and Verification of Object-Oriented Programs volume \n  2262\n   of \n  Lecture Notes in Computer Science\n  . \n  Springer-Verlag 2002\n  .  P. M\u00fcller. Modular Specification and Verification of Object-Oriented Programs volume 2262 of Lecture Notes in Computer Science. Springer-Verlag 2002.","DOI":"10.1007\/3-540-45651-1"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_14"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90009-9"},{"key":"e_1_3_2_1_39_1","volume-title":"Universiteit Utrecht","author":"Pierik C.","year":"2006"},{"key":"e_1_3_2_1_40_1","unstructured":"A. Poetzsch-Heffter P. M\u00fcller and J. Sch\u00e4fer. The Jive tool. http:\/\/tinyurl.com\/3cke34 Apr. 2006. Checked August 2 2006.  A. Poetzsch-Heffter P. M\u00fcller and J. Sch\u00e4fer. The Jive tool. http:\/\/tinyurl.com\/3cke34 Apr. 2006. Checked August 2 2006."},{"key":"e_1_3_2_1_41_1","volume-title":"Mass.","author":"Roy P. V.","year":"2004"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"N.\n       \n      Soundarajan\n     and \n      \n      \n      S.\n       \n      Fridella\n      \n  \n  . \n  Incremental reasoning for object oriented systems. In O. Owe S. Krogdahl and T. Lyche editors From Object-Orientation to Formal Methods Essays in Memory of Ole-Johan Dahl volume \n  2635\n   of \n  Lecture Notes in Computer Science pages \n  302\n  --\n  333\n  . \n  Springer-Verlag 2004\n  .  N. Soundarajan and S. Fridella. Incremental reasoning for object oriented systems. In O. Owe S. Krogdahl and T. Lyche editors From Object-Orientation to Formal Methods Essays in Memory of Ole-Johan Dahl volume 2635 of Lecture Notes in Computer Science pages 302--333. Springer-Verlag 2004.","DOI":"10.1007\/978-3-540-39993-3_15"}],"event":{"name":"OOPSLA07: ACM SIGPLAN Object Oriented Programming Systems and Applications Conference","location":"Montreal Quebec Canada","acronym":"OOPSLA07","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1297027.1297053","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1297027.1297053","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:58:27Z","timestamp":1750244307000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1297027.1297053"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,21]]},"references-count":37,"alternative-id":["10.1145\/1297027.1297053","10.1145\/1297027"],"URL":"https:\/\/doi.org\/10.1145\/1297027.1297053","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1297105.1297053","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2007,10,21]]},"assertion":[{"value":"2007-10-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}