Zongyuan Liu | 刘宗源

As of 30 January 2026
A photo of Zongyuan Liu

I’m a PostDoc in the Logic and Semantics group at Department of Computer Science, Aarhus University, advised by Lars Birkedal. My research area is program verification. I am interested in developing tools for improving correctness and security of system software. Currently, I'm working with Jean Pichon-Pharabod on building advanced program logics for very relaxed memory models like Arm-A, and translation validation for realistic compilers like LLVM.

I can be reached at zy dot liu at cs dot au dot dk.

Publications

An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics
Zongyuan Liu, Angus Hammond, Thibaut Pérami, Peter Sewell, Lars Birkedal, and Jean Pichon Pharabod
TOPLAS
An extended version of POPL’24 paper
ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Zongyuan Liu, Nils Lauermann, Alasdair Armstrong, and Peter Sewell
POPL’26
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, and Jean Pichon Pharabod
POPL’24Pre-printSlides
These authors contributed equally.
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A
Zongyuan Liu, Sergei Stepanenko, Jean Pichon Pharabod, Amin Timany, Aslan Askarov, and Lars Birkedal
PLDI’23Pre-printSlides

Talks

A Separation Logic for Communicating Virtual Machines
Zongyuan Liu, Sergei Stepanenko, Jean Pichon Pharabod, Amin Timany, Aslan Askarov, and Lars Birkedal
Iris Workshop 2022Slides