Foundations for entailment checking in quantitative separation logic

DOI10.1007/978-3-030-99336-8_3zbMATH Open1528.68208arXiv2201.11464OpenAlexW4226360391MaRDI QIDQ6166785FDOQ6166785

Authors: Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll 

Publication date: 3 August 2023

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

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.

Full work available at URL: https://arxiv.org/abs/2201.11464

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• Title not available (Why is that?)
• Deciding entailments in inductive separation logic with tree automata
• Title not available (Why is that?)
• BI as an assertion language for mutable data structures
• Probability and Computing
• Programming Languages and Systems
• A decision procedure for separation logic in SMT
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Abstraction, Refinement and Proof for Probabilistic Systems
• Tractable Reasoning in a Fragment of Separation Logic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Shape Analysis for Composite Data Structures
• Linear-invariant generation for probabilistic programs: automated support for proof-based methods
• The tree width of separation logic with recursive definitions
• Title not available (Why is that?)
• Viper: a verification infrastructure for permission-based reasoning
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Weakest precondition reasoning for expected runtimes of randomized algorithms
• Compositional shape analysis by means of bi-abduction
• Latticed \(k\)-induction with an application to probabilistic programs
• The effects of adding reachability predicates in propositional separation logic
• Verified tail bounds for randomized programs
• Unifying decidable entailments in separation logic with inductive definitions
• The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
• Foundations for decision problems in separation logic with general inductive predicates
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• Coupling proofs are probabilistic product programs

Cited In (2)

• A Splitting Algorithm Based on Soft Constraints for the Computation of Truth Degree in Quantitative Logic
• A specification logic for programs in the probabilistic guarded command language

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)