A Logic-Based Framework for Reasoning about Composite Data Structures

DOI10.1007/978-3-642-04081-8_13zbMATH Open1254.68146OpenAlexW1503421880MaRDI QIDQ3184673FDOQ3184673

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (11)

• An efficient decision procedure for imperative tree data structures
• Separation logics and modalities: a survey
• Quantitative separation logic and programs with lists
• Decision Procedure for Entailment of Symbolic Heaps with Arrays
• Verification of multi-linked heaps
• A shape graph logic and a shape system
• Title not available (Why is that?)
• Decidable logics combining heap structures and data
• 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

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)