| Naslov: | Safety, relative tightness and the probabilistic frame rule |
|---|
| Avtorji: | ID Jereb, Janez Ignacij (Avtor)
ID Simpson, Alex (Avtor) |
|---|
| Datoteke: |  PDF - Predstavitvena datoteka, prenos (505,93 KB)
MD5: 7DAC639C6B51BFF54BAE2F5E5956F3A4
 URL - Izvorni URL, za dostop obiščite https://entics.episciences.org/16743
|
|---|
| Jezik: | Angleški jezik |
|---|
| Tipologija: | 1.08 - Objavljeni znanstveni prispevek na konferenci |
|---|
| Organizacija: |  IMFM - Inštitut za matematiko, fiziko in mehaniko
|
|---|
| Povzetek: | 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. |
|---|
| Ključne besede: | probabilistic separation logic, separation logic, frame rule, partial state, operational semantics, partial correctness, total correctness, reasoning about independence |
|---|
| Status publikacije: | Objavljeno |
|---|
| Verzija publikacije: | Objavljena publikacija |
|---|
| Leto izida: | 2025 |
|---|
| Št. strani: | Str. 12-1-12-17 |
|---|
| PID: | 20.500.12556/DiRROS-29256  |
|---|
| UDK: | 510.6 |
|---|
| ISSN pri članku: | 2969-2431 |
|---|
| DOI: | 10.46298/entics.16743 |
|---|
| COBISS.SI-ID: | 276910851 |
|---|
| Opomba: |
|
|---|
| Datum objave v DiRROS: | 05.05.2026 |
|---|
| Število ogledov: | 179 |
|---|
| Število prenosov: | 92 |
|---|
| Metapodatki: |    |
|---|
|
:
|
Kopiraj citat |
|---|
| | | | Objavi na: |  |
|---|
Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše
podrobnosti ali sproži prenos. |
