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

complexitypointer arithmeticseparation logic

Mathematics Subject Classification ID

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

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
• A complete axiomatisation for quantifier-free separation logic
• Reasoning about sequences of memory states

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)