A Replay-Oriented Software Architecture for Easy Debugging. - Chunhan Wu; Xingyuan Zhang; Yuanyuan Wang (CSSE (2), 2008)

A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). - Chunhan Wu; Xingyuan Zhang; Christian Urban (ITP, 2011)

The Myhill-Nerode Theorem Based on Regular Expressions. - Chunhan Wu; Xingyuan Zhang; Christian Urban (Arch. Formal Proofs, 2011)

A Formal Model and Correctness Proof for an Access Control Policy Framework. - Chunhan Wu; Xingyuan Zhang; Christian Urban (CPP, 2013)

A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions. - Chunhan Wu; Xingyuan Zhang; Christian Urban (J. Autom. Reason., 2014)

Priority Inheritance Protocol Proved Correct. - Xingyuan Zhang; Christian Urban; Chunhan Wu (J. Autom. Reason., 2020)