Recursive proofs for inductive tree data-structures

We develop logical mechanisms and decision procedures to facilitate the verification of full functional properties of inductive tree data-structures using recursion that are sound, incomplete, but terminating. Our contribution rests in a new extension of first-order logic with recursive definitions called Dryad, a syntactical restriction on pre- and post-conditions of recursive imperative programs using Dryad, and a systematic methodology for accurately unfolding the footprint on the heap uncovered by the program that finding simple recursive proofs using abstraction and calls to SMT solvers. We evaluate our methodology empirically and show that several complex tree data-structure algorithms can be checked against full functional specifications automatically, given pre- and post-conditions. This results in the first automatic terminating methodology for proving a wide variety of annotated algorithms on tree data-structures correct, including max-heaps, treaps, red-black trees, A...

• Type: Journal
• Year: 2012
• Where: POPL
• Authors: Parthasarathy Madhusudan, Xiaokang Qiu, Andrei Stefanescu
• Keywords: Binomial Heaps, Logical Mechanisms, POPL 2012, Programming Languages, Tree Data Structures