A Logic-Based Framework for Reasoning about Composite Data Structures

DOI10.1007/978-3-642-04081-8_13MaRDI QIDQ3184673zbMATH OpenOpenAlexFDO

Authors Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea, Mihaela Sighireanu

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

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

Recommendations

• A logic of reachable patterns in linked data-structures
• scientific article; zbMATH DE number 1956491
• Foundations of Software Science and Computation Structures
• Decidable logics combining heap structures and data
• Building a calculus of data structures

Cites work

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

Cited in

(11)

• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• A logic of reachable patterns in linked data-structures
• A Logic-Based Framework for Reasoning about Composite Data Structures
• scientific article; zbMATH DE number 3876614 (Why is no real title available?)
• Verification of multi-linked heaps
• Separation logics and modalities: a survey
• Decision Procedure for Entailment of Symbolic Heaps with Arrays
• An efficient decision procedure for imperative tree data structures
• Decidable logics combining heap structures and data
• Quantitative separation logic and programs with lists
• A shape graph logic and a shape system

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

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