Emanuele D’Osualdo 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. Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

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

  2. (Submitted) TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

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

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