48 citations · 91 across the 10 of their papers we have counts for
10 papers
First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation
Janine Lohse, Tim Rohde, Jimmy Xin +5
There has recently been exciting progress in the realm of probabilistic separation logics. An important subclass of these-including PSL, Lilac, Bluebell, and pcOL-are distributiona…
Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
Jialu Bao, Emanuele D'Osualdo, Azadeh Farzan
We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-st…
The Path to Durable Linearizability
Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis
There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a po…
Proving Hypersafety Compositionally
Emanuele D'Osualdo, Azadeh Farzan, Derek Dreyer
Hypersafety properties of arity are program properties that relate traces of a program (or, more generally, traces of programs). Classic examples include determinism, i…
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
Dan Frumin, Emanuele D'Osualdo, Bas van den Heuvel +1
The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical fo…
Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
Emanuele D'Osualdo, Felix Stutz
We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographi…
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner +1
We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how t…
On Hierarchical Communication Topologies in the pi-calculus
Emanuele D'Osualdo, C. -H. Luke Ong
This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if…
A Type System for proving Depth Boundedness in the pi-calculus
Emanuele D'Osualdo, Luke Ong
The depth-bounded fragment of the pi-calculus is an expressive class of systems enjoying decidability of some important verification problems. Unfortunately membership of the fragm…
Automatic Verification of Erlang-Style Concurrency
Emanuele D'Osualdo, Jonathan Kochems, C. -H. Luke Ong
This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs automatically. Inspired by Core Erlang, we introduce Lambda-Actor, a p…