Verification of B+ trees by integration of shape analysis and interactive theorem proving

Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif

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 three-valued logic analyzer (TVLA) and KIV. The approach uses shape analysis to automatically discharge proof obligations for various data structure properties, such as “acyclicity”. To this purpose, we define a mapping between typed algebraic heaps and TVLA. We verify the main operations of B+ trees by decomposing the problem into three layers: The top-level is an interactive proof of the main recursive procedures. The actual modifications of the data structure are verified with shape analysis. TVLA itself relies on problem-specific constraints and lemmas, that were proven in KIV as a foundation for an overall correct analysis.
published 2013 Software & Systems Modeling

Publisher: Springer

DOI: Springer Link