Verified Software

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

   ACM Transactions on Programming Languages and Systems (TOPLAS), submitted Jan 2020; accepted 2021., vol. 43(4)

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

   • Emanuele D’Osualdo
   • Felix Stutz

   Proceedings of the 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), pp. 31:1–31:23

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

   Proceedings of 30^th IEEE Computer Security Foundations Symposium, (CSF 2017)