Reasoning about sequences of memory states

DOI10.1016/J.APAL.2009.07.004MaRDI QIDQ636268zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

computational complexitytemporal logicseparation logicBüchi automaton

Mathematics Subject Classification ID

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

Recommendations

• Reasoning About Sequences of Memory States
• Checking satisfiability of two-dimensional logic PPTL\(^{\mathrm{SL}}\)
• On the complexity of pointer arithmetic in separation logic
• The power of modal separation logics
• On the complexity of modal separation logics

Cites work

• scientific article; zbMATH DE number 1617328 (Why is no real title available?)
• scientific article; zbMATH DE number 1670482 (Why is no real title available?)
• scientific article; zbMATH DE number 1956555 (Why is no real title available?)
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 2086598 (Why is no real title available?)
• A really temporal logic
• An automata-theoretic approach to branching-time model checking
• An automata-theoretic approach to constraint LTL
• BI as an assertion language for mutable data structures
• Beyond Shapes: Lists with Ordered Data
• Characterizing Provability in BI’s Pointer Logic Through Resource Graphs
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Foundations of Software Science and Computational Structures
• Many-dimensional modal logics: theory and applications
• Multi-dimensional modal logic as a framework for spatio-temporal reasoning
• On the Almighty Wand
• Programming Languages and Systems
• Programs with Lists Are Counter Automata
• Reasoning About Sequences of Memory States
• Reasoning about infinite computations
• Shape Analysis for Composite Data Structures
• Static Analysis
• Tableaux and resource graphs for separation logic
• The complexity of propositional linear temporal logics
• The effects of bounding syntactic resources on Presburger LTL
• Towards Model-Checking Programs with Lists
• Verification on infinite structures.

Cited in

(10)

• Separation logics and modalities: a survey
• On the almighty wand
• Tableaux methods for propositional dynamic logics with separating parallel composition
• On the complexity of pointer arithmetic in separation logic
• Regular patterns in second-order unification
• A complete axiomatisation for quantifier-free separation logic
• Reasoning About Sequences of Memory States
• Separation logic with one quantified variable
• Checking satisfiability of two-dimensional logic PPTL\(^{\mathrm{SL}}\)
• On temporal and separation logics

Describes a project that uses

Uses Software

• Smallfoot
• TVLA

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)