Reference. The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
Cite
Cited by (1)
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants zilberstein-2026-probabilistic
Although randomization has long been used in distributed computing, formal methods for reasoning aboutprobabilistic concurrent programs have lagged behind. No existing program logics can express specificationsabout the full distributions of outcomes resulting from programs that are both probabilistic and concurrent. To address this, we introduce Probabilistic Concurrent Outcome Logic ( pcOL ), which incorporates ideas fromconcurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoningprinciples. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separationmodels probabilistic independence, so as to compositionally describe joint distributions over variables inconcurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to deriveprecise information about threads that rely on randomized shared state. We demonstrate pcOL on a variety ofexamples, including to prove almost sure termination of unbounded loops.
Cites 20 works (5 here)
With notes (5)
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic spies-2021-transfinitex
Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST timany-2017-a
We present a logical relations model of a higher-order functional programming language with impredicative polymorphism, recursive types, and a Haskell-style ST monad type with runST. We use our logical relations model to show that runST provides proper encapsulation of state, by showing that effectful computations encapsulated by runST are heap independent. Furthermore, we show that contextual refinements and equivalences that are expected to hold for pure computations do indeed hold in the presence of runST. This is the first time such relational results have been proven for a language with monadic encapsulation of state. We have formalized all the technical development and results in Coq.
Interactive proofs in higher-order concurrent separation logic krebbers-2017-interactive
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning jung-2015-iris
External (15)
- Oxidizing OCaml with Modal Memory Management (2024)
- Artifact for The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic (2024)
- Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (2023)
- A High-Level Separation Logic for Heap Space under Garbage Collection (2023)
- Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory (2023)
- Verifying a concurrent, crash-safe file system with sequential reasoning (2022)
- A separation logic for heap space under garbage collection (2022)
- Later credits: resourceful reasoning for the later modality (2022)
- Post-crash modality in Perennial's Coq Mechanization (software) (2022)
- GoJournal: a verified, concurrent, crash-safe journaling system (2021)
- Verifying concurrent, crash-safe systems with Perennial (2019)
- Mechanized relational verification of concurrent programs with continuations (2019)
- Certifying a file system using crash hoare logic (2017)
- Temporary Read-Only Permissions for Separation Logic (2017)
- The Essence of Higher-Order Concurrent Separation Logic (2017)