48 citations · 91 across the 10 of their papers we have counts for
5 papers · 1 filter
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…
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…
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…