Yan Liu

About

I am a Research Fellow at the Australian National University (ANU) School of Computing (2025–), working on formal verification for secure embedded systems. My research sits at the intersection of formal methods, programming languages, and systems security, with a long-term goal of making formal verification a natural part of the software development lifecycle — specifically, automating the formalisation process to close the gap between verification’s clear value and its steep adoption barrier.

My background spans academia and industry across four countries. Before joining ANU I was a Staff Engineer at Pi Squared Inc. (2024–2025) working on zero-knowledge circuits and cross-chain protocols, and Rust Security Lead at Runtime Verification (2022–2024) developing Rust MIR semantics in the K Framework and leading smart contract audits. Earlier I was a Senior Engineer at AntGroup (2019–2022), a Sessional Lecturer at Monash University (2018–2019), and a Research Fellow at NUS / ADSC–UIUC (2013–2017).

I hold a PhD in Computer Science from the National University of Singapore (2014), where I was supervised by Prof. Jin Song Dong. My thesis applied model checking to pervasive computing systems.

Research

My current research programme centres on secure-by-construction embedded systems and AI-assisted verified software development, unified by a choreography-style language called ChorFi built on the seL4 microkernel.

• Fiducia — Secure-by-Construction Embedded Systems
  A DSL and toolchain for building information-flow-secure embedded systems on seL4. Developers express inter-device communication and intra-device computation in a single ChorFi choreography specification; safety, liveness, and non-interference are verified automatically at compile time via model checking and a sound security type system. Motto: if it compiles, security is guaranteed. Joint work with Prof. Alex Potanin, A/Prof. Alwen Tiu (ANU), and collaborators at UNSW and NUS.

Past Projects

• mir-semantics — Formal Semantics of Rust MIR in K
  Formal operational semantics of Rust’s Middle Intermediate Representation (MIR) in the K Framework, enabling concrete and symbolic execution of Rust programs, step-by-step state inspection, and a foundation for full formal verification. Ships as kmir, a Python front-end to the semantics. Developed at Runtime Verification (2022–2024).

Selected Publications

Journal Articles

• Scrutinizing Implementations of Smart Home Integrations
  K. Mahadewa, K. Wang, G. Bai, L. Shi, Y. Liu, J. S. Dong, Z. Liang
  IEEE Transactions on Software Engineering (TSE), vol. 47, no. 12, pp. 2667–2683, 2019
  [doi]
• Towards Formal Modelling and Verification of Pervasive Computing Systems
  Y. Liu, X. Zhang, Y. Liu, J. Sun, J. S. Dong, J. Biswas, M. Mokhtari
  Transactions on Computational Collective Intelligence (LNCS vol. 8780), pp. 62–91, 2014
  [doi]
• Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP
  J. Sun, Y. Liu, J. S. Dong, Y. Liu, L. Shi, É. André
  ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 22, no. 1, 2013
  [doi]

Conference Papers

• Smart Maintenance via Dynamic Fault Tree Analysis: A Case Study on Singapore MRT System
  Y. Liu, Y. Wu, Z. Kalbarczyk
  47th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 2017, pp. 511–518
  [doi]
• MDP-based Reliability Analysis of an Ambient Assisted Living System
  Y. Liu, L. Gui, Y. Liu
  FM 2014: Formal Methods (LNCS vol. 8442), pp. 688–702
  [doi]
• Formal Analysis of Pervasive Computing Systems
  Y. Liu, X. Zhang, Y. Liu, J. Sun, J. S. Dong, J. Biswas, M. Mokhtari
  17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2012, pp. 169–178
  [doi]
• Improved BDD-based Discrete Analysis of Timed Systems
  T. K. Nguyen, J. Sun, Y. Liu, J. S. Dong, Y. Liu
  FM 2012: Formal Methods (LNCS vol. 7436), pp. 326–340
  [doi]

Audit Reports & Technical Standards

• HydraDX Omnipool AMM — Security Audit
  Y. Liu et al. (Runtime Verification)
  Publicly available audit report, Runtime Verification, 2023
  [report]

Teaching & Service

Courses Taught

• FIT5171 Advanced Software Testing — Monash University, 2018–2019
  Sessional Lecturer (postgraduate) — formal testing, model-based testing, verification-based quality assurance
• FIT3013 Formal Methods — Monash University, 2018–2019
  Sessional Lecturer (undergraduate) — formal specification, model checking, theorem proving (PAT, Alloy)
• FIT2102 Programming Paradigms — Monash University, 2018–2019
  Sessional Lecturer (undergraduate) — functional programming in Haskell, type systems, higher-order functions

Contact