VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. - Zongyuan Liu 001; Sergei Stepanenko; Jean Pichon-Pharabod; Amin Timany; Aslan Askarov; Lars Birkedal (Proc. ACM Program. Lang., 2023)

An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. - Angus Hammond; Zongyuan Liu 001; Thibaut Pérami; Peter Sewell; Lars Birkedal; Jean Pichon-Pharabod (Proc. ACM Program. Lang., 2024)