Reasoning about sequences of memory states

DOI10.1016/j.apal.2009.07.004zbMath1225.68068OpenAlexW1983255876MaRDI QIDQ636268

Etienne Lozes, Rémi Brochenin, Stéphane P. Demri

Publication date: 26 August 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2009.07.004

zbMATH Keywords

computational complexitytemporal logicseparation logicBüchi automaton

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition ⋮ Regular Patterns in Second-Order Unification ⋮ Separation logic with one quantified variable ⋮ Separation logics and modalities: a survey ⋮ On the almighty wand ⋮ On Temporal and Separation Logics ⋮ Unnamed Item

Uses Software

• Smallfoot
• TVLA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An automata-theoretic approach to constraint LTL
• Reasoning about infinite computations
• Many-dimensional modal logics: theory and applications
• Multi-dimensional modal logic as a framework for spatio-temporal reasoning
• Tableaux and Resource Graphs for Separation Logic
• On the Almighty Wand
• Beyond Shapes: Lists with Ordered Data
• Towards Model-Checking Programs with Lists
• The Effects of Bounding Syntactic Resources on Presburger LTL
• The complexity of propositional linear temporal logics
• A really temporal logic
• BI as an assertion language for mutable data structures
• An automata-theoretic approach to branching-time model checking
• Characterizing Provability in BI’s Pointer Logic Through Resource Graphs
• Shape Analysis for Composite Data Structures
• Reasoning About Sequences of Memory States
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Static Analysis
• Programming Languages and Systems
• Foundations of Software Science and Computational Structures
• Programs with Lists Are Counter Automata