{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:39Z","timestamp":1775873679190,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642175107","type":"print"},{"value":"9783642175114","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17511-4_20","type":"book-chapter","created":{"date-parts":[[2010,12,7]],"date-time":"2010-12-07T06:24:40Z","timestamp":1291703080000},"page":"348-370","source":"Crossref","is-referenced-by-count":551,"title":["Dafny: An Automatic Program Verifier for Functional Correctness"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-45236-2_5","volume-title":"FME 2003: Formal Methods","author":"J.-R. Abrial","year":"2003","unstructured":"Abrial, J.-R.: Event based sequential program development: Application to constructing a pointer program. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 51\u201374. Springer, Heidelberg (2003)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-540-70592-5_17","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"A. Banerjee","year":"2008","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 387\u2013411. Springer, Heidelberg (2008)"},{"key":"20_CR3","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)"},{"issue":"6","key":"20_CR4","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6), 27\u201356 (2004)","journal-title":"Journal of Object Technology"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"20_CR6","unstructured":"Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2008), www.SMT-LIB.org"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"20_CR8","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: The KeY Approach. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Bevier, W.R., Hunt, Jr., W.A., Moore, J.S., Young, W.D.: Special issue on system verification. Journal of Automated Reasoning\u00a05(4), 409\u2013530 (1989)","DOI":"10.1007\/BF00243131"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"issue":"3","key":"20_CR11","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/357172.357175","volume":"4","author":"M. Broy","year":"1982","unstructured":"Broy, M., Pepper, P.: Combining algebraic and algorithmic reasoning: An approach to the Schorr-Waite algorithm. ACM TOPLAS\u00a04(3), 362\u2013381 (1982)","journal-title":"ACM TOPLAS"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Bubel, R.: The Schorr-Waite-algorithm. In: [7], ch. 15","DOI":"10.1007\/978-3-540-69061-0_15"},{"key":"20_CR13","first-page":"292","volume-title":"OOPSLA 2002","author":"D. Clarke","year":"2002","unstructured":"Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA 2002, pp. 292\u2013310. ACM, New York (2002)"},{"key":"20_CR14","first-page":"48","volume-title":"OOPSLA 1998","author":"D. Clarke","year":"1998","unstructured":"Clarke, D., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA 1998, pp. 48\u201364. ACM, New York (1998)"},{"key":"20_CR15","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.A., 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.) Theorem Proving in Higher Order Logics. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"20_CR17","unstructured":"Darvas, \u00c1.P.: Reasoning About Data Abstraction in Contract Languages. PhD thesis, ETH Zurich, Diss. ETH No. 18622 (2009)"},{"key":"20_CR18","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)"},{"issue":"3","key":"20_CR19","first-page":"365","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J.\u00a0ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J.\u00a0ACM"},{"key":"20_CR20","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (1998)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"20_CR22","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":"20_CR23","first-page":"234","volume-title":"PLDI 2002","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI 2002, pp. 234\u2013245. ACM, New York (2002)"},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/3-540-61474-5_103","volume-title":"Computer Aided Verification","author":"G. Gonthier","year":"1996","unstructured":"Gonthier, G.: Verifying the safety of a practical concurrent garbage collector. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 462\u2013465. Springer, Heidelberg (1996)"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-05089-3_22","volume-title":"FM 2009: Formal Methods","author":"J. Hoenicke","year":"2009","unstructured":"Hoenicke, J., Leino, K.R.M., Podelski, A., Sch\u00e4f, M., Wies, T.: It\u2019s doomed; we can prove it. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 338\u2013353. Springer, Heidelberg (2009)"},{"key":"20_CR26","first-page":"190","volume-title":"SEFM 2005","author":"T. Hubert","year":"2005","unstructured":"Hubert, T., March\u00e9, C.: A case study of C source code verification: the Schorr-Waite algorithm. In: SEFM 2005, pp. 190\u2013199. IEEE, Los Alamitos (2005)"},{"key":"20_CR27","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (2008)"},{"key":"20_CR28","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":"20_CR29","first-page":"207","volume-title":"SOSP 2009","author":"G. Klein","year":"2009","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: SOSP 2009, pp. 207\u2013220. ACM, New York (2009)"},{"issue":"3","key":"20_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes\u00a031(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"20_CR31","unstructured":"Leino, K.R.M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, Technical Report Caltech-CS-TR-95-03 (1995)"},{"key":"20_CR32","first-page":"144","volume-title":"OOPSLA 1998","author":"K.R.M. Leino","year":"1998","unstructured":"Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: OOPSLA 1998, pp. 144\u2013153. ACM, New York (1998)"},{"key":"20_CR33","unstructured":"Leino, K.R.M.: This is Boogie 2. Manuscript KRML 178 (2008), http:\/\/research.microsoft.com\/~leino\/papers.html"},{"key":"20_CR34","series-title":"NATO Science for Peace and Security Series D: Information and Communication Security","first-page":"231","volume-title":"Engineering Methods and Tools for Software Safety and Security","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M.: Specification and verification of object-oriented software. In: Engineering Methods and Tools for Software Safety and Security. NATO Science for Peace and Security Series D: Information and Communication Security, vol.\u00a022, pp. 231\u2013266. IOS Press, Amsterdam (2009); Summer School Marktoberdorf 2008 lecture notes"},{"key":"20_CR35","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: Shin, S.Y., Ossowski, S. (eds.) SAC 2009. LNCS, vol.\u00a05867, pp. 615\u2013622. Springer, Heidelberg (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"20_CR36","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":"20_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-78739-6_24","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2008","unstructured":"Leino, K.R.M., M\u00fcller, P.: Verification of equivalent-results methods. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 307\u2013321. Springer, Heidelberg (2008)"},{"key":"20_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, Springer, Heidelberg (2009)"},{"key":"20_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-13010-6_4","volume-title":"Advanced Lectures on Software Engineering","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., M\u00fcller, P.: Using the Spec# language, methodology, and tools to write bug-free programs. In: M\u00fcller, P. (ed.) Advanced Lectures on Software Engineering. LNCS, vol.\u00a06029, pp. 91\u2013139. Springer, Heidelberg (2010)"},{"issue":"5","key":"20_CR40","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/570886.570888","volume":"24","author":"K.R.M. Leino","year":"2002","unstructured":"Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM TOPLAS\u00a024(5), 491\u2013553 (2002)","journal-title":"ACM TOPLAS"},{"key":"20_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol.\u00a06015, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"issue":"1-2","key":"20_CR42","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F. Mehta","year":"2005","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Information and Computation\u00a0199(1-2), 200\u2013227 (2005); 19th International Conference on Automated Deduction (CADE-19)","journal-title":"Information and Computation"},{"key":"20_CR43","series-title":"Series in Computer Science.International","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1988","unstructured":"Meyer, B.: Object-oriented Software Construction. Series in Computer Science.International. Prentice-Hall International, Englewood Cliffs (1988)"},{"key":"20_CR44","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.scico.2006.03.001","volume":"62","author":"P. M\u00fcller","year":"2006","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming\u00a062, 253\u2013286 (2006)","journal-title":"Science of Computer Programming"},{"key":"20_CR45","first-page":"247","volume-title":"POPL 2005","author":"M.J. Parkinson","year":"2005","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: POPL 2005, pp. 247\u2013258. ACM, New York (2005)"},{"key":"20_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-70594-9_17","volume-title":"Mathematics of Program Construction","author":"Y. R\u00e9gis-Gianas","year":"2008","unstructured":"R\u00e9gis-Gianas, Y., Pottier, F.: A Hoare logic for call-by-value functional programs. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol.\u00a05133, pp. 305\u2013335. Springer, Heidelberg (2008)"},{"key":"20_CR47","first-page":"55","volume-title":"LICS 2002","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE, Los Alamitos (2002)"},{"issue":"8","key":"20_CR48","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/363534.363554","volume":"10","author":"H. Schorr","year":"1967","unstructured":"Schorr, H., Waite, W.M.: An efficient machine-independent procedure for garbage collection in various list structures. Commun. ACM\u00a010(8), 501\u2013506 (1967)","journal-title":"Commun. ACM"},{"key":"20_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-68863-1_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"J. Smans","year":"2008","unstructured":"Smans, J., Jacobs, B., Piessens, F.: VeriCool: An automatic verifier for a concurrent object-oriented language. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 220\u2013239. Springer, Heidelberg (2008)"},{"key":"20_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-03013-0_8","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"J. Smans","year":"2009","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol.\u00a05653, pp. 148\u2013172. Springer, Heidelberg (2009)"},{"key":"20_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-540-78743-3_19","volume-title":"Fundamental Approaches to Software Engineering","author":"J. Smans","year":"2008","unstructured":"Smans, J., Jacobs, B., Piessens, F., Schulte, W.: Automatic verifier for Java-like programs based on dynamic frames. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, pp. 261\u2013275. Springer, Heidelberg (2008)"},{"key":"20_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-87873-5_10","volume-title":"Verified Software: Theories, Tools, Experiments","author":"B.W. Weide","year":"2008","unstructured":"Weide, B.W., Sitaraman, M., Harton, H.K., Adcock, B., Bucci, P., Bronish, D., Heym, W.D., Kirschenbaum, J., Frazier, D.: Incremental benchmarks for software verification tools and techniques. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 84\u201398. Springer, Heidelberg (2008)"},{"key":"20_CR53","first-page":"349","volume-title":"PLDI 2008","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: PLDI 2008, pp. 349\u2013361. ACM, New York (2008)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17511-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T21:20:15Z","timestamp":1559856015000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17511-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642175107","9783642175114"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}