Foundations for entailment checking in quantitative separation logic
From MaRDI portal
Publication:6166785
Abstract: Quantitative separation logic (QSL) is an extension of separation logic (SL) for the verification of probabilistic pointer programs. In QSL, formulae evaluate to real numbers instead of truth values, e.g., the probability of memory-safe termination in a given symbolic heap. As with SL, one of the key problems when reasoning with QSL is emph{entailment}: does a formula f entail another formula g? We give a generic reduction from entailment checking in QSL to entailment checking in SL. This allows to leverage the large body of SL research for the automated verification of probabilistic pointer programs. We analyze the complexity of our approach and demonstrate its applicability. In particular, we obtain the first decidability results for the verification of such programs by applying our reduction to a quantitative extension of the well-known symbolic-heap fragment of separation logic.
Recommendations
- scientific article; zbMATH DE number 1140581
- Compositional entailment checking for a fragment of separation logic
- Compositional entailment checking for a fragment of separation logic
- On elementary logics for quantitative dependencies
- A complete axiomatisation for quantifier-free separation logic
- Effective entailment checking for separation logic with inductive definitions
- On propositional quantifiers in provability logic
- Characterizing quantifier extensions of dependence logic
- scientific article; zbMATH DE number 2062214
- scientific article; zbMATH DE number 5295712
Cites work
- scientific article; zbMATH DE number 3165828 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 3615887 (Why is no real title available?)
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- A decision procedure for separation logic in SMT
- Abstraction, Refinement and Proof for Probabilistic Systems
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- BI as an assertion language for mutable data structures
- Compositional shape analysis by means of bi-abduction
- Coupling proofs are probabilistic product programs
- Deciding entailments in inductive separation logic with tree automata
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Foundations for decision problems in separation logic with general inductive predicates
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Latticed \(k\)-induction with an application to probabilistic programs
- Linear-invariant generation for probabilistic programs: automated support for proof-based methods
- Probability and Computing
- Programming Languages and Systems
- Shape Analysis for Composite Data Structures
- The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
- The effects of adding reachability predicates in propositional separation logic
- The tree width of separation logic with recursive definitions
- Tractable Reasoning in a Fragment of Separation Logic
- Unifying decidable entailments in separation logic with inductive definitions
- Verified tail bounds for randomized programs
- Viper: a verification infrastructure for permission-based reasoning
- Weakest precondition reasoning for expected runtimes of randomized algorithms
Cited in
(2)
This page was built for publication: Foundations for entailment checking in quantitative separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166785)
