I am interested in creatling 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.
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.
2023–2023 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.
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 Karmois, 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 ]
A BiBTeX file of the publications above is available here.
Will be reviewing artefacts for accepted papers in the upcoming 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.
