Recursive proofs for inductive tree data-structures

DOI10.1145/2103656.2103673MaRDI QIDQ2942864zbMATH OpenOpenAlexFDO

Authors Parthasarathy Madhusudan, Xiaokang Qiu, A. Stefanescu

Publication date 11 September 2015

Published in Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2103656.2103673

zbMATH Keywords

treeheap analysisSMT solversrecursive program

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Proving tree algorithms for succinct data structures
• INDUCTIVE ALGORITHMS ON FINITE TREES
• Inducibility of \(d\)-ary trees
• Inducibility and universality for trees
• Inductive theorem proving based on tree grammars
• Proof-based synthesis of sorting algorithms for trees
• Automatically analyzing inductive properties for recursive data structures
• A tree-based approach to data flow proofs
• Further results on the inducibility of \(d\)-ary trees
• Inductive invariants for nested recursion

Cited in

(13)

• Inductive theorem proving based on tree grammars
• An assertional proof of red-black trees using Dafny
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• An efficient decision procedure for imperative tree data structures
• Automatic functional correctness proofs for functional search trees
• Local reasoning for global graph properties
• Simpler proofs with decentralized invariants
• A shape graph logic and a shape system
• Tools and Algorithms for the Construction and Analysis of Systems
• A decidable logic for tree data-structures with measurements
• Reasoning About Data Trees Using CHCs
• Reasoning about algebraic data types with abstractions
• A first-order logic with frames

This page was built for publication: Recursive proofs for inductive tree data-structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2942864)