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

    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

    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

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