Dr Roger Su

Senior Research Associate

PhD Auckland 2022

Engineering
Computer Science and Engineering
Location
Desk 301.22, Level 3, Computer Science Building (K17)
  • Book Chapters | 2025
    Colvin RJ; Su RC, 2025, 'Structural Operational Semantics for Functional and Security Verification of Pipelined Processors', in Lecture Notes in Computer Science, Springer Nature Switzerland, pp. 363 - 388, http://dx.doi.org/10.1007/978-3-031-98668-0_18
    Book Chapters | 2024
    Colvin RJ; Hayes IJ; Heiner S; Höfner P; Meinicke L; Su RC, 2024, 'Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures', in Lecture Notes in Computer Science, Springer Nature Switzerland, pp. 65 - 87, http://dx.doi.org/10.1007/978-3-031-66676-6_4
  • Journal articles | 2026
    Su RC; Colvin RJ, 2026, 'Weak Memory Model Formalisms: Introduction and Survey', Concurrency and Computation: Practice and Experience, 38, http://dx.doi.org/10.1002/cpe.70484
    Journal articles | 2019
    Soo K-U; Stokes T, 2019, 'Algebraic properties of if-then-else and commutative three-valued tests', International Journal of Algebra and Computation, 29, pp. 743 - 759, http://dx.doi.org/10.1142/s0218196719500255
  • Working Papers | 2025
    Su R; Colvin RJ, 2025, Weak memory model formalisms: Introduction and survey, http://dx.doi.org, http://arxiv.org/abs/2508.04115
  • Conference Papers | 2025
    Colvin RJ; Heiner S; Höfner P; Su R, 2025, 'Rely-guarantee concurrency verification of queued locks in Isabelle/HOL', Menlo Park, California, USA, presented at Verified Software: Theory, Tools, and Experiments (VSTTE), Menlo Park, California, USA, 06 October 2025
    Software / Code | 2025
    Colvin RJ; Heiner S; Höfner P; Su R, 2025, Rely-guarantee extensions and locks, Archive of Formal Proofs, Published: 21 November 2025, Software / Code, http://www.isa-afp.org/entries/RG_Locks.html
    Conference Papers | 2019
    Chen S; Liu W; Liu J; Soo K-U; Chen W, 2019, 'Maximizing Social Welfare in Fractional Hedonic Games using Shapley Value', in 2019 IEEE International Conference on Agents (ICA), IEEE, pp. 21 - 26, presented at 2019 IEEE International Conference on Agents (ICA), 18 October 2019 - 21 October 2019, http://dx.doi.org/10.1109/agents.2019.8929212

I am a researcher in the field of Formal Methods, which studies mathematical methods for reasoning about various aspects of computing. 

As part of the Trustworthy Systems research group, I currently work on formal reasoning techniques for the correctness of schedulers. 

This is part of the PISTIs-V project, which aims to integrate the seL4 operating system microkernel with the RISC-V hardware architecture. More information can be found on the website of Trustworthy Systems group (below). 

In the recent past, I was a postdoctoral research fellow at the ANU, where I had worked on (1) models of hardware-level behaviours, and (2) computer-checked verification of concurrent programs.