{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T04:13:40Z","timestamp":1761970420517,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642317613"},{"type":"electronic","value":"9783642317620"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31762-0_2","type":"book-chapter","created":{"date-parts":[[2012,7,11]],"date-time":"2012-07-11T10:09:11Z","timestamp":1342001351000},"page":"3-21","source":"Crossref","is-referenced-by-count":22,"title":["The COST IC0701 Verification Competition 2011"],"prefix":"10.1007","author":[{"given":"Thorsten","family":"Bormer","sequence":"first","affiliation":[]},{"given":"Marc","family":"Brockschmidt","sequence":"additional","affiliation":[]},{"given":"Dino","family":"Distefano","sequence":"additional","affiliation":[]},{"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[]},{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"additional","affiliation":[]},{"given":"Radu","family":"Grigore","sequence":"additional","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"Vladimir","family":"Klebanov","sequence":"additional","affiliation":[]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[]},{"given":"Rosemary","family":"Monahan","sequence":"additional","affiliation":[]},{"given":"Wojciech","family":"Mostowski","sequence":"additional","affiliation":[]},{"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Scheben","sequence":"additional","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Bogdan","family":"Tofan","sequence":"additional","affiliation":[]},{"given":"Julian","family":"Tschannen","sequence":"additional","affiliation":[]},{"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"2_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroc\u0142aw, Poland (August 2011)","key":"2_CR3"},{"unstructured":"Brockschmidt, M., Otto, C., Giesl, J.: Modular termination proofs of recursive Java Bytecode programs by term rewriting. In: Proc. RTA\u00a0 2011. LIPIcs, vol.\u00a010, pp. 155\u2013170 (2011)","key":"2_CR4"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/1449764.1449782","volume-title":"Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications, OOPSLA 2008","author":"D. Distefano","year":"2008","unstructured":"Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications, OOPSLA 2008, pp. 213\u2013226. ACM, New York (2008)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02348-4_3","volume-title":"Rewriting Techniques and Applications","author":"C. Fuhs","year":"2009","unstructured":"Fuhs, C., Giesl, J., Pl\u00fccker, M., Schneider-Kamp, P., Falke, S.: Proving Termination of Integer Term Rewriting. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 32\u201347. Springer, Heidelberg (2009)"},{"key":"2_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"unstructured":"Kaldewaij, A.: Programming: the derivation of algorithms. Prentice-Hall, Inc. (1990)","key":"2_CR10"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"I.T. Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 268\u2013283. Springer, Heidelberg (2006)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V. Klebanov","year":"2011","unstructured":"Klebanov, V., M\u00fcller, P., Shankar, N., Leavens, G.T., W\u00fcstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Wei\u00df, B.: The 1st Verified Software Competition: Experience Report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 154\u2013168. Springer, Heidelberg (2011)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An Automatic Program Verifier for Functional Correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"unstructured":"Moy, Y., March\u00e9, C.: The Jessie plugin for Deduction Verification in Frama-C \u2014 Tutorial and Reference Manual. INRIA & LRI (2011), \n                    \n                      http:\/\/krakatoa.lri.fr\/","key":"2_CR14"},{"doi-asserted-by":"crossref","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, vol.\u00a0II.1, pp. 13\u201339. Kluwer (1998)","key":"2_CR15","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-642-18070-5_10","volume-title":"Formal Verification of Object-Oriented Software","author":"P.H. Schmitt","year":"2011","unstructured":"Schmitt, P.H., Ulbrich, M., Wei\u00df, B.: Dynamic Frames in Java Dynamic Logic. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol.\u00a06528, pp. 138\u2013152. Springer, Heidelberg (2011)"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-27815-3_37","volume-title":"Algebraic Methodology and Software Technology","author":"K. Stenzel","year":"2004","unstructured":"Stenzel, K.: A Formally Verified Calculus for Full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 491\u2013505. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Verification of Object-Oriented Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31762-0_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:47:36Z","timestamp":1620128856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31762-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642317613","9783642317620"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31762-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}