{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T06:43:15Z","timestamp":1770964995961,"version":"3.50.1"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319192482","type":"print"},{"value":"9783319192499","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_26","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"414-434","source":"Crossref","is-referenced-by-count":21,"title":["A Fully Verified Container Library"],"prefix":"10.1007","author":[{"given":"Nadia","family":"Polikarpova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julian","family":"Tschannen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_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":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-27764-4_5","volume-title":"Mathematics of Program Construction","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, pp. 54\u201384. Springer, Heidelberg (2004)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/11817963_48","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2006","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 532\u2013546. Springer, Heidelberg (2006)"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-12029-9_19","volume-title":"Fundamental Approaches to Software Engineering","author":"D. Beyer","year":"2010","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G., Zufferey, D.: Shape refinement through explicit heap analysis. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol.\u00a06013, pp. 263\u2013277. Springer, Heidelberg (2010)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Blanc, N., Groce, A., Kroening, D.: Verifying C++ with STL containers via predicate abstraction. In: 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2007), Atlanta, Georgia, USA, November 5-9, pp. 521\u2013524 (2007)","DOI":"10.1145\/1321631.1321724"},{"key":"26_CR6","unstructured":"Bruns, D.: Specification of red-black trees: Showcasing dynamic frames, model fields and sequences. In: Ahrendt, W., Bubel, R. (eds.) 10th KeY Symposium, Nijmegen, the Netherlands (2011), Extended Abstract"},{"issue":"6","key":"26_CR7","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C. Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM\u00a058(6), 26 (2011)","journal-title":"J. ACM"},{"key":"26_CR8","unstructured":"Charles, J.: Adding native specifications to JML. In: Workshop on Formal Techniques for Java-like Programs, (FTFJP) (2006)"},{"issue":"9","key":"26_CR9","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W.-N. Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program.\u00a077(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Chlipala, A., Gregory Malecha, J., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: Proceeding of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP 2009, Edinburgh, Scotland, UK, August 31- September 2, pp. 79\u201390. ACM (2009)","DOI":"10.1145\/1596550.1596565"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-319-06410-9_43","volume-title":"FM 2014: Formal Methods","author":"M. Christakis","year":"2014","unstructured":"Christakis, M., Leino, K.R.M., Schulte, W.: Formalizing and verifying a modern build language. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol.\u00a08442, pp. 643\u2013657. Springer, Heidelberg (2014)"},{"key":"26_CR12","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":"26_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, pp. 105\u2013118. ACM (2011)","DOI":"10.1145\/1926385.1926399"},{"key":"26_CR14","unstructured":"Dafny example gallery, \n                        http:\/\/dafny.codeplex.com\/SourceControl\/latest\n                       (last access: November 2014)"},{"key":"26_CR15","first-page":"187","volume-title":"Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011","author":"I. Dillig","year":"2011","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 187\u2013200. ACM, New York (2011)"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-21768-5_9","volume-title":"Tests and Proofs","author":"C. Dross","year":"2011","unstructured":"Dross, C., Filli\u00e2tre, J.-C., Moy, Y.: Correct code containing containers. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol.\u00a06706, pp. 102\u2013118. Springer, Heidelberg (2011)"},{"key":"26_CR17","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A., Stump, A.: The 2nd verified software competition: Experience report. In: COMPARE. CEUR Workshop Proceedings, vol.\u00a0873, CEUR-WS.org (2012), \n                        https:\/\/sites.google.com\/site\/vstte2012\/compet"},{"issue":"2","key":"26_CR18","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/s10817-009-9140-y","volume":"43","author":"R.A. Gamboa","year":"2009","unstructured":"Gamboa, R.A.: A formalization of powerlist algebra in ACL2. J. Autom. Reasoning\u00a043(2), 139\u2013172 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-41071-0_8","volume-title":"Formal Methods: Foundations and Applications","author":"C. Gladisch","year":"2013","unstructured":"Gladisch, C., Tyszberowicz, S.: Specifying a linked data structure in JML for formal verification and runtime checking. In: Iyoda, J., de Moura, L. (eds.) SBMF 2013. LNCS, vol.\u00a08195, pp. 99\u2013114. Springer, Heidelberg (2013)"},{"issue":"3","key":"26_CR20","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1002\/spe.683","volume":"36","author":"D. Gregor","year":"2006","unstructured":"Gregor, D., Schupp STLlint, S.: lifting static checking from languages to libraries. Softw., Pract. Exper.\u00a036(3), 225\u2013254 (2006)","journal-title":"Softw., Pract. Exper."},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, pp. 235\u2013246. ACM (2008)","DOI":"10.1145\/1328438.1328468"},{"key":"26_CR22","first-page":"38","volume-title":"Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011","author":"P. Hawkins","year":"2011","unstructured":"Hawkins, P., Aiken, A., Fisher, K., Rinard, M., Sagiv, M.: Data representation synthesis. In: Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 38\u201349. ACM, New York (2011)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-08867-9_3","volume-title":"Computer Aided Verification","author":"S. Itzhaky","year":"2014","unstructured":"Itzhaky, S., Bj\u00f8rner, N., Reps, T., Sagiv, M., Thakur, A.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 35\u201351. Springer, Heidelberg (2014)"},{"key":"26_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B. Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 41\u201355. Springer, Heidelberg (2011)"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-18275-4_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jacobs","year":"2011","unstructured":"Jacobs, S., Kuncak, V.: Towards complete reasoning about axiomatic specifications. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 278\u2013293. Springer, Heidelberg (2011)"},{"key":"26_CR26","unstructured":"Documentation of java.util.LinkedList, \n                        http:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/LinkedList.html\n                       (last access: December 2014)"},{"key":"26_CR27","unstructured":"Documentation of java.util.Map, \n                        http:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/Map.html\n                       (last access: December 2014)"},{"key":"26_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":"26_CR29","doi-asserted-by":"crossref","unstructured":"Kawaguchi, M., Rondon, P.M., Jhala, R.: Type-based data structure verification. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, pp. 304\u2013315 (2009)","DOI":"10.1145\/1543135.1542510"},{"key":"26_CR30","doi-asserted-by":"crossref","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, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"26_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-15205-4_5","volume-title":"Computer Science Logic","author":"V. Kuncak","year":"2010","unstructured":"Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 34\u201348. Springer, Heidelberg (2010)"},{"key":"26_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-11319-2_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. Kuncak","year":"2010","unstructured":"Kuncak, V., Piskac, R., Suter, P., Wies, T.: Building a calculus of data structures. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 26\u201344. Springer, Heidelberg (2010)"},{"key":"26_CR33","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, pp. 171\u2013182. ACM (2008)","DOI":"10.1145\/1328438.1328461"},{"issue":"6","key":"26_CR34","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s10009-011-0199-5","volume":"13","author":"V. Laviron","year":"2011","unstructured":"Laviron, V., Logozzo, F.: Subpolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities. STTT\u00a013(6), 585\u2013601 (2011)","journal-title":"STTT"},{"key":"26_CR35","series-title":"LNAI","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 (LNAI), vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"26_CR36","unstructured":"Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Workshop (2010), \n                        http:\/\/fm.csl.sri.com\/UV10\/"},{"key":"26_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K.R. M. Leino","year":"2004","unstructured":"M. Leino, K.R., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013515. Springer, Heidelberg (2004)"},{"key":"26_CR38","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, pp. 246\u2013257 (2002)","DOI":"10.1145\/512529.512559"},{"key":"26_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-54108-7_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K.R.M. Leino","year":"2014","unstructured":"Leino, K.R.M., Polikarpova, N.: Verified calculations. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol.\u00a08164, pp. 170\u2013190. Springer, Heidelberg (2014)"},{"issue":"7","key":"26_CR40","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"26_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-39634-2_11","volume-title":"Interactive Theorem Proving","author":"A. Lochbihler","year":"2013","unstructured":"Lochbihler, A.: Light-weight containers for Isabelle: Efficient, extensible, nestable. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 116\u2013132. Springer, Heidelberg (2013)"},{"key":"26_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-27705-4_15","volume-title":"Verified Software: Theories, Tools, Experiments","author":"H. Mehnert","year":"2012","unstructured":"Mehnert, H., Sieczkowski, F., Birkedal, L., Sestoft, P.: Formalized verification of snapshotable trees: Separation and sharing. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 179\u2013195. Springer, Heidelberg (2012)"},{"issue":"3","key":"26_CR43","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. Sci. Comput. Program.\u00a062(3), 253\u2013286 (2006)","journal-title":"Sci. Comput. Program."},{"key":"26_CR44","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, Victoria, BC, Canada, September 20-28, pp. 229\u2013240. ACM (2008)","DOI":"10.1145\/1411204.1411237"},{"key":"26_CR45","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, pp. 247\u2013258 (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"26_CR46","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, pp. 75\u201386. ACM (2008)","DOI":"10.1145\/1328438.1328451"},{"key":"26_CR47","doi-asserted-by":"crossref","unstructured":"Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in C using separation logic. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom, June 09-11, p. 46 (2014)","DOI":"10.1145\/2594291.2594325"},{"key":"26_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/978-3-319-08867-9_47","volume-title":"Computer Aided Verification","author":"R. Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 711\u2013728. Springer, Heidelberg (2014)"},{"key":"26_CR49","unstructured":"Polikarpova, N.: Specified and Verified Reusable Components. PhD thesis, ETH Zurich (2014)"},{"key":"26_CR50","unstructured":"Nadia Polikarpova. EiffelBase2 (repository of verified code) (2015), \n                        http:\/\/dx.doi.org\/10.5281\/zenodo.16520"},{"key":"26_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-15057-9_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"N. Polikarpova","year":"2010","unstructured":"Polikarpova, N., Furia, C.A., Meyer, B.: Specifying reusable components. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 127\u2013141. Springer, Heidelberg (2010)"},{"key":"26_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-319-06410-9_35","volume-title":"FM 2014: Formal Methods","author":"N. Polikarpova","year":"2014","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A., Meyer, B.: Flexible invariants through semantic collaboration. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol.\u00a08442, pp. 514\u2013530. Springer, Heidelberg (2014)"},{"key":"26_CR53","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)"},{"issue":"3","key":"26_CR54","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S. Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"26_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-18275-4_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Suter","year":"2011","unstructured":"Suter, P., Steiger, R., Kuncak, V.: Sets with cardinality constraints in satisfiability modulo theories. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 403\u2013418. Springer, Heidelberg (2011)"},{"key":"26_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-662-46681-0_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Tschannen","year":"2015","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: Auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol.\u00a09035, pp. 566\u2013580. Springer, Heidelberg (2015)"},{"key":"26_CR57","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/2633357.2633366","volume-title":"Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, Haskell 2014","author":"N. Vazou","year":"2014","unstructured":"Vazou, N., Seidel, E.L., Jhala, R.: LiquidHaskell: Experience with refinement types in the real world. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, Haskell 2014, pp. 39\u201351. ACM, New York (2014)"},{"key":"26_CR58","unstructured":"Verifast example gallery, \n                        http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast\/examples\/\n                       (last access: November 2014)"},{"key":"26_CR59","unstructured":"Why3 example gallery, \n                        http:\/\/toccata.lri.fr\/gallery\/why3.en.html\n                       (last access: November 2014)"},{"key":"26_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-22438-6_36","volume-title":"Automated Deduction \u2013 CADE-23","author":"T. Wies","year":"2011","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 476\u2013491. Springer, Heidelberg (2011)"},{"key":"26_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-27705-4_6","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T. Wies","year":"2012","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: Deciding functional lists with sublist sets. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 66\u201381. Springer, Heidelberg (2012)"},{"key":"26_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"},{"key":"26_CR63","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, pp. 349\u2013361 (2008)","DOI":"10.1145\/1379022.1375624"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T01:29:19Z","timestamp":1676942959000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}