| Title: | Safety, relative tightness and the probabilistic frame rule |
|---|
| Authors: | ID Jereb, Janez Ignacij (Author)
ID Simpson, Alex (Author) |
|---|
| Files: |  PDF - Presentation file, download (505,93 KB)
MD5: 7DAC639C6B51BFF54BAE2F5E5956F3A4
 URL - Source URL, visit https://entics.episciences.org/16743
|
|---|
| Language: | English |
|---|
| Typology: | 1.08 - Published Scientific Conference Contribution |
|---|
| Organization: |  IMFM - Institute of Mathematics, Physics, and Mechanics
|
|---|
| Abstract: | 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. |
|---|
| Keywords: | probabilistic separation logic, separation logic, frame rule, partial state, operational semantics, partial correctness, total correctness, reasoning about independence |
|---|
| Publication status: | Published |
|---|
| Publication version: | Version of Record |
|---|
| Year of publishing: | 2025 |
|---|
| Number of pages: | Str. 12-1-12-17 |
|---|
| PID: | 20.500.12556/DiRROS-29256  |
|---|
| UDC: | 510.6 |
|---|
| ISSN on article: | 2969-2431 |
|---|
| DOI: | 10.46298/entics.16743 |
|---|
| COBISS.SI-ID: | 276910851 |
|---|
| Note: |
|
|---|
| Publication date in DiRROS: | 05.05.2026 |
|---|
| Views: | 182 |
|---|
| Downloads: | 92 |
|---|
| Metadata: |    |
|---|
|
:
|
Copy citation |
|---|
| | | | Share: |  |
|---|
Hover the mouse pointer over a document title to show the abstract or click
on the title to get all document metadata. |
