{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:28:13Z","timestamp":1768004893051,"version":"3.49.0"},"reference-count":89,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2018,9,1]],"date-time":"2018-09-01T00:00:00Z","timestamp":1535760000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The comprehensive functionality and nontrivial design of realistic general-purpose container libraries pose challenges to formal verification that go beyond those of individual benchmark problems mainly targeted by the state of the art. We present our experience verifying the full functional correctness of EiffelBase2: a container library offering all the features customary in modern language frameworks, such as external iterators, and hash tables with generic mutable keys and load balancing. Verification uses the automated deductive verifier AutoProof, which we extended as part of the present work. Our results indicate that verification of a realistic container library (135 public methods, 8400 LOC) is possible with moderate annotation overhead (1.4 lines of specification per LOC) and good performance (0.2 s per method on average).<\/jats:p>","DOI":"10.1007\/s00165-017-0435-1","type":"journal-article","created":{"date-parts":[[2017,9,20]],"date-time":"2017-09-20T05:43:23Z","timestamp":1505886203000},"page":"495-523","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["A fully verified container library"],"prefix":"10.1145","volume":"30","author":[{"given":"Nadia","family":"Polikarpova","sequence":"first","affiliation":[{"name":"MIT CSAIL, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julian","family":"Tschannen","sequence":"additional","affiliation":[{"name":"Google, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, G\u00f6teborg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Ameri M Furia CA (June 2016) Why just Boogie? Translating between intermediate verification languages. In: Proceedings of the 12th international conference on integrated formal methods (iFM) volume 9681 of lecture notes in computer science. Springer pp 1\u201317"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Barnett M Chang B-YE DeLine R Jacobs B Leino KRM (2005) Boogie: a modular reusable verifier for object-oriented programs. In: FMCO pp 364\u2013387","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Blanc N.; Groce A.; Kroening D.: Verifying C++ with STL containers via predicate abstraction. 22nd IEEE\/ACM international conference on automated software engineering (ASE 2007) Nov 5\u20139 2007 pp. 521\u2013524. Atlanta Georgia USA (2007)","DOI":"10.1145\/1321631.1321724"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Beyer D Henzinger TA Th\u00e9oduloz G (2006) Lazy shape analysis. In: 18th international conference on computer aided verification CAV 2006 Seattle WA USA Aug 17\u201320 2006 Proceedings volume 4144 of lecture notes in computer science. Springer pp 532\u2013546","DOI":"10.1007\/11817963_48"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Beyer D Henzinger TA Th\u00e9oduloz G Zufferey D (2010) Shape refinement through explicit heap analysis. In: Fundamental approaches to software engineering volume 6013 of lecture notes in computer science. Springer pp 263\u2013277","DOI":"10.1007\/978-3-642-12029-9_19"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Barnett M Naumann DA (2004) Friends need a bit more: maintaining invariants over shared state. In: 7th international conference on mathematics of program construction MPC 2004 Stirling Scotland UK July 12\u201314 2004 Proceedings pp 54\u201384","DOI":"10.1007\/978-3-540-27764-4_5"},{"key":"e_1_2_1_2_8_2","unstructured":"Bruns D (2011) Specification of red-black trees: showcasing dynamic frames model fields and sequences. In: 10th\u00a0keY symposium Nijmegen The Netherlands Extended Abstract."},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Cousot P Cousot R Logozzo F (2011) 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 Jan 26\u201328 2011. ACM pp 105\u2013118","DOI":"10.1145\/1925844.1926399"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Cohen E Dahlweid M Hillebrand MA Leinenbach D Moskal M Santen T Schulte W Tobies S (2009) VCC: a practical system for verifying concurrent C. In: 22nd international conference on theorem proving in higher order logics TPHOLs 2009 Munich Germany Aug 17\u201320 2009. Proceedings volume 5674 of lecture notes in computer science. Springer pp 23\u201342","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_1_2_13_2","unstructured":"Charles J (2006) Adding native specifications to JML. In: Workshop on formal techniques for java-like programs (FTfJP)"},{"key":"e_1_2_1_2_14_2","volume-title":"Introduction to algorithms","author":"Cormen TH","year":"2009","edition":"3"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Christakis M Leino KRM Schulte W (2014) Formalizing and verifying a modern build language. In: FM 2014: formal methods\u201419th international symposium Singapore May 12\u201316 2014. Proceedings volume 8442 of lecture notes in computer science. Springer pp 643\u2013657","DOI":"10.1007\/978-3-319-06410-9_43"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.649"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Chlipala A Malecha JG Morrisett G Shinnar A Wisnesky R (2009) 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 Aug 31\u2013Sept 2 2009. ACM pp 79\u201390","DOI":"10.1145\/1631687.1596565"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Cok DR (2006) Specifying Java iterators with JML and ESC\/Java2. In: Proceedings of the 2006 conference on specification and verification of component-based systems SAVCBS \u201906. ACM pp 71\u201374","DOI":"10.1145\/1181195.1181210"},{"key":"e_1_2_1_2_19_2","unstructured":"Dafny example gallery. http:\/\/dafny.codeplex.com\/SourceControl\/latest. Last access Feb 2016."},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/356876.356881"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Dillig I Dillig T Aiken A (2011) Precise reasoning for programs using containers. In: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL\u201911 New York NY USA. ACM pp 187\u2013200","DOI":"10.1145\/1926385.1926407"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Dross C Filli\u00e2tre J-C Moy Y (2011) Correct code containing containers. In: 5th international conference on tests and proofs (TAP\u201911) volume 6706 of lecture notes in computer science Zurich. Springer pp 102\u2013118","DOI":"10.1007\/978-3-642-21768-5_9"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Moura dL Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In:14th international conference tools and algorithms for the construction and analysis of systems TACAS 2008 held as part of the Joint European conferences on theory and practice of software ETAPS 2008 Budapest Hungary March 29\u2013April 6 2008. Proceedings volume 4963 of lecture notes in computer science. Springer pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J Gondelman L Paskevich A (2014) The spirit of ghost code. In: Proceedings of the 26th international conference on computer aided verification (CAV) volume 8559 of lecture notes in computer science. Springer pp 1\u201316","DOI":"10.1007\/978-3-319-08867-9_1"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Furia CA Nordio M Polikarpova N Tschannen J (2016) AutoProof: auto-active functional verification of object-oriented programs. Int J Softw Tools Technol Transf Online since April 2016. http:\/\/link.springer.com\/article\/10.1007\/s10009-016-0419-0.","DOI":"10.1007\/s10009-016-0419-0"},{"key":"e_1_2_1_2_26_2","unstructured":"Filli\u00e2tre J-C Paskevich A Stump A (2012) The 2nd verified software competition: experience report. In: COMPARE volume 873 of CEUR workshop proceedings. CEUR-WS.org https:\/\/sites.google.com\/site\/vstte2012\/compet."},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Furia CA Poskitt CM Tschannen J (June 2015) The AutoProof verifier: Usability by non-experts and on standard code. In: Proceedings of the 2nd workshop on formal integrated development environment (F-IDE) volume 187 of electronic proceedings in theoretical computer science. EPTCS Workshop co-located with FM 2015 pp 42\u201355","DOI":"10.4204\/EPTCS.187.4"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9140-y"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Gulwani S McCloskey B Tiwari A (2008) 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 Jan 7\u201312 2008. ACM pp 235\u2013246","DOI":"10.1145\/1328897.1328468"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.683"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Gladisch C Tyszberowicz S (2013) Specifying a linked data structure in JML for formal verification and runtime checking. In: Brazilian symposium on formal methods (SBMF) volume 8195 of lecture notes in computer science. Springer pp 99\u2013114","DOI":"10.1007\/978-3-642-41071-0_8"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Hawkins P Aiken A Fisher K Rinard M Sagiv M (2011) Data representation synthesis. In: Proceedings of the 32Nd ACM SIGPLAN conference on programming language design and implementation PLDI\u201911 New York NY USA. ACM pp 38\u201349","DOI":"10.1145\/1993498.1993504"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187678"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Itzhaky S Bj\u00f8rner N Reps TW Sagiv M Thakur AV (2014) Property-directed shape analysis. In: 26th international conference computer aided verification CAV 2014 Held as part of the Vienna Summer of Logic VSL 2014 Vienna Austria July 18\u201322 2014. Proceedings volume 8559 of lecture notes in computer science. Springer pp 35\u201351","DOI":"10.1007\/978-3-319-08867-9_3"},{"key":"e_1_2_1_2_35_2","unstructured":"Documentation of java.util.LinkedList. http:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/LinkedList.html. Last access Feb 2016."},{"key":"e_1_2_1_2_36_2","unstructured":"Documentation of java.util.Map. http:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/Map.html. Last access Feb 2016."},{"issue":"2","key":"e_1_2_1_2_37_2","first-page":"1","article-title":"Modular verification of linked lists with views via separation logic","volume":"10","author":"Jensen JB","year":"2011","journal-title":"J Object Technol"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Jacobs S Kuncak V (2011) Towards complete reasoning about axiomatic specifications. In: 12th international conference on verification model checking and abstract interpretation VMCAI 2011 Austin TX USA Jan 23\u201325 2011. Proceedings volume 6538 of lecture notes in computer science. Springer pp 278\u2013293","DOI":"10.1007\/978-3-642-18275-4_20"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Jacobs B Piessens F Schulte W (2006) VC generation for functional behavior and non-interference of iterators. In: Proceedings of the 2006 conference on specification and verification of component-based systems SAVCBS\u201906. ACM pp 71\u201374","DOI":"10.1145\/1181195.1181209"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Jacobs B Smans J Philippaerts P Vogels F Penninckx W Piessens F (2011) VeriFast: A powerful sound predictable fast verifier for C and Java. NASA Form Methods pp 41\u201355","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Kassios IT (2006) Dynamic frames: support for framing dependencies and sharing without restrictions. In: FM 2006: formal methods 14th international symposium on formal methods Hamilton Canada Aug 21\u201327 2006. Proceedings pp 268\u2013283","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_1_2_42_2","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 (2009) seL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM symposium on operating systems principles 2009 SOSP 2009 Big Sky Montana USA Oct 11\u201314 2009. ACM pp 207\u2013220","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Kuncak V Piskac R Suter P (2010) Ordered sets in the calculus of data structures. In: Computer science logic 24th international workshop CSL 2010 19th annual conference of the EACSL Brno Czech Republic Aug 23\u201327 2010. Proceedings volume 6247 of lecture notes in computer science. Springer pp 34\u201348","DOI":"10.1007\/978-3-642-15205-4_5"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Kuncak V Piskac R Suter P Wies T (2010) Building a calculus of data structures. In: 11th international conference on verification model checking and abstract interpretation VMCAI 2010 Madrid Spain Jan 17\u201319 2010. Proceedings volume 5944 of lecture notes in computer science. Springer pp 26\u201344","DOI":"10.1007\/978-3-642-11319-2_6"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Kawaguchi M Rondon PM Jhala R (2009) 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\u201321 2009 pp 304\u2013315","DOI":"10.1145\/1543135.1542510"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_2_47_2","unstructured":"Leino KRM (1995) Toward reliable modular programs. Ph.D. thesis Caltech"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Leino KRM (2010) Dafny: An automatic program verifier for functional correctness. In: 16th international conference on logic for programming artificial intelligence and reasoning LPAR-16 Dakar Senegal April 25\u2013May 1 2010 revised selected papers volume 6355 of lecture notes in computer science. Springer pp 348\u2013370","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0199-5"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Leino KRM M\u00fcller P (2004) Object invariants in dynamic contexts. In: ECOOP 2004\u2014object-oriented programming 18th European conference Oslo Norway June 14\u201318 2004 Proceedings volume 3086 of lecture notes in computer science. Springer pp 491\u2013516","DOI":"10.1007\/978-3-540-24851-4_22"},{"key":"e_1_2_1_2_52_2","unstructured":"Leino KRM M\u00fcller P (2006) A verification methodology for model fields. In: 15th European symposium on programming\u2014programming languages and systems ESOP 2006 Held as part of the joint European conferences on theory and practice of software ETAPS 2006 Vienna Austria March 27\u201328 2006 Proceedings volume 3924 of lecture notes in computer science. Springer pp 115\u2013130"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Leino KRM M\u00fcller P (Sept 2009) Using the Spec# language methodology and tools to write bug-free programs. http:\/\/www.codeplex.com\/Download?ProjectName=specsharp&DownloadId=84056","DOI":"10.1007\/978-3-642-13010-6_4"},{"key":"e_1_2_1_2_54_2","unstructured":"Leino KRM Moskal M (2010) Usable auto-active verification. In: Usable verification workshop. http:\/\/fm.csl.sri.com\/UV10\/"},{"key":"e_1_2_1_2_55_2","unstructured":"Leino KRM Moskal M (2010) VACID-0: Verification of ample correctness of invariants of data-structures 0 edn. VSTTE Workshops http:\/\/goo.gl\/0VnvyO"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Lochbihler A (2013) Light-weight containers for Isabelle: efficient extensible nestable. In: 4th international conference on interactive theorem proving ITP 2013 Rennes France July 22\u201326 2013. Proceedings volume 7998 of lecture notes in computer science. Springer pp 116\u2013132","DOI":"10.1007\/978-3-642-39634-2_11"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Leino KRM Polikarpova N (2013) Verified calculations. In: 5th international conference on verified software: theories tools experiments VSTTE 2013 Menlo Park CA USA May 17\u201319 2013 revised selected papers pp 170\u2013190","DOI":"10.1007\/978-3-642-54108-7_9"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Leino KRM Poetzsch-Heffter A Zhou Y (2002) 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\u201319 2002 pp 246\u2013257","DOI":"10.1145\/543552.512559"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Lahiri SK Qadeer S (2008) 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 Jan 7\u201312 2008. ACM pp 171\u2013182","DOI":"10.1145\/1328897.1328461"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Leino KRM Wallenburg A (2008) Class-local object invariants. In: Proceeding of the 1st annual India software engineering conference ISEC 2008 Hyderabad India Feb 19\u201322 2008 pp 57\u201366","DOI":"10.1145\/1342211.1342225"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"crossref","unstructured":"Mehnert H Sieczkowski F Birkedal L Sestoft P (2012) Formalized verification of snapshotable trees: separation and sharing. In: 4th International conference on verified software: theories tools experiments VSTTE 2012 Philadelphia PA USA Jan 28\u201329 2012. Proceedings pp 179\u2013195","DOI":"10.1007\/978-3-642-27705-4_15"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"crossref","unstructured":"M\u00fcller P (2002) Modular specification and verification of object-oriented programs volume 2262 of lecture notes in computer science. Springer","DOI":"10.1007\/3-540-45651-1"},{"key":"e_1_2_1_2_65_2","unstructured":"Documentation of Systems.Collections.Generic.Dictionary. https:\/\/msdn.microsoft.com\/en-us\/library\/xfhwa508.aspx. Last access Feb 2016"},{"key":"e_1_2_1_2_66_2","unstructured":"Documentation of Systems.Collections.Generic.List.Enumerator. https:\/\/msdn.microsoft.com\/en-us\/library\/x854yt9s.aspx. Last access Feb 2016"},{"key":"e_1_2_1_2_67_2","doi-asserted-by":"crossref","unstructured":"Nanevski A Morrisett G Shinnar A Govereau P Birkedal L (2008) Ynot: dependent types for imperative programs. In: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming ICFP 2008 Victoria BC Canada Sept 20\u201328 2008. ACM pp 229\u2013240","DOI":"10.1145\/1411203.1411237"},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring C (2011) Introduction to the Coq proof-assistant for practical software verification. In: Tools for practical software verification LASER international summer school 2011 Elba Island Italy revised tutorial lectures volume 7682 of lecture notes in computer science. Springer pp 45\u201395","DOI":"10.1007\/978-3-642-35746-6_3"},{"key":"e_1_2_1_2_69_2","doi-asserted-by":"crossref","unstructured":"Parkinson MJ and Bierman GM (2008) 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 Jan 7\u201312 2008. ACM pp 75\u201386","DOI":"10.1145\/1328897.1328451"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"crossref","unstructured":"Polikarpova N Furia CA Meyer B (2010) Specifying reusable components. In: Proceedings of the 3rd international conference on verified software: theories tools and experiments (VSTTE\u201910) volume 6217 of lecture notes in computer science. Springer pp 127\u2013141","DOI":"10.1007\/978-3-642-15057-9_9"},{"key":"e_1_2_1_2_71_2","unstructured":"Polikarpova N (2014) Specified and verified reusable components. Ph.D. thesis ETH Zurich"},{"key":"e_1_2_1_2_72_2","unstructured":"Polikarpova N (2015) EiffelBase2 (repository of verified code). http:\/\/dx.doi.org\/10.5281\/zenodo.16520"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"crossref","unstructured":"Pek E Qiu X Madhusudan P (2014) Natural proofs for data structure manipulation in C using separation logic. In: ACM SIGPLAN conference on programming language design and implementation PLDI \u201914 Edinburgh UK June 09\u201311 2014 pp 46","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_2_1_2_74_2","doi-asserted-by":"crossref","unstructured":"Polikarpova N Tschannen J Furia CA (June 2015) A fully verified container library. In: Proceedings of the 20th international symposium on formal methods (FM) volume 9109 of lecture notes in computer science. Springer pp 414\u2013434","DOI":"10.1007\/978-3-319-19249-9_26"},{"key":"e_1_2_1_2_75_2","doi-asserted-by":"crossref","unstructured":"Polikarpova N Tschannen J Furia CA Meyer B (2014) Flexible invariants through semantic collaboration. In: FM 2014: formal methods\u201419th international symposium Singapore May 12\u201316 2014. Proceedings pp 514\u2013530","DOI":"10.1007\/978-3-319-06410-9_35"},{"key":"e_1_2_1_2_76_2","doi-asserted-by":"crossref","unstructured":"Piskac R Wies T Zufferey D (2014) Automating separation logic with trees and data. In: 26th international conference on computer aided verification CAV 2014 Held as part of the Vienna Summer of Logic VSL 2014 Vienna Austria July 18\u201322 2014. Proceedings volume 8559 of lecture notes in computer science. Springer pp 711\u2013728","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_2_1_2_77_2","doi-asserted-by":"crossref","unstructured":"R\u00e9gis-Gianas Y Pottier F (2008) A Hoare logic for call-by-value functional programs. In: 9th international conference on mathematics of program construction MPC 2008 Marseille France July 15\u201318 2008. Proceedings volume 5133 of lecture notes in computer science. Springer pp 305\u2013335","DOI":"10.1007\/978-3-540-70594-9_17"},{"key":"e_1_2_1_2_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_2_79_2","doi-asserted-by":"crossref","unstructured":"Suter P Steiger R Kuncak V (2011) Sets with cardinality constraints in satisfiability modulo theories. In: 12th international conference on verification model checking and abstract interpretation VMCAI 2011 Austin TX USA Jan 23\u201325 2011. Proceedings volume 6538 of lecture notes in computer science. Springer pp 403\u2013418","DOI":"10.1007\/978-3-642-18275-4_28"},{"key":"e_1_2_1_2_80_2","doi-asserted-by":"crossref","unstructured":"Tschannen J Furia CA Nordio M Polikarpova N (2015) AutoProof: Auto-active functional verification of object-oriented programs. In: Proceedings of the 21st international conference on tools and algorithms for the construction and analysis of systems (TACAS) volume 9035 of lecture notes in computer science. Springer pp 566\u2013580","DOI":"10.1007\/978-3-662-46681-0_53"},{"key":"e_1_2_1_2_81_2","unstructured":"Verifast example gallery. http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast\/examples\/. Last access Feb 2016"},{"key":"e_1_2_1_2_82_2","doi-asserted-by":"crossref","unstructured":"Vazou N Seidel EL Jhala R (2014) LiquidHaskell: experience with refinement types in the real world. In: Proceedings of the 2014 ACM SIGPLAN symposium on haskell Haskell\u201914 New York NY USA. ACM pp 39\u201351","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_2_1_2_83_2","doi-asserted-by":"crossref","unstructured":"Weide B Edwards S Heym WD Long T and Ogden W (April 1996) Characterizing observability and controllability of software components. In: Proceedings fourth international conference on software reuse 1996 pp 62\u201371","DOI":"10.1109\/ICSR.1996.496114"},{"key":"e_1_2_1_2_84_2","unstructured":"Why3 example gallery. http:\/\/toccata.lri.fr\/gallery\/why3.en.html. Last access Feb 2016."},{"key":"e_1_2_1_2_85_2","doi-asserted-by":"crossref","unstructured":"Wies T Mu\u00f1iz M Kuncak V (2011) An efficient decision procedure for imperative tree data structures. In: Automated deduction\u2014CADE-23\u201423rd international conference on automated deduction Wroclaw Poland July 31 Aug 5 2011. Proceedings volume 6803 of lecture notes in computer science. Springer pp 476\u2013491","DOI":"10.1007\/978-3-642-22438-6_36"},{"key":"e_1_2_1_2_86_2","doi-asserted-by":"crossref","unstructured":"Wies T Mu\u00f1iz M Kuncak V (2012) Deciding functional lists with sublist sets. In: 4th international conference on verified software: theories tools experiments VSTTE 2012 Philadelphia PA USA Jan 28\u201329 2012. Proceedings volume 7152 of lecture notes in computer science. Springer pp 66\u201381","DOI":"10.1007\/978-3-642-27705-4_6"},{"key":"e_1_2_1_2_87_2","doi-asserted-by":"crossref","unstructured":"Xi\u00a0H Pfenning F (1999) Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL\u201999 New York NY USA. ACM pp 214\u2013227","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_1_2_88_2","doi-asserted-by":"crossref","unstructured":"Yang H Lee O Berdine J Calcagno C Cook B Distefano D O\u2019Hearn PW (2008) Scalable shape analysis for systems code. In: 20th international conference Computer Aided Verification CAV 2008 Princeton NJ USA July 7\u201314 2008. Proceedings volume 5123 of lecture notes in computer science. Springer pp 385\u2013398","DOI":"10.1007\/978-3-540-70545-1_36"},{"key":"e_1_2_1_2_89_2","doi-asserted-by":"crossref","unstructured":"Zee K Kuncak V Rinard MC (2008) 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\u201313 2008 pp 349\u2013361","DOI":"10.1145\/1379022.1375624"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0435-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0435-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0435-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0435-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T20:33:25Z","timestamp":1750883605000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0435-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9]]},"references-count":89,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,9]]}},"alternative-id":["10.1007\/s00165-017-0435-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0435-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9]]}}}