Name
Title | ||
|---|---|---|
Verification of B$$^+$$ trees by integration of shape analysis and interactive theorem proving |
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 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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/s10270-013-0320-1 | Software and Systems Modeling (SoSyM) |
Keywords | Field | DocType |
Theorem proving, Shape analysis, B$$^+$$ trees, Pointer structures | Data structure,Programming language,Computer science,Correctness,Automated theorem proving,Theoretical computer science,Heap (data structure),Mathematical proof,Recursion,Shape analysis (digital geometry),Proof assistant | Journal |
Volume | Issue | ISSN |
14 | 1 | 1619-1374 |
Citations | PageRank | References |
0 | 0.34 | 9 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gidon Ernst | 1 | 144 | 14.46 |
| Gerhard Schellhorn | 2 | 769 | 56.43 |
| Wolfgang Reif | 3 | 915 | 95.46 |