Value-Dependent Information-Flow Security on Weak Memory Models. - Graeme Smith 001; Nicholas Coughlin; Toby Murray (FM, 2019)

Rely/Guarantee Reasoning for Noninterference in Non-Blocking Algorithms. - Nicholas Coughlin; Graeme Smith 001 (CSF, 2020)

Backwards-directed information flow analysis for concurrent programs. - Kirsten Winter; Nicholas Coughlin; Graeme Smith 001 (CSF, 2021)

Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models. - Nicholas Coughlin; Kirsten Winter; Graeme Smith 001 (FM, 2021)

Information-flow control on ARM and POWER multicore processors. - Graeme Smith 001; Nicholas Coughlin; Toby Murray (Formal Methods Syst. Des., 2021)

Compositional noninterference on hardware weak memory models. - Nicholas Coughlin; Graeme Smith 001 (Sci. Comput. Program., 2022)

Lift-off: Trustworthy ARMv8 semantics from formal specifications. - Kait Lam; Nicholas Coughlin (FMCAD, 2023)

Compositional Reasoning for Non-multicopy Atomic Architectures. - Nicholas Coughlin; Kirsten Winter; Graeme Smith 001 (Formal Aspects Comput., 2023)

Detecting Speculative Execution Vulnerabilities on Weak Memory Models. - Nicholas Coughlin; Kait Lam; Graeme Smith 001; Kirsten Winter (FM (1), 2024)

Lift-Offline: Instruction Lifter Generators. - Nicholas Coughlin; Alistair Michael; Kait Lam (SAS, 2024)