{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:45:25Z","timestamp":1725896725527},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642246890"},{"type":"electronic","value":"9783642246906"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24690-6_14","type":"book-chapter","created":{"date-parts":[[2011,10,25]],"date-time":"2011-10-25T01:35:37Z","timestamp":1319506537000},"page":"188-203","source":"Crossref","is-referenced-by-count":4,"title":["Verification of B\u2009+\u2009 Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving"],"prefix":"10.1007","author":[{"given":"Gidon","family":"Ernst","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF00288683","volume":"1","author":"R. Bayer","year":"1972","unstructured":"Bayer, R., McCreight, E.: Organization and maintenance of large ordered indices. Acta Informatica\u00a01, 173\u2013189 (1972)","journal-title":"Acta Informatica"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-73368-3_25","volume-title":"Computer Aided Verification","author":"I. Bogudlov","year":"2007","unstructured":"Bogudlov, I., Lev-Ami, T., Reps, T., Sagiv, M.: Revamping TVLA: Making Parametric Shape Analysis Competitive. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 221\u2013225. Springer, Heidelberg (2007)"},{"key":"14_CR3","unstructured":"Ernst, G.: KIV and TVLA proofs for B\u2009+\u2009-Trees (2011), \n                    \n                      http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/btree.html"},{"key":"14_CR4","unstructured":"Fielding, E.: The specification of abstract mappings and their implementation as B+ trees. Technical report, Oxford University, PRG-18 (1980)"},{"key":"14_CR5","first-page":"338","volume-title":"Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, POPL","author":"D. Gopan","year":"2005","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, POPL, pp. 338\u2013350. ACM, New York (2005)"},{"key":"14_CR6","first-page":"239","volume-title":"Proc. of the 36th ACM SIGPLAN-SIGACT Symp Principles of programming languages, POPL","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: Proc. of the 36th ACM SIGPLAN-SIGACT Symp Principles of programming languages, POPL, pp. 239\u2013251. ACM, New York (2009)"},{"key":"14_CR7","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"14_CR8","unstructured":"Herter, J.: Towards shape analysis of B-trees. Master\u2019s thesis, Universit\u00e4t Saarbr\u00fccken (2008)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/11823230_17","volume-title":"Static Analysis","author":"A. Loginov","year":"2006","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Automated verification of the deutsch-schorr-waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 261\u2013279. Springer, Heidelberg (2006)"},{"key":"14_CR10","first-page":"237","volume-title":"Proc. of the 37th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, POPL","author":"G. Malecha","year":"2010","unstructured":"Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: Proc. of the 37th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, POPL, pp. 237\u2013248. ACM, New York (2010)"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-94-017-0435-9_1","volume-title":"Automated Deduction\u2014A Basis for Applications","author":"W. Reif","year":"1998","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, pp. 13\u201339. Kluwer, Dordrecht (1998)"},{"key":"14_CR12","unstructured":"Reineke, J.: Shape analysis of sets. In: Workshop \u201cTrustworthy Software\u201d. IBFI (2006)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/11547662_20","volume-title":"Static Analysis","author":"N. Rinetzky","year":"2005","unstructured":"Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural Shape Analysis for Cutpoint-Free Programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 284\u2013302. Springer, Heidelberg (2005)"},{"key":"14_CR14","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024, 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1016\/j.entcs.2008.10.021","volume":"218","author":"A. Sexton","year":"2008","unstructured":"Sexton, A., Thielecke, H.: Reasoning about B+ trees with operational semantics and separation logic. Electron. Notes Theor. Comput. Sci.\u00a0218, 355\u2013369 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24690-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,14]],"date-time":"2019-04-14T02:38:25Z","timestamp":1555209505000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24690-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642246890","9783642246906"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24690-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}