On Symbolic Heaps Modulo Permission Theories

DOI10.4230/LIPIcs.FSTTCS.2017.25zbMath1491.68050OpenAlexW2789677522MaRDI QIDQ5136317

Etienne Lozes, Stéphane P. Demri, Denis Lugiez

Publication date: 25 November 2020

Full work available at URL: https://hal-amu.archives-ouvertes.fr/hal-01788798

zbMATH Keywords

entailmentseparation logicpermissionreasoning modulo theories

Mathematics Subject Classification ID

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

Uses Software

• VeriFast
• CVC4
• SeLoger

Cites Work

• Unnamed Item
• Unnamed Item
• Tractable Reasoning in a Fragment of Separation Logic
• Permission accounting in separation logic
• The complexity of satisfiability problems
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science

This page was built for publication: On Symbolic Heaps Modulo Permission Theories