People
Alumni
Sacha Ayoun
Sacha was a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner. He completed his PhD in 2025. As an undergraduate, Sacha worked at the French Alternative and Atomic Energy Commission (CEA) as a researcher-engineer intern in 2017. His goal was to improve the Frame-C abstract interpreter to better handle file descriptors. In 2018 he completed his Supelec Engineer Diploma at CentraleSupelec as well as his MSc in Advanced Computing at Imperial.
Sacha was a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner. He completed his PhD in 2025. As an undergraduate, Sacha worked at the French Alternative and Atomic Energy Commission (CEA) as a researcher-engineer intern in 2017. His goal was to improve the Frame-C abstract interpreter to better handle file descriptors. In 2018 he completed his Supelec Engineer Diploma at CentraleSupelec as well as his MSc in Advanced Computing at Imperial.
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 Collage.com, Inc. a Michigan-based photo products e-commerce company.
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 Collage.com, Inc. a Michigan-based photo products e-commerce company.
Daiva Naudžiūnienė
Daiva defended her PhD 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.
Daiva defended her PhD 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.
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.
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.
Xiaojia Rao
Xiaojia was a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner. He completed his PhD in 2025. Xiaojia studied for his BA and MMath degree at the University of Cambridge and then moved to Imperial College London in 2020 to join the MSc in Advanced Computing. His Master’s thesis was on a verified model of WebAssembly in Coq called WasmCert-Coq.
Xiaojia was a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner. He completed his PhD in 2025. Xiaojia studied for his BA and MMath degree at the University of Cambridge and then moved to Imperial College London in 2020 to join the MSc in Advanced Computing. His Master’s thesis was on a verified model of WebAssembly in Coq called WasmCert-Coq.
Gabriela Sampaio
Gabriela was a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner. She completed her BSc and MSc at Federal University of Pernambuco (UFPE, Brazil), spending a year abroad at the University of Kent, working on the Erlang refactoring project (Wrangler). In 2022, Gabriela defended her PhD thesis, A Trusted Infrastructure for Symbolic Analysis of Event based Web APIS, and took up a position at Meta (formerly Facebook).
Gabriela was a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner. She completed her BSc and MSc at Federal University of Pernambuco (UFPE, Brazil), spending a year abroad at the University of Kent, working on the Erlang refactoring project (Wrangler). In 2022, Gabriela defended her PhD thesis, A Trusted Infrastructure for Symbolic Analysis of Event based Web APIS, and took up a position at Meta (formerly Facebook).
Julian Sutherland
Julian defended his PhD thesis, Compositional termination verification for fine-grained concurrency, in 2022. Julian is currently a Formal Verification Engineer at Nethermind, a blockchain company working on Ethereum.
Julian defended his PhD thesis, Compositional termination verification for fine-grained concurrency, in 2022. Julian is currently a Formal Verification Engineer at Nethermind, a blockchain company working on Ethereum.
Thomas Wood
Thomas was a PhD student with the group, working on software automated testing, verification and reasoning techniques and theory.
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.
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.
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
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.
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.
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.
Andreas Lööw
Andreas joined the group as a postdoctoral researcher in 2021, working on the formal foundations for Gillian. In 2025, he became a lecturer at Royal Holloway, University of London. Andreas did his PhD at Chalmers University of Technology, in Sweden, under the supervision of Magnus Myreen. At Chalmers, Andreas worked on interactive theorem proving for software and hardware correctness. Specifically, he worked on building trustworthy computer systems, known as verified stacks, with full-system correctness theorems. Much of his work revolved around trustworthy hardware, for example in the form of the development and verification of the Verilog synthesis tool Lutsig. Andreas defended his thesis, Building Verified Hardware and Verified Stacks in HOL, in September 2021.
Andreas joined the group as a postdoctoral researcher in 2021, working on the formal foundations for Gillian. In 2025, he became a lecturer at Royal Holloway, University of London. Andreas did his PhD at Chalmers University of Technology, in Sweden, under the supervision of Magnus Myreen. At Chalmers, Andreas worked on interactive theorem proving for software and hardware correctness. Specifically, he worked on building trustworthy computer systems, known as verified stacks, with full-system correctness theorems. Much of his work revolved around trustworthy hardware, for example in the form of the development and verification of the Verilog synthesis tool Lutsig. Andreas defended his thesis, Building Verified Hardware and Verified Stacks in HOL, in September 2021.
Petar Maksimović
Petar was a Research Fellow with the group and the Academic Program Manager for the Research Institute on Verified Trustworthy Software Systems (VeTSS) until his move to industry in 2022. Petar is also a Research Assistant Professor at the Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade.
Petar was a Research Fellow with the group and the Academic Program Manager for the Research Institute on Verified Trustworthy Software Systems (VeTSS) until his move to industry in 2022. Petar is also a Research Assistant Professor at the Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade.
Daniele Nantes
Daniele is a tenured assistant professor at the Department of Mathematics, University of Brasília, and collaborated with the group during a long sabbatical leave. Daniele’s research focuses on equational reasoning and comparative expressiveness of models and languages with concurrency. She was a researcher with the Theoretical Computer Science Group (GTC-UnB), and an external collaborator of the VIDI project Unifying Correctness for Communicating Systems. Her latest publications are Formalising nominal C-unification generalised with protected variables, published in Mathematical Structures for Computer Science, and the conference papers Nominal Equational Problems, published in ETAPS’ Foundations of Software Science and Computation Structures (FOSSACS 2021) series, and Non-deterministic Functions as Non-Deterministic Processes, in Formal Structures for Computation and Deduction (FSCD 2021) series.
Daniele is a tenured assistant professor at the Department of Mathematics, University of Brasília, and collaborated with the group during a long sabbatical leave. Daniele’s research focuses on equational reasoning and comparative expressiveness of models and languages with concurrency. She was a researcher with the Theoretical Computer Science Group (GTC-UnB), and an external collaborator of the VIDI project Unifying Correctness for Communicating Systems. Her latest publications are Formalising nominal C-unification generalised with protected variables, published in Mathematical Structures for Computer Science, and the conference papers Nominal Equational Problems, published in ETAPS’ Foundations of Software Science and Computation Structures (FOSSACS 2021) series, and Non-deterministic Functions as Non-Deterministic Processes, in Formal Structures for Computation and Deduction (FSCD 2021) series.