Foundations for entailment checking in quantitative separation logic

DOI10.1007/978-3-030-99336-8_3zbMath1528.68208arXiv2201.11464OpenAlexW4226360391MaRDI QIDQ6166785

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

Publication date: 3 August 2023

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

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

Mathematics Subject Classification ID

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

Related Items (1)

A specification logic for programs in the probabilistic guarded command language

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• 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
• A decision procedure for separation logic in SMT
• Unifying decidable entailments in separation logic with inductive definitions
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Tractable Reasoning in a Fragment of Separation Logic
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
• Abstraction, Refinement and Proof for Probabilistic Systems
• The Tree Width of Separation Logic with Recursive Definitions
• Linear-Invariant Generation for Probabilistic Programs:
• The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates
• BI as an assertion language for mutable data structures
• Coupling proofs are probabilistic product programs
• Compositional Shape Analysis by Means of Bi-Abduction
• Foundations for Decision Problems in Separation Logic with General Inductive Predicates
• Shape Analysis for Composite Data Structures
• Probability and Computing
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programming Languages and Systems
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

This page was built for publication: Foundations for entailment checking in quantitative separation logic