On Symbolic Heaps Modulo Permission Theories
From MaRDI portal
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25)
Recommendations
- Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
- Decidability for entailments of symbolic heaps with arrays
- Satisfiability modulo heap-based programs
- Modular reasoning about heap paths via effectively propositional formulas
- Reasoning in the theory of heap: satisfiability and interpolation
- Model and proof generation for heap-manipulating programs
- Logical characterizations of heap abstractions
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- Verified heap theorem prover by paramodulation
- Verify heaps via unified model checking
Cites work
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- scientific article; zbMATH DE number 1948162 (Why is no real title available?)
- scientific article; zbMATH DE number 2090840 (Why is no real title available?)
- Permission accounting in separation logic
- The complexity of satisfiability problems
- Tractable Reasoning in a Fragment of Separation Logic
Cited in
(3)
This page was built for publication: On Symbolic Heaps Modulo Permission Theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5136317)
