معرفی
Emanuele D’Osualdo is a Tenure-track Professor of Formal Methods for Software Engineering at the University of Konstanz. Previously, he held postdoctoral positions at MPI-SWS Saarbrücken (2020-2024) under Derek Dreyer and at Imperial College London (2015-2020) as a Marie Curie Fellow under Prof. P. Gardner. His research focuses on formal methods for software verification, including static analysis, model checking, and compositional verification techniques for concurrent and probabilistic systems.
Research interests span Programming Languages, Verification, Security, Concurrency Theory, and Probabilistic Programming. Notable contributions include the Soter tool for Erlang verification, the James Bound library for π-calculus analysis, and foundational work on hierarchical communication topologies. His 2016 doctoral thesis on concurrency verification earned the CPHC/BCS Distinguished Dissertation Award.
Recent work includes Bluebell (POPL 2025), advancing probabilistic reasoning via relational lifting, and compositional approaches to hypersafety (OOPSLA 2022). Active in academic service, he has delivered keynotes at HYPER’25 and participates in major conferences like CAV and POPL.
- Awards: 2016 CPHC/BCS Distinguished Dissertation Award
- Tools: Soter (Erlang verifier), James Bound (π-calculus library)
- Grants/Advising: Supervises graduate students at University of Konstanz (details forthcoming)
Led the Formal Methods research group focused on concurrency, security, and probabilistic systems at the University of Konstanz.
