Photo of Sacha Ayoun
Sacha Ayoun
PhD Student
Photo of Philippa Gardner
Philippa Gardner
Professor, Group Leader
Photo of Xiaojia Rao
Xiaojia Rao
PhD Student


Pedro da Rocha Pinto Pedro was a PhD student and a Post Doc in the group, working on developing logics for verification of fine-grained concurrent programs. Pedro defended his PhD thesis, Reasoning with Time and Data Abstractions in January 2017. He is currently working for, Inc. a Michigan-based photo products e-commerce company.

Daiva Naudžiūnienė Daiva defended her Ph.D. on An Infrastructure for Tractable Verification of JavaScript Programs in March 2018. Since 2017, Daiva has been working as a Research Scientist at Facebook as part of the engineering team led by Peter O’Hearn.

Gian Ntzik Gian was a PhD student and Post Doc with the group. Gian defended his thesis Reasoning about POSIX File Systems in February 2017 and is currently working for Amadeus in systems development and research.

Azalea Raad Azalea was a PhD student with the group, defending her thesis on Abstraction, Refinement and Concurrent Reasoning in February 2017. She then moved to the Max Planck Institute for Software Systems (Kaiserslautern) working a postdoctoral researcher with Derek Dreyer and Viktor Vafeiadis on the ERC RustBelt project. In 2020, Azalea joined the faculty at Imperial College London as a lecturer.

Thomas Wood Thomas was a PhD student with the group, working on software automated testing, verification and reasoning techniques and theory.

Shale Xiong Shale was a PhD student with the group. Shale defended his thesis: Parametric Operational Semantics for Consistency Models in February 2020 and he is currently working for Arm Research, Cambridge, as a Research Engineer in their Security group.

Martin Bodin Martin joined the group as a Research Associate in 2018. His work focused on a formalism called skeletons to represent the semantics of real-world programming languages (JavaScript, R, etc.) He also was part of the team working on the formalisation of WebAssembly/Wasm in Coq. In 2020 Martin was appointed CRCN (chargé de recherche de classe normale) in the Sound Programming of Adaptive Dependable Embedded Systems (Spades) group at Inria Grenoble-Rhône-Alpes Research Centre, France.

Andrea Cerone Andrea joined the group as a Research Associate in 2016. He left Imperial College in 2019, to move to industry. He is still an active researcher, continuing his work on the mathematical foundations of geo-replicated and distributed systems, with a particular emphasis to databases, and its applications for overcoming practical challenges in such systems. His latest publication is Data Consistency in Transactional Storage Systems: A Centralised Semantics at Ecoop 2020

Emanuele D'Osualdo 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.

José Fragoso Santos José joined the group as a Research Associate in 2015, working on program analysis and JavaScript Verification. He is now an Assistant Professor at the Instituto Superior Técnico, Lisbon, Portugal.