{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T23:25:46Z","timestamp":1664753146468},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,3,29]],"date-time":"2013-03-29T00:00:00Z","timestamp":1364515200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10270-013-0320-1","type":"journal-article","created":{"date-parts":[[2013,3,28]],"date-time":"2013-03-28T14:34:45Z","timestamp":1364481285000},"page":"27-44","source":"Crossref","is-referenced-by-count":2,"title":["Verification of B $$^+$$ trees by integration of shape analysis and interactive theorem proving"],"prefix":"10.1007","volume":"14","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","published-online":{"date-parts":[[2013,3,29]]},"reference":[{"key":"320_CR1","doi-asserted-by":"crossref","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 Inform. 1, 173\u2013189 (1972)","journal-title":"Acta Inform."},{"key":"320_CR2","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Proceedings of the 1st International Conference on Interactive Theorem Proving, ITP, pp. 131\u2013146. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"320_CR3","doi-asserted-by":"crossref","unstructured":"Bogudlov, I., Lev-Ami, T., Reps, T., Sagiv,M.: Revamping TVLA: making parametric shape analysis competitive. In: Proceedings of the 19th Interenational Conference on Computer Aided Verification, CAV, pp. 221\u2013225. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_25"},{"key":"320_CR4","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: Proceedings of the 35th International Symposium on Principles of Programming Languages, POPL, pp. 247\u2013260. ACM (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"320_CR5","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"320_CR6","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: Proceedings of the 23rd Interantional Conference on Object-Oriented Programming Systems Languages and Applications, OOPSLA, pp. 213\u2013226. ACM (2008)","DOI":"10.1145\/1449764.1449782"},{"key":"320_CR7","unstructured":"Dunets, A., Schellhorn, G., Reif, W.: Automated flaw detection in algebraic specifications. J. Autom. Reason 45(4), 354\u2013395 (2010)"},{"key":"320_CR8","unstructured":"Ernst, G.: KIV and TVLA proofs for B $$^{+}$$ trees. http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/btree.html (2011)"},{"key":"320_CR9","doi-asserted-by":"crossref","unstructured":"Ernst, G., Schellhorn, G., Reif, W.: Verification of B $$^{+}$$ trees: an experiment combining shape analysis and interactive theorem proving. In: Proceedings of the 9th International Conference on Software Engineering and Formal Methods, SEFM, pp. 188\u2013203. Springer (2011)","DOI":"10.1007\/978-3-642-24690-6_14"},{"key":"320_CR10","unstructured":"Fielding, E.: The specification of abstract mappings and their implementation as B $$^{+}$$ trees. Technical report, Oxford University, PRG-18 (1980)"},{"key":"320_CR11","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"JH Gallier","year":"1985","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers, Inc., New York (1985)"},{"key":"320_CR12","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: Proceedings of the 32th International Symposium on Principles of Programming Languages, POPL, pp. 338\u2013350. ACM (2005)","DOI":"10.1145\/1047659.1040333"},{"key":"320_CR13","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: Proceedings of the 36th International Symposium on Principles of Programming Languages, POPL, pp. 239\u2013251. ACM (2009)","DOI":"10.1145\/1480881.1480912"},{"key":"320_CR14","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge, Massachusetts (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"320_CR15","unstructured":"Herter, J.: Towards shape analysis of B-trees. Universit\u00e4t Saarbr\u00fccken, Master\u2019s thesis (2008)"},{"key":"320_CR16","doi-asserted-by":"crossref","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Prof. of Static Analysis Symposium, SAS, pp. 261\u2013279. Springer (2006)","DOI":"10.1007\/11823230_17"},{"key":"320_CR17","doi-asserted-by":"crossref","unstructured":"Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: Proceedings of the 37th International Symposium on Principles of Programming Languages, POPL, pp. 237\u2013248. ACM (2010)","DOI":"10.1145\/1706299.1706329"},{"key":"320_CR18","doi-asserted-by":"crossref","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, vol. II, chapter 1, pp. 13\u201339. Kluwer, Dordrecht (1998)","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"320_CR19","unstructured":"Reineke, J.: Shape analysis of sets. In: Workshop \u201cTrustworthy Software\u201d. IBFI (2006)"},{"key":"320_CR20","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural shape analysis for cutpoint-free programs. In: Proceedings of Static Analysis Symposium, SAS, pp. 284\u2013302. Springer (2005)","DOI":"10.1007\/11547662_20"},{"key":"320_CR21","doi-asserted-by":"crossref","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. 24, 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"320_CR22","unstructured":"Sexton, A., Thielecke, H.: Reasoning about B $$^{+}$$ trees with operational semantics and separation logic. Electron. Notes Theor. Comput. Sci. 218, 355\u2013369 (2008)"},{"key":"320_CR23","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pp. 530\u2013545. Springer (2004)","DOI":"10.1007\/978-3-540-24730-2_39"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0320-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-013-0320-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0320-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,11]],"date-time":"2019-07-11T13:39:43Z","timestamp":1562852383000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-013-0320-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,29]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["320"],"URL":"https:\/\/doi.org\/10.1007\/s10270-013-0320-1","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,29]]}}}