{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T15:50:45Z","timestamp":1748361045284,"version":"3.40.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319121536"},{"type":"electronic","value":"9783319121543"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12154-3_11","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T08:20:23Z","timestamp":1413188423000},"page":"167-180","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Automatically Verified Implementation of Data Structures Based on AVL Trees"],"prefix":"10.1007","author":[{"given":"Martin","family":"Clochard","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,10,14]]},"reference":[{"issue":"2","key":"11_CR1","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"GT Leavens","year":"2007","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput. 19(2), 159\u2013189 (2007)","journal-title":"Formal Aspects Comput."},{"key":"11_CR2","unstructured":"Leino, K.R.M., Moskal, M.: VACID-0: Verification of ample correctness of invariants of data-structures. In: Proceedings of Tools and Experiments Workshop at VSTTE (2010)"},{"issue":"5","key":"11_CR3","first-page":"1259","volume":"3","author":"GM Adel\u2019son-Vel\u2019ski\u01d0","year":"1962","unstructured":"Adel\u2019son-Vel\u2019ski\u01d0, G.M., Landis, E.M.: An algorithm for the organization of information. Sov. Mathematics-Doklady 3(5), 1259\u20131263 (1962)","journal-title":"Sov. Mathematics-Doklady"},{"issue":"2","key":"11_CR4","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1017\/S0956796805005769","volume":"16","author":"R Hinze","year":"2006","unstructured":"Hinze, R., Paterson, R.: Finger trees: a simple general-purpose data structure. J. Funct. Program. 16(2), 197\u2013217 (2006)","journal-title":"J. Funct. Program."},{"key":"11_CR5","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, pp. 53\u201364, August 2011"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-540-24725-8_26","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., Letouzey, P.: Functors for proofs and programs. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 370\u2013384. Springer, Heidelberg (2004)"},{"key":"11_CR7","unstructured":"Nipkow, T., Pusch, C.: AVL Trees. Archive of Formal Proofs. Formal proof development, March 2004. http:\/\/afp.sf.net\/entries\/AVL-Trees.shtml"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Ralston, R.: ACL2-certified AVL Trees. In: Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 \u201909, pp. 71\u201374. ACM (2009)","DOI":"10.1145\/1637837.1637848"},{"key":"11_CR9","unstructured":"Appel, A.: Efficient Verified Red-Black Trees (2011). http:\/\/www.cs.princeton.edu\/appel\/papers\/redblack.pdf"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Program verification through characteristic formulae. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP \u201910, pp. 321\u2013332. ACM (2010)","DOI":"10.1145\/1863543.1863590"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-14052-5_24","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2010","unstructured":"Lammich, P., Lochbihler, A.: The Isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 339\u2013354. Springer, Heidelberg (2010)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Sozeau, M.: Program-ing finger trees in Coq. In: Hinze, R., Ramsey, N. (eds.) 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, pp. 13\u201324. ACM Press (2007)","DOI":"10.1145\/1291220.1291156"},{"key":"11_CR13","unstructured":"Nordhoff, B., K\u00f6rner, S., Lammich, P.: Finger Trees. Archive of Formal Proofs, October 2010. http:\/\/afp.sf.net\/entries\/Finger-Trees.shtml. Formal proof development"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12154-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,19]],"date-time":"2023-01-19T23:10:58Z","timestamp":1674169858000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12154-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319121536","9783319121543"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12154-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"14 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}