Seung Hoon (Simon) Park

Profile picture of Seung Hoon Park PhD Student, Imperial College London

Email
semail obfustication.park23@imperiemail obfusticational.ac.uk [Public PGP key]

Address
Department of Computing
Imperial College London
South Kensington Campus
London, SW7 2AZ, United Kingdom

Phone
+44 (0)7710 279760


Research Interests

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.

Education

2023–2027 PhDImperial College London, London, United Kingdom
  • Supervisor: Prof Philippa Gardner
  • Subject: Computer Science
2020–2021 BSc (Hons)University of New South Wales, Sydney, Australia
  • Thesis: Interaction Trees in Isabelle/HOL
  • Supervisor: Dr Christine Rizkallah
  • Subject: Computer Science
  • Awarded with First Class Honours (H1)
2017–2020 BScUniversity of New South Wales, Sydney, Australia
  • Subject: Computer Science, Mathematics
  • Awarded with Distinction

Research

2021–2023 Research Assistant (Full-time)University of Oxford, Oxford, United Kingdom
  • Supervisor: Prof Thomas Melham
  • Working as part of the SCorCH project funded under Digital Security by Design.
  • Conducting research on formalising a CHERI-C memory model for automated verification.
2019–2021 Research Assistant (Part-time)University of New South Wales, Sydney, Australia
  • Supervisor: Dr Christine Rizkallah
  • Worked on verifying a C implementation of the Shortest Path Checker algorithm in Isabelle/HOL.
2018–2019 Taste of Research Scholar (Full-time)Data61 CSIRO, Sydney, Australia
  • Supervisor: Dr Christine Rizkallah
  • Worked on C implementation of the Shortest Path Checker algorithm for verification in Isabelle/HOL.

Teaching

2024–2024 Laboratory 2Imperial 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 CompilersImperial 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 VerificationImperial 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 VerificationUniversity 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 AlgorithmsUniversity 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 InterfacingUniversity 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.

Honours, Scholarships and Awards

2023–2027 Imperial College London Doctoral Scholarship Award.
2023–2023 EMW @ ETAPS 2023 Scholarship.
2022–2023 PLMW @ POPL 2023 Scholarship.
2019–2019 UNSW Student Exchange Achievement Award.
2018–2019 UNSW Engineering Taste of Research Scholarship.
2018–2019 UNSW Engineering Dean's Honours List.

Publications

[1] Seung Hoon Park. A Formal CHERI-C Memory Model. Archive of Formal Proofs, Nov 2022. Formal proof development. [ bib | .html ]
[2] 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 ]
[3] 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.

Miscellaneous

2024 PLDI 2024 Artefact Evaluation Committee
  • Will be reviewing artefacts for accepted papers in the upcoming Programming Language Design and Implementation (PLDI) conference.
2024 POPL 2024 Student VolunteerInstitution 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 StudentUniversity 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 ParticipantSorbonne 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 ParticipantBoston, 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 ParticipantTechnion-Israel Institute of Technology, Haifa, Israel
  • Attended the Federated Logic Conference held in Technion-Israel Institute of Technology, 2022.
2022 SPLV 2022 StudentHeriot-Watt University, Edinburgh, United Kingdom
  • Attended the Scottish Programming Languages and Verification Summer School held in Heriot-Watt University, 2022.
2022 MGS 2022 StudentUniversity 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 StudentGeorgia 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.

The translation was initiated on 2023-03-02.