A Logic-Based Framework for Reasoning about Composite Data Structures

DOI10.1007/978-3-642-04081-8_13zbMath1254.68146OpenAlexW1503421880MaRDI QIDQ3184673

Constantin Enea, Mihaela Sighireanu, Ahmed Bouajjani, Cezara Dragoi

Publication date: 22 October 2009

Published in: CONCUR 2009 - Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04081-8_13

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Temporal logic (03B44)

Related Items (8)

Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ A Logic-Based Framework for Reasoning about Composite Data Structures ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Separation logics and modalities: a survey ⋮ Verification of multi-linked heaps ⋮ Quantitative separation logic and programs with lists ⋮ An Efficient Decision Procedure for Imperative Tree Data Structures ⋮ A shape graph logic and a shape system

Cites Work

• A survey and annotated bibliography of multiobjective combinatorial optimization
• A logic of reachable patterns in linked data-structures
• A Logic-Based Framework for Reasoning about Composite Data Structures
• Back to the future
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Shape Analysis for Composite Data Structures
• Rewriting Systems with Data
• Shape Analysis of Single-Parent Heaps
• What Else Is Decidable about Integer Arrays?
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programs with Lists Are Counter Automata
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: A Logic-Based Framework for Reasoning about Composite Data Structures