I am interested in creating reliable and scalable software verification tools.
For my PhD, I am working on Gillian 2.0: a platform for compositional verification and
true bug-finding based on compositional symbolic execution. The platform is being
built both in OCaml, for efficient and pragmatic execution, and in Coq, for
providing formal guarantees behind the theory of the platform.
I am also working with the University of Oxford on formalising executable memory
semantics for the CHERI-C language using Isabelle/HOL. Using this work and Gillian, I
instantiated Gillian-CHERI-C: an automated verification tool for CHERI-C programs
that can catch temporal and spatial memory safety bugs. The tool will soon be extended
to work with the Gillian 2.0 platform.
I have also worked on verifying checkers for certified algorithms implemented in C using
Isabelle/HOL and AutoCorres.
2025–2025 The Theory and Practice of Concurrent Programming, Imperial College London, London, United Kingdom
Lecturer in Charge: Prof Alastair Donaldson and Dr Azalea Raad
Marked courseworks for the COMP 60007 – The Theory and Practice of Concurrent Programming module in Term 1, 2025.
2025–2025 Modal Logic for Strategic Reasoning, Imperial College London, London, United Kingdom
Lecturer in Charge: Dr Francesco Belardinelli
Marked courseworks for the COMP 70031 – Modal Logic for Strategic Reasoning module in Term 2, 2025.
2023–2024 Scalable Software Verification, Imperial College London, London, United Kingdom
Lecturer in Charge: Prof Philippa Gardner
Conducted tutorials, marked courseworks and assisted with the Gillian laboratory for the COMP 70023 – Scalable Software Verification module in Term 1, 2023.
2024–2024 Laboratory 2, Imperial College London, London, United Kingdom
Coordinator in Charge: Dr Mark Wheelhouse
Marked courseworks for the COMP 50007.1 – Laboratory 2 submodule in Term 2, 2024.
2024–2024 Compilers, Imperial College London, London, United Kingdom
Lecturer in Charge: Prof Paul Kelly
Marked courseworks for the COMP 50006 – Compilers module in Term 2, 2024.
2021–2021 Algorithmic Verification, University of New South Wales, Sydney, Australia
Lecturer in Charge: Dr Paul Hunter
Designed and conducted tutorials for the COMP3153/COMP9153 – Algorithmic Verification course in Term 2, 2021.
2020–2021 Algorithms, University of New South Wales, Sydney, Australia
Lecturer in Charge: AProf Aleksandar Ignjatovic
Managed student forums and marked students' assignments and final examinations
for the COMP3121 – Algorithms and Programming Techniques and COMP9101 – Design and Analysis of Algorithms courses held in Term 2, 2021 and Term 2, 2020.
2019–2020 Microprocessors and Interfacing, University of New South Wales, Sydney, Australia
Lecturer in Charge: Prof Sri Parameswaran
Managed student forums, conducted lab demonstrations and marked students' assessments for the COMP2121 – Microprocessors and Interfacing course in Term 1, 2019 and Term 1, 2020.
Seung Hoon Park, Rekha Pai, and Tom Melham.
A Formal CHERI-C Semantics for Verification. In Sriram
Sankaranarayanan and Natasha Sharygina, editors,
Tools and Algorithms for the Construction and Analysis
of Systems, volume 13993. Springer Cham, April 2023.
[ bib |
DOI |
.pdf ]
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Nat Karmios, Seung Hoon Park, Petar Maksimović, Philippa Gardner.
Unified Compositional Formal Methods: Exact Separation Logic
and the Gillian Platform for Correctness and Incorrectness
Reasoning. In
Formal Methods for Incorrectness, 2024.
[ bib |
.html |
.pdf ]
Andreas Lööw, Seung Hoon Park, Daniele Nantes-Sobrinho,
Sacha-Élie Ayoun, Opale Sjöstedt, and Philippa Gardner.
Compositional Symbolic Execution for the Next 700 Memory Models.
volume 9, New York, NY, USA, Oct 2025. Association for Computing
Machinery.
[ bib |
DOI |
.pdf |
talk ]
A BiBTeX file of the publications above is available here.
Attended the Systems, Programming, Languages, and Application: Software for Humanity (SPLASH) conference held in Singapore, 2025.
Presented "Compositional Symbolic Execution for the Next 700 Memory Models" in the Object-oriented Programming, Systems, Languages, and Application (OOPSLA) track.
Received funding and participated as a student volunteer.
2025 PLDI 2025 Student Volunteer, Seoul, South Korea
Attended the Programming Language Design and Implementation (PLDI) conference held in 2025.
Received funding and participated as a student volunteer.
2024 SSFT 2025 Assistant, Menlo College, California, United States
Attended the Fourteenth Summer School on Formal Techniques (SSFT) in 2025.
Assisted with the "Compositional Verification using the Gillian Platform" lectures and labs [ link | lab ].
2024 PLDI 2024 Artefact Evaluation Committee,
Reviewed artefacts for accepted papers in the Programming Language Design and Implementation (PLDI) conference.
2024 POPL 2024 Student Volunteer, Institution of Engineering and Technology, London, United Kingdom
Attended the Principles of Programming Languages (POPL) conference held in 2024.
Received funding and participated as a student volunteer.
2023 VeTSS 2023 Summer School Student, University of Surrey, Surrey, United Kingdom
Attended the Research Institute on Verified Trustworthy Software Systems Summer School held in University of Surrey, 2023.
2023 ETAPS 2023 Participant, Sorbonne Université and IHP, Paris, France
Attended the European joint conferences on Theory And Practice of Software held in Sorbonne Université and IHP, 2023.
Presented "A Formal CHERI-C Semantics for Verification" in the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
Received scholarship to attend the ETAPS Mentoring Workship (EMW).
2023 POPL 2023 Participant, Boston, United States
Attended the Principles of Programming Languages Conference in 2023.
Received full scholarship to attend both the conference and the Programming Languages Mentoring Workshop (PLMW).
2022 FLoC 2022 Participant, Technion-Israel Institute of Technology, Haifa, Israel
Attended the Federated Logic Conference held in Technion-Israel Institute of Technology, 2022.
2022 SPLV 2022 Student, Heriot-Watt University, Edinburgh, United Kingdom
Attended the Scottish Programming Languages and Verification Summer School held in Heriot-Watt University, 2022.
2022 MGS 2022 Student, University of Nottingham, Nottingham, United Kingdom
Attended the Midlands Graduate School in the Foundations of Computing Science held in the University of Nottingham, 2022.
2019 Exchange Student, Georgia Institute of Technology, Atlanta, United States
Attended Georgia Institute of Technology as an exchange student for the Fall 2019 semester.
This document was partially generated using the
LaTeX2HTML translator Version 2020.2 (Released July 1, 2020) and biblatex2html 1.99.
