Safety, relative tightness and the probabilistic frame rule

Jereb, Janez Ignacij (author), Simpson, Alex (author)

Probabilistic separation logic offers an approach to reasoning about imperative probabilistic programs in which a separating conjunction is used as a mechanism for expressing independence properties. Crucial to the effectiveness of the formalism is the frame rule, which enables modular reasoning about independent probabilistic state. We explore a semantic formulation of probabilistic separation logic, in which the frame rule has the same simple formulation as in separation logic, without further side conditions. This is achieved by building a notion of safety into specifications, using which we establish a crucial property of specifications, called relative tightness, from which the soundness of the frame rule follows.

• Language: English
• Keywords: probabilistic separation logic, separation logic, frame rule, partial state, operational semantics, partial correctness, total correctness, reasoning about independence
• Work type: Article
• Typology: 1.08 - Published Scientific Conference Contribution
• Organization: FMF - Faculty of Mathematics and Physics; FRI - Faculty of Computer and Information Science
• Publication status: Published
• Publication version: Version of Record
• Year: 2025
• Number of pages: Str. 12-1-12-17
• PID: 20.500.12556/RUL-182236
• UDC: 510.6
• ISSN on article: 2969-2431
• DOI: 10.46298/entics.16743
• COBISS.SI-ID: 276910851
• Publication date in RUL: 05.05.2026

Record is a part of a proceedings

• Title: Proceedings of MFPS XLI
• COBISS.SI-ID: 276899075

Record is a part of a journal

• Title: Electronic notes in theorical informatics and computer science
• Shortened title: Electron. notes theor. inform. comput. sci.
• Publisher: INRIA
• ISSN: 2969-2431
• COBISS.SI-ID: 276891907

Licences

• License: CC BY 4.0, Creative Commons Attribution 4.0 International
• Link: http://creativecommons.org/licenses/by/4.0/
• Description: This is the standard Creative Commons license that gives others maximum freedom to do what they want with the work as long as they credit the author.

Secondary language

• Language: Slovenian
• Keywords: logika, semantika

Projects

• Funder: ARIS - Slovenian Research and Innovation Agency
• Project number: P1-0294
• Name: Računsko intenzivne metode v teoretičnem računalništvu, diskretni matematiki, kombinatorični optimizaciji ter numerični analizi in algebri z uporabo v naravoslovju in družboslovju