Safety, relative tightness and the probabilistic frame rule

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

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.

• Jezik: Angleški jezik
• Ključne besede: probabilistic separation logic, separation logic, frame rule, partial state, operational semantics, partial correctness, total correctness, reasoning about independence
• Vrsta gradiva: Članek v reviji
• Tipologija: 1.08 - Objavljeni znanstveni prispevek na konferenci
• Organizacija: FMF - Fakulteta za matematiko in fiziko ; FRI - Fakulteta za računalništvo in informatiko
• Status publikacije: Objavljeno
• Različica publikacije: Objavljena publikacija
• Leto izida: 2025
• Št. strani: Str. 12-1-12-17
• PID: 20.500.12556/RUL-182236
• UDK: 510.6
• ISSN pri članku: 2969-2431
• DOI: 10.46298/entics.16743
• COBISS.SI-ID: 276910851
• Datum objave v RUL: 05.05.2026

Gradivo je del zbornika

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

Gradivo je del revije

• Naslov: Electronic notes in theorical informatics and computer science
• Skrajšan naslov: Electron. notes theor. inform. comput. sci.
• Založnik: INRIA
• ISSN: 2969-2431
• COBISS.SI-ID: 276891907

Licence

• Licenca: CC BY 4.0, Creative Commons Priznanje avtorstva 4.0 Mednarodna
• Povezava: http://creativecommons.org/licenses/by/4.0/deed.sl
• Opis: To je standardna licenca Creative Commons, ki daje uporabnikom največ možnosti za nadaljnjo uporabo dela, pri čemer morajo navesti avtorja.

Sekundarni jezik

• Jezik: Slovenski jezik
• Ključne besede: logika, semantika

Projekti

• Financer: ARIS - Javna agencija za znanstvenoraziskovalno in inovacijsko dejavnost Republike Slovenije
• Številka projekta: P1-0294
• Naslov: 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