Soter: an automatic safety verifier for erlang. - Emanuele D'Osualdo; Jonathan Kochems; Luke Ong (AGERE!@SPLASH, 2012)

Automatic Verification of Erlang-Style Concurrency. - Emanuele D'Osualdo; Jonathan Kochems; C.-H. Luke Ong (SAS, 2013)

A Type System for proving Depth Boundedness in the pi-calculus. - Emanuele D'Osualdo; Luke Ong (CoRR, 2015)

Verification of message passing concurrent systems. - Emanuele D'Osualdo (2015)

On Hierarchical Communication Topologies in the pi -calculus. - Emanuele D'Osualdo; C.-H. Luke Ong (ESOP, 2016)

First-order logic with reachability for infinite-state systems. - Emanuele D'Osualdo; Roland Meyer 001; Georg Zetzsche (LICS, 2016)

Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-Bounded Processes. - Emanuele D'Osualdo; Luke Ong; Alwen Tiu (CSF, 2017)

Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions. - Emanuele D'Osualdo; Felix Stutz (CONCUR, 2020)

TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs. - Emanuele D'Osualdo; Julian Sutherland; Azadeh Farzan; Philippa Gardner (ACM Trans. Program. Lang. Syst., 2021)

Proving hypersafety compositionally. - Emanuele D'Osualdo; Azadeh Farzan; Derek Dreyer (Proc. ACM Program. Lang., 2022)

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 001; Jorge A. Pérez 001 (Proc. ACM Program. Lang., 2022)

The Path to Durable Linearizability. - Emanuele D'Osualdo; Azalea Raad; Viktor Vafeiadis (Proc. ACM Program. Lang., 2023)

DimSum: A Decentralized Approach to Multi-language Semantics and Verification. - Michael Sammler; Simon Spies; Youngju Song; Emanuele D'Osualdo; Robbert Krebbers; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2023)

An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols. - Felix Stutz; Emanuele D'Osualdo (ESOP (2), 2025)

Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning. - Jialu Bao; Emanuele D'Osualdo; Azadeh Farzan (Proc. ACM Program. Lang., 2025)