On the complexity of pointer arithmetic in separation logic

DOI10.1007/978-3-030-02768-1_18MaRDI QIDQ6166154zbMATH OpenOpenAlexFDO

Authors James Brotherston, Max Kanovich

Publication date 2 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://discovery.ucl.ac.uk/id/eprint/10074307/

zbMATH Keywords

complexityseparation logicpointer arithmetic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Tractable Reasoning in a Fragment of Separation Logic
• Reasoning about sequences of memory states
• The SAT-based approach to separation logic
• Reasoning About Sequences of Memory States
• Tractability of separation logic with inductive definitions: beyond lists

Cited in

(3)

• Compositional satisfiability solving in separation logic
• Reasoning about sequences of memory states
• A complete axiomatisation for quantifier-free separation logic

This page was built for publication: On the complexity of pointer arithmetic in separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166154)