Abstract
Interactive proofs of correctness of pointer-manipulating programs tend to be difficult. We propose an approach that integrates shape analysis and interactive theorem proving, namely TVLA and KIV. The approach uses shape analysis to automatically discharge proof obligations for various data structure properties, such as “acyclicity”. We verify the main operations of B + trees by decomposition of the problem into three layers. At the top level is an interactive proof of the main recursive procedures. The actual modifications of the data structure are verified with shape analysis. To this purpose we define a mapping of typed algebraic heaps to TVLA. TVLA itself relies on various constraints and lemmas, that were proven in KIV as a foundation for an overall correct analysis.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bayer, R., McCreight, E.: Organization and maintenance of large ordered indices. Acta Informatica 1, 173–189 (1972)
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. 4590, pp. 221–225. Springer, Heidelberg (2007)
Ernst, G.: KIV and TVLA proofs for B + -Trees (2011), http://www.informatik.uni-augsburg.de/swt/projects/btree.html
Fielding, E.: The specification of abstract mappings and their implementation as B+ trees. Technical report, Oxford University, PRG-18 (1980)
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–350. ACM, New York (2005)
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–251. ACM, New York (2009)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Herter, J.: Towards shape analysis of B-trees. Master’s thesis, Universität Saarbrücken (2008)
Loginov, A., Reps, T., Sagiv, M.: Automated verification of the deutsch-schorr-waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 261–279. Springer, Heidelberg (2006)
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–248. ACM, New York (2010)
Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications, pp. 13–39. Kluwer, Dordrecht (1998)
Reineke, J.: Shape analysis of sets. In: Workshop “Trustworthy Software”. IBFI (2006)
Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural Shape Analysis for Cutpoint-Free Programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 284–302. Springer, Heidelberg (2005)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24, 217–298 (2002)
Sexton, A., Thielecke, H.: Reasoning about B+ trees with operational semantics and separation logic. Electron. Notes Theor. Comput. Sci. 218, 355–369 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ernst, G., Schellhorn, G., Reif, W. (2011). Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving. In: Barthe, G., Pardo, A., Schneider, G. (eds) Software Engineering and Formal Methods. SEFM 2011. Lecture Notes in Computer Science, vol 7041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24690-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-24690-6_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24689-0
Online ISBN: 978-3-642-24690-6
eBook Packages: Computer ScienceComputer Science (R0)