Recursive proofs for inductive tree data-structures

P. Madhusudan, Xiaokang Qiu, Andrei Stefanescu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We develop logical mechanisms and procedures to facilitate the verification of full functional properties of inductive tree datastructures 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 leads to finding simple recursive proofs using formula 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, AVL trees, binomial heaps, and B-trees.

Original languageEnglish (US)
Title of host publicationPOPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Number of pages13
StatePublished - 2012
Event39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12 - Philadelphia, PA, United States
Duration: Jan 25 2012Jan 27 2012

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566


Conference39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12
Country/TerritoryUnited States
CityPhiladelphia, PA


  • Heap analysis
  • Recursive program
  • SMT solver
  • Tree

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Recursive proofs for inductive tree data-structures'. Together they form a unique fingerprint.

Cite this