Papers

• ESOP 2025
  session types, picalculus, concurrency, type systems, automata

  An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols

  • F. Stutz
  • E. D'Osualdo
• POPL 2025
  probabilistic, logics, separation

  Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning

  • J. Bao
  • E. D'Osualdo
  • A. Farzan
• POPL 2023
  linearizability, persistency, weak memory

  The Path to Durable Linearizability

  • E. D'Osualdo
  • A. Raad
  • V. Vafeiadis
• POPL 2023
  refinement

  DimSum: A Decentralized Approach to Multi-language Semantics and Verification

  • M. Sammler
  • S. Spies
  • Y. Song
  • E. D'Osualdo
  • R. Krebbers
  • D. Garg
  • D. Dreyer
• OOPSLA 2022
  logics, hyperproperties

  Proving Hypersafety Compositionally

  • E. D'Osualdo
  • A. Farzan
  • D. Dreyer
• OOPSLA 2022
  concurrency, separation, type systems, session types, logics

  A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency

  • D. Frumin
  • E. D'Osualdo
  • B. v/d Heuvel
  • J. A. Pérez
• TOPLAS 2021
  concurrency, separation, logics, linearisability, termination, liveness, fine-grained, VeSPA

  TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

  • E. D'Osualdo
  • J. Sutherland
  • A. Farzan
  • P. Gardner
• CONCUR 2020
  invariants, cryptographic protocol, wsts, decidability, VeSPA

  Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

  • E. D'Osualdo
  • F. Stutz
• CSF 2017
  secrecy, cryptographic protocol, wsts, decidability

  Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes

  • E. D'Osualdo
  • C.-H. L. Ong
  • A. Tiu
• LICS 2016
  valence, automata, logics, decidability

  First-order logic with reachability for infinite-state systems

  • E. D'Osualdo
  • R. Meyer
  • G. Zetzsche
• ESOP 2016
  picalculus, type systems, concurrency

  On Hierarchical Communication Topologies in the π-calculus

  • E. D'Osualdo
  • C.-H. L. Ong
• PhD Thesis 2015
  petri nets, erlang, static analysis, picalculus, type systems, concurrency, soter

  Verification of Message Passing Concurrent Systems

  • E. D'Osualdo
• CoRR 2015
  picalculus, type systems, automata

  A Type System for proving Depth Boundedness in the π-calculus

  • E. D'Osualdo
  • C.-H. L. Ong
• SAS 2013
  erlang, static analysis, verification, petri nets, concurrency, soter

  Automatic Verification of Erlang-Style Concurrency

  • E. D'Osualdo
  • J. Kochems
  • C.-H. L. Ong
• AGERE 2012
  tool, static analysis, erlang, soter

  Soter: An Automatic Safety Verifier for Erlang

  • E. D'Osualdo
  • J. Kochems
  • C.-H. L. Ong