Reasoning About Sequences of Memory States

DOI10.1007/978-3-540-72734-7_8MaRDI QIDQ5434501zbMATH OpenOpenAlexFDO

Authors Rémi Brochenin, Stéphane Demri, Etienne Lozes

Publication date 4 January 2008

Published in Logical Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-72734-7_8

Mathematics Subject Classification ID

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

Recommendations

• Reasoning about sequences of memory states
• Checking satisfiability of two-dimensional logic PPTL\(^{\mathrm{SL}}\)
• Pointer logic for verification of pointer programs
• Verify heaps via unified model checking
• Program Verification with Separation Logic

Cited in

(8)

• Verify heaps via unified model checking
• Checking satisfiability of two-dimensional logic PPTL\(^{\mathrm{SL}}\)
• Using unified model checking to verify heaps
• On the Almighty Wand
• Automatically verifying temporal properties of pointer programs with cyclic proof
• On the complexity of pointer arithmetic in separation logic
• Reasoning about sequences of memory states
• Model checking dynamic memory allocation in operating systems

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 Q5434501)