{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T11:48:22Z","timestamp":1725709702986},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357459"},{"type":"electronic","value":"9783642357466"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35746-6_6","type":"book-chapter","created":{"date-parts":[[2012,12,13]],"date-time":"2012-12-13T20:38:40Z","timestamp":1355431120000},"page":"156-181","source":"Crossref","is-referenced-by-count":6,"title":["Using Dafny, an Automatic Program Verifier"],"prefix":"10.1007","author":[{"given":"Luke","family":"Herbert","sequence":"first","affiliation":[]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[]},{"given":"Jose","family":"Quaresma","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_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":"6_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., et al.: Specification and verification: The Spec# experience. Communications of the ACM\u00a054(6), 81\u201391 (2011) ISSN: 0001-0782, doi:10.1145\/1953122.1953145","DOI":"10.1145\/1953122.1953145"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A Practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576\u2013580 (1969) ISSN: 0001-0782, doi:10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"6_CR5","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., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 268\u2013283. Springer, Heidelberg (2006)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Kassios, I.T.: The dynamic frames theory. Formal Aspects of Computing\u00a023, 267\u2013288 (2011) ISSN: 0934-5043, doi:10.1007\/s00165-010-0152-5","DOI":"10.1007\/s00165-010-0152-5"},{"key":"6_CR7","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":"6_CR8","unstructured":"Koenig, J.: Dafny Guide. Microsoft Research (2011), \n                  \n                    http:\/\/rise4fun.com\/Dafny\/tutorial\/guide\n                  \n                  \n                 (visited on January 30, 2012)"},{"key":"6_CR9","unstructured":"Koenig, J., Leino, K.R.M.: Getting started with Dafny: A Guide. Summer School Marktoberdorf 2011 Lecture Notes. IOS Press (to appear, 2012)"},{"key":"6_CR10","unstructured":"Leino, K.R.M.: Specification and verification of object-oriented software. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security. NATO Science for Peace and Security Series D: Information and Communication Security. Summer School Marktoberdorf 2008 Lecture Notes, vol.\u00a022, pp. 231\u2013266. IOS Press (2009)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An Automatic Program Verifier for Functional Correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS (LNAI), vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-15057-9_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., Monahan, R.: Dafny Meets the Verification Benchmarks Challenge. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 112\u2013126. Springer, Heidelberg (2010)"},{"key":"6_CR13","unstructured":"Meyer, B.: Object-oriented Software Construction. Series in Computer Science. Prentice-Hall International (1988)"},{"key":"6_CR14","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":"6_CR15","unstructured":"Wei\u00df, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. PhD thesis, Karlsruhe Institute of Technology (2011)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Wiles, A.: Modular elliptic curves and Fermat\u2019s last theorem. The Annals of Mathematics\u00a0141(3), 443\u2013551 (1995) ISSN: 0003486X, doi:10.2307\/2118559","DOI":"10.2307\/2118559"}],"container-title":["Lecture Notes in Computer Science","Tools for Practical Software Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35746-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,9]],"date-time":"2019-05-09T20:14:28Z","timestamp":1557432868000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35746-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642357459","9783642357466"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35746-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}