Reasoning about sequences of memory states
DOI10.1016/J.APAL.2009.07.004zbMATH Open1225.68068OpenAlexW1983255876MaRDI QIDQ636268FDOQ636268
Authors: Rémi Brochenin, Etienne Lozes, Stéphane 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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cites Work
- Title not available (Why is that?)
- Many-dimensional modal logics: theory and applications
- 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 constraint LTL
- Verification on infinite structures.
- Programming Languages and Systems
- Title not available (Why is that?)
- Tableaux and resource graphs for separation logic
- Reasoning about infinite computations
- Programs with Lists Are Counter Automata
- Multi-dimensional modal logic as a framework for spatio-temporal reasoning
- An automata-theoretic approach to branching-time model checking
- On the Almighty Wand
- Beyond Shapes: Lists with Ordered Data
- Title not available (Why is that?)
- Static Analysis
- The effects of bounding syntactic resources on Presburger LTL
- Shape Analysis for Composite Data Structures
- Title not available (Why is that?)
- Title not available (Why is that?)
- Towards Model-Checking Programs with Lists
- Characterizing Provability in BI’s Pointer Logic Through Resource Graphs
- Reasoning About Sequences of Memory States
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Foundations of Software Science and Computational Structures
Cited In (10)
- Checking satisfiability of two-dimensional logic PPTL\(^{\mathrm{SL}}\)
- Separation logics and modalities: a survey
- On the almighty wand
- Tableaux methods for propositional dynamic logics with separating parallel composition
- Regular patterns in second-order unification
- Reasoning About Sequences of Memory States
- Separation logic with one quantified variable
- Title not available (Why is that?)
- On the complexity of pointer arithmetic in separation logic
- On Temporal and Separation Logics
Uses Software
This page was built for publication: Reasoning about sequences of memory states
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q636268)
