During his PhD studies, Zongyuan explored the application of separation logic to the verification of low-level systems. Separation logic is a verification technique that ensures software correctness and security by providing a formal framework for modular reasoning about complex program behaviours. However, applying separation logic to low-level systems is challenging, as it requires reasoning about intricate low-level behaviours while preserving high-level modularity.

Zongyuan investigated separation logic for two critical aspects of low-level systems: (1) virtual memory and memory sharing in system software, and (2) concurrency under relaxed hardware architectures. His research advances the understanding of separation logic as a modular approach to reasoning about these demanding aspects, laying the groundwork for rigorous verification of real-world software.

The PhD study was completed at Department of Computer Science, Faculty of Natural Sciences, Aarhus University.

This summary was prepared by the PhD student.

Time: Wednesday, 30 April 2025 at 13:00
Place: Building 5342, room 333, Department of Computer Science, Aarhus University, Åbogade 34, 8200 Aarhus N.
Title of PhD thesis: Separation Logic for Low-level and Realistic Programs
Contact information: Zongyuan Liu, e-mail: zy.liu@cs.au.dk, tel.: +45 50145213
Members of the assessment committee:
Faculty Tenured Researcher Viktor Vafeiadis, Max Planck Institute for Software systems, Germany
Research Professor Aleks Nanevski, IMDEA Software Institute, Spain
Professor Anders Møller (chair), Department of Computer Science, Aarhus University, Denmark
Main supervisor: Professor Lars Birkedal, Department of Computer Science, Aarhus University, Denmark
Co-supervisor: Tenure-track Assistant Professor Jean Pichon-Pharabod, Department of Computer Science, Aarhus University, Denmark
Language: The PhD dissertation will be defended in English
 

The defence is public.
The PhD thesis is available for reading at the Graduate School of Natural Sciences/GSNS, Ny Munkegade 120, building 1521, 8000 Aarhus C