Language Specifiaction and Program Verification

Emanuele joined the group as a Marie-Curie Fellow in 2018 with his project “Verification through Security and Progress Abstractions” (VeSPA). In 2020 he moved to the Max Planck Institute for Software Systems (MPI-SWS), Germany, to work on the verification of concurrent programs with the IRIS program logic project.

Group Publications

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

   • Emanuele D’Osualdo
   • Azadeh Farzan
   • Philippa Gardner
   • Julian Sutherland

   Transactions on Programming Languages and Systems (TOPLAS) 2021

2. Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

   • Emanuele D’Osualdo
   • Felix Stutz

   Concurrency Theory (CONCUR) 2020

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

   • Emanuele D’Osualdo
   • Luke Ong
   • Alwen Tiu

   Computer Security Foundations Symposium (CSF) 2017