Recursive proofs for inductive tree data-structures
DOI10.1145/2103656.2103673zbMATH Open1321.68226OpenAlexW4245933182MaRDI QIDQ2942864FDOQ2942864
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
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
Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cited In (13)
- 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
- Inductive theorem proving based on tree grammars
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)
