Recursive proofs for inductive tree data-structures

DOI10.1145/2103656.2103673zbMath1321.68226OpenAlexW4245933182MaRDI QIDQ2942864

P. Madhusudan, Xiaokang Qiu, Andrei Ştefănescu

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)

Related Items (5)

Local Reasoning for Global Graph Properties ⋮ A First-Order Logic with Frames ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Reasoning about algebraic data types with abstractions ⋮ A shape graph logic and a shape system

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