| 2026 | FM | Generating Rely-Guarantee Conditions with the Conditional-Writes Domain. | James Tobler, Graeme Smith |
| 2026 | ISIT | Quantum f-divergences and Their Local Behaviour: An Analysis via Relative Expansion Coefficients. | Shreyas Iyer, Peixue Wu, Paula Belzig, Graeme Smith |
| 2025 | ISIT | Reverse-Type Data Processing Inequality. | Paula Belzig, Li Gao, Graeme Smith, Peixue Wu |
| 2025 | ISIT | Additivity of Quantum Capacities in Simple Non-Degradable Quantum Channels. | Graeme Smith, Peixue Wu |
| 2025 | TASE | Detecting Speculative Data Flow Vulnerabilities Using Weakest Precondition Reasoning. | Graeme Smith |
| 2024 | FM | Detecting Speculative Execution Vulnerabilities on Weak Memory Models. | Nicholas Coughlin, Kait Lam, Graeme Smith, Kirsten Winter |
| 2022 | ICFEM | Declassification Predicates for Controlled Information Release. | Graeme Smith |
| 2022 | ISIT | The platypus of the quantum channel zoo. | Felix Leditzky, Debbie W. Leung, Vikesh Siddhu, Graeme Smith, John A. Smolin |
| 2022 | ISIT | On the separation of correlation-assisted sum capacities of multiple access channels. | Akshay Seshadri, Felix Leditzky, Vikesh Siddhu, Graeme Smith |
| 2021 | FM | Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models. | Nicholas Coughlin, Kirsten Winter, Graeme Smith |
| 2020 | ISIT | A Tight Uniform Continuity Bound for Equivocation. | Mohammad A. Alhejji, Graeme Smith |
| 2019 | FM | Value-Dependent Information-Flow Security on Weak Memory Models. | Graeme Smith, Nicholas Coughlin, Toby Murray |
| 2019 | FM | Specification with Class: A Brief History of Object-Z. | Graeme Smith, David J. Duke |
| 2019 | FM | Weakening Correctness and Linearizability for Concurrent Objects on Multicore Processors. | Graeme Smith, Lindsay Groves |
| 2018 | FM | A Wide-Spectrum Language for Verification of Programs on Weak Memory Models. | Robert J. Colvin, Graeme Smith |
| 2018 | TASE | Observational Models for Linearizability Checking on Weak Memory Models. | Kirsten Winter, Graeme Smith, John Derrick |
| 2017 | FORTE | An Observational Approach to Defining Linearizability on Weak Memory Models. | John Derrick, Graeme Smith |
| 2017 | ICFEM | Improving the Scalability of Automatic Linearizability Checking in SPIN. | Patrick Doolan, Graeme Smith, Chenyi Zhang, Padmanabhan Krishnan |
| 2017 | ISIT | Degradable states and one-way entanglement distillation. | Felix Leditzky, Nilanjana Datta, Graeme Smith |
| 2017 | ITW | Quantum and private capacities of low-noise channels. | Felix Leditzky, Debbie W. Leung, Graeme Smith |
| 2016 | SAC | Invariant generation for linearizability proofs. | Graeme Smith, John Derrick |
| 2016 | SEFM | Model Checking Simulation Rules for Linearizability. | Graeme Smith |
| 2015 | ECOOP | Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. | Brijesh Dongol, John Derrick, Lindsay Groves, Graeme Smith |
| 2015 | FM | A Framework for Correctness Criteria on Weak Memory Models. | John Derrick, Graeme Smith |
| 2014 | ICTAC | Reasoning Algebraically About Refinement on TSO Architectures. | Brijesh Dongol, John Derrick, Graeme Smith |
| 2014 | IFM | Verifying Linearizability on TSO Architectures. | John Derrick, Graeme Smith, Brijesh Dongol |
| 2014 | SEFM | Using Z in the Development and Maintenance of Computational Models of Real-World Systems. | Shahrzad Moeiniyan Bagheri, Graeme Smith, Jim Hanan |
| 2014 | TASE | A Formal Development Approach for Self-Organising Systems. | Qin Li, Graeme Smith |
| 2013 | ICECCS | Using Bounded Fairness to Specify and Verify Ordered Asynchronous Multi-agent Systems. | Qin Li, Graeme Smith |
| 2012 | ICECCS | Reasoning About Adaptivity of Agents and Multi-agent Systems. | Graeme Smith, Jeffrey W. Sanders, Kirsten Winter |
| 2012 | ISIT | New constructions of codes for asymmetric channels via concatenation. | Markus Grassl, Peter W. Shor, Graeme Smith, John A. Smolin, Bei Zeng |
| 2012 | PST | Using conventional reasoning techniques for self-organising systems. | Graeme Smith, Jeff W. Sanders |
| 2012 | SEW | Incremental Development of Multi-agent Systems in Object-Z. | Graeme Smith, Kirsten Winter |
| 2011 | TASE | Refactoring Object-Oriented Specifications with Inheritance-Based Polymorphism. | Graeme Smith, Steffen Helke |
| 2010 | ISIT | Super-duper-activation of the zero-error quantum capacity. | Jianxin Chen, Toby S. Cubitt, Aram W. Harrow, Graeme Smith |
| 2010 | ITW | Quantum channel capacities. | Graeme Smith |
| 2009 | ATC | Formal Development of Self-organising Systems. | Graeme Smith, Jeffrey W. Sanders |
| 2008 | FM | Introducing Objects through Refinement. | Tim McComb, Graeme Smith |
| 2008 | ISIT | Codeword stabilized quantum codes. | Andrew W. Cross, Graeme Smith, John A. Smolin, Bei Zeng |
| 2008 | ISIT | Private classical capacity with symmetric assistance. | Graeme Smith |
| 2008 | ITW | Degenerate quantum codes and the quantum channel capacity problem. | Graeme Smith, John A. Smolin |
| 2008 | ITW | Additive extensions of a quantum channel. | Graeme Smith, John A. Smolin |
| 2008 | TASE | Towards More Flexible Development of Z Specifications. | Zheng Fu, Graeme Smith |
| 2007 | IFM | A Stepwise Development Process for Reasoning About the Reliability of Real-Time Systems. | Larissa Meinicke, Graeme Smith |
| 2006 | FM | Compositional Class Refinement in Object-Z. | Tim McComb, Graeme Smith |
| 2003 | SEFM | Animation of Object-Z Specifications Using a Z Animator. | Tim McComb, Graeme Smith |
| 2002 | ICFEM | Introducing Reference Semantics via Refinement. | Graeme Smith |
| 2002 | ICFEM | Abstract Specification in Object-Z and CSP. | Graeme Smith, John Derrick |
| 2002 | IFM | An Integration of Real-Time Object-Z and CSP for Specifying Concurrent Real-Time Systems. | Graeme Smith |
| 2001 | APSEC | Model Checking Object-Z Classes: Some Experiments with FDR. | Geoff Kassel, Graeme Smith |
| 2000 | IFM | Structural Refinement in Object-Z/CSP. | John Derrick, Graeme Smith |
| 2000 | IFM | Structuring Real-Time Object-Z Specifications. | Graeme Smith, Ian J. Hayes |
| 1999 | IFM | Towards Real-Time Object-Z. | Graeme Smith, Ian J. Hayes |
| 1997 | FM | A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems. | Graeme Smith |
| 1997 | FORTE | Combining CSP and Object-Z: Finite or Infinite Trace Semantics? | Clemens Fischer, Graeme Smith |
| 1997 | ICFEM | Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP. | Graeme Smith, John Derrick |
| 1997 | ICSE | The Second ISEW Cleanroom Workshop. | Graeme Smith |
| 1995 | APSEC | Reasoning about Object-Z Specifications. | Graeme Smith |
| 1994 | APSEC | Formal definitions of behavioural compatibility for active and passive objects. | Graeme Smith |
| 1990 | FORTE | Transferring Formal Techniques to Industry. | Roger Duke, Gordon A. Rose, Graeme Smith |
| 1989 | FORTE | Object-Z: An Object-Oriented Extension to Z. | David A. Carrington, David J. Duke, Roger Duke, Paul King, Gordon A. Rose, Graeme Smith |