Object-Z: An Object-Oriented Extension to Z. - David A. Carrington; David J. Duke; Roger Duke; Paul King; Gordon A. Rose; Graeme Smith 001 (FORTE, 1989)

Temporal Logic and Z Specifications. - Roger Duke; Graeme Smith 001 (Aust. Comput. J., 1989)

Transferring Formal Techniques to Industry. - Roger Duke; Gordon A. Rose; Graeme Smith 001 (FORTE, 1990)

Formalisation of behavioural and structural concepts for communication systems. - Paul King; Graeme Smith 001 (PSTV, 1990)

Associated Paper: The Object-Z Specification Language. - Roger Duke; Paul King; Gordon A. Rose; Graeme Smith 001 (TOOLS (5), 1991)

An object-oriented approach to formal specification - Graeme Smith 001 (1992)

Formal definitions of behavioural compatibility for active and passive objects. - Graeme Smith 001 (APSEC, 1994)

A Fully Abstract Semantics of Classes for Object-Z. - Graeme Smith 001 (Formal Aspects Comput., 1995)

A Blocking Model for Reactive Objects. - Roger Duke; Cecily Bailes; Graeme Smith 001 (Formal Aspects Comput., 1996)

A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems. - Graeme Smith 001 (FME, 1997)

Combining CSP and Object-Z: Finite or Infinite Trace Semantics? - Clemens Fischer; Graeme Smith 001 (FORTE, 1997)

Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP. - Graeme Smith 001; John Derrick (ICFEM, 1997)

Towards Real-Time Object-Z. - Graeme Smith 001; Ian J. Hayes (IFM, 1999)

Stepwise Development from Ideal Specifications. - Graeme Smith 001 (ACSC, 2000)

Structural Refinement in Object-Z/CSP. - John Derrick; Graeme Smith 001 (IFM, 2000)

Structuring Real-Time Object-Z Specifications. - Graeme Smith 001; Ian J. Hayes (IFM, 2000)

Incremental Development of Real-Time Requirements: The Light Control Case Study. - Graeme Smith 001; Colin J. Fidge (J. Univers. Comput. Sci., 2000)

Model Checking Object-Z Classes: Some Experiments with FDR. - Geoff Kassel; Graeme Smith 001 (APSEC, 2001)

Specification, Refinement and Verification of Concurrent Systems-An Integration of Object-Z and CSP. - Graeme Smith 001; John Derrick (Formal Methods Syst. Des., 2001)

Introducing Reference Semantics via Refinement. - Graeme Smith 001 (ICFEM, 2002)

Abstract Specification in Object-Z and CSP. - Graeme Smith 001; John Derrick (ICFEM, 2002)

An Integration of Real-Time Object-Z and CSP for Specifying Concurrent Real-Time Systems. - Graeme Smith 001 (IFM, 2002)

Encoding Object-Z in Isabelle/HOL. - Graeme Smith 001; Florian Kammüller; Thomas Santen (ZB, 2002)

An Introduction to Real-Time Object-Z. - Graeme Smith 001; Ian J. Hayes (Formal Aspects Comput., 2002)

Animation of Object-Z Specifications Using a Z Animator. - Tim McComb; Graeme Smith 001 (SEFM, 2003)

Proving Temporal Properties of Z Specifications Using Abstraction. - Graeme Smith 001; Kirsten Winter (ZB, 2003)

Compositional Verification for Object-Z. - Kirsten Winter; Graeme Smith 001 (ZB, 2003)

Structural Refinement of Systems Specified in Object-Z and CSP. - John Derrick; Graeme Smith 001 (Formal Aspects Comput., 2003)

Linear Temporal Logic and Z Refinement. - John Derrick; Graeme Smith 001 (AMAST, 2004)

Architectural Design in Object-Z. - Tim McComb; Graeme Smith 001 (Australian Software Engineering Conference, 2004)

Model Checking Z Specifications Using SAL. - Graeme Smith 001; Luke Wildman (ZB, 2005)

Preface. - Judi Romijn; Graeme Smith 001; Jaco van de Pol (IFM Doctoral Symposium, 2005)

Model Checking Downward Simulations. - Graeme Smith 001; John Derrick (REFINE, 2005)

Guest Editorial Integrated Formal Methods. - Eerke A. Boiten; John Derrick; Graeme Smith 001 (Formal Aspects Comput., 2005)

Compositional Class Refinement in Object-Z. - Tim McComb; Graeme Smith 001 (FM, 2006)

Simulation Machines for Checking Action System Refinements. - Graeme Smith 001; Kirsten Winter (Refine@ICFEM, 2006)

Verifying data refinements using a model checker. - Graeme Smith 001; John Derrick (Formal Aspects Comput., 2006)

A Stepwise Development Process for Reasoning About the Reliability of Real-Time Systems. - Larissa Meinicke; Graeme Smith 001 (IFM, 2007)

Preface. - Eerke A. Boiten; John Derrick; Graeme Smith 001 (REFINE@IFM, 2007)

Using Model Checking to Automatically Find Retrieve Relations. - John Derrick; Graeme Smith 001 (REFINE@IFM, 2007)

Introducing Objects through Refinement. - Tim McComb; Graeme Smith 001 (FM, 2008)

A Minimal Set of Refactoring Rules for Object-Z. - Tim McComb; Graeme Smith 001 (FMOODS, 2008)

Towards More Flexible Development of Z Specifications. - Zheng Fu; Graeme Smith 001 (TASE, 2008)

Refactoring Real-time Specifications. - Graeme Smith 001; Tim McComb (Refine@FM, 2008)

Formal Ensemble Engineering. - Jeffrey W. Sanders; Graeme Smith 001 (Software-Intensive Systems and New Computing Paradigms, 2008)

Formal Development of Self-organising Systems. - Graeme Smith 001; Jeffrey W. Sanders (ATC, 2009)

Refining Emergent Properties. - Jeff W. Sanders; Graeme Smith 001 (REFINE@FMWeek, 2009)

Model checking action system refinements. - Graeme Smith 001; Kirsten Winter (Formal Aspects Comput., 2009)

An Approach to Formal Verification of Free-Flight Separation. - Sebastian Eder; Graeme Smith 001 (SASO Workshops, 2010)

Gravity Points in Potential-Field Approaches to Self Organisation. - Aaron Sampson; Graeme Smith 001 (SASO Workshops, 2010)

Assuring Adaptive Behaviour in Self-Organising Systems. - Jeff W. Sanders; Graeme Smith 001 (SASO Workshops, 2010)

Editorial. - Eerke A. Boiten; Michael J. Butler; John Derrick; Graeme Smith 001 (Formal Aspects Comput., 2010)

Refactoring Object-Oriented Specifications with Inheritance-Based Polymorphism. - Graeme Smith 001; Steffen Helke (TASE, 2011)

Property transformation under specification change. - Zheng Fu; Graeme Smith 001 (Frontiers Comput. Sci. China, 2011)

Reasoning About Adaptivity of Agents and Multi-agent Systems. - Graeme Smith 001; Jeffrey W. Sanders; Kirsten Winter (ICECCS, 2012)

Using conventional reasoning techniques for self-organising systems. - Graeme Smith 001; Jeff W. Sanders (PST, 2012)

Incremental Development of Multi-agent Systems in Object-Z. - Graeme Smith 001; Kirsten Winter (SEW, 2012)

Temporal-logic property preservation under Z refinement. - John Derrick; Graeme Smith 001 (Formal Aspects Comput., 2012)

Emergence and refinement. - Jeff W. Sanders; Graeme Smith 001 (Formal Aspects Comput., 2012)

Using Bounded Fairness to Specify and Verify Ordered Asynchronous Multi-agent Systems. - Qin Li 002; Graeme Smith 001 (ICECCS, 2013)

A Refinement Framework for Autonomous Agents. - Qin Li 002; Graeme Smith 001 (SBMF, 2013)

MAZE: An Extension of Object-Z for Multi-Agent Systems. - Graeme Smith 001; Qin Li 002 (ABZ, 2014)

On Directional Bias for Network Coverage. - Graeme Smith 001; Jeff W. Sanders; Qin Li 002 (BIC-TA, 2014)

Admit Your Weakness: Verifying Correctness on TSO Architectures. - Graeme Smith 001; John Derrick; Brijesh Dongol (FACS, 2014)

Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures. - John Derrick; Graeme Smith 001; Lindsay Groves; Brijesh Dongol (Haifa Verification Conference, 2014)

Reasoning Algebraically About Refinement on TSO Architectures. - Brijesh Dongol; John Derrick; Graeme Smith 001 (ICTAC, 2014)

Verifying Linearizability on TSO Architectures. - John Derrick; Graeme Smith 001; Brijesh Dongol (IFM, 2014)

Using Z in the Development and Maintenance of Computational Models of Real-World Systems. - Shahrzad Moeiniyan Bagheri; Graeme Smith 001; Jim Hanan (SEFM Workshops, 2014)

A Formal Development Approach for Self-Organising Systems. - Qin Li 002; Graeme Smith 001 (TASE, 2014)

A macro-level model for investigating the effect of directional bias on network coverage. - Graeme Smith 001; Jeff W. Sanders; Qin Li 002 (CoRR, 2014)

Designing Adaptive Systems Using Teleo-Reactive Agents. - Graeme Smith 001; Jeff W. Sanders; Kirsten Winter (Trans. Comput. Collect. Intell., 2014)

A Macro-Level Model for Investigating the E ect of Directional Bias on Network Coverage. - Graeme Smith 001; Jeff W. Sanders; Qin Li 002 (ACSC, 2015)

Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. - Brijesh Dongol; John Derrick; Lindsay Groves; Graeme Smith 001 (ECOOP, 2015)

A Framework for Correctness Criteria on Weak Memory Models. - John Derrick; Graeme Smith 001 (FM, 2015)

Invariant generation for linearizability proofs. - Graeme Smith 001; John Derrick (SAC, 2016)

Model Checking Simulation Rules for Linearizability. - Graeme Smith 001 (SEFM, 2016)

Formal development of multi-agent systems using MAZE. - Qin Li 002; Graeme Smith 001 (Sci. Comput. Program., 2016)

A Proof Method for Linearizability on TSO Architectures. - John Derrick; Graeme Smith 001; Lindsay Groves; Brijesh Dongol (Provably Correct Systems, 2017)

An Observational Approach to Defining Linearizability on Weak Memory Models. - John Derrick; Graeme Smith 001 (FORTE, 2017)

Improving the Scalability of Automatic Linearizability Checking in SPIN. - Patrick Doolan; Graeme Smith 001; Chenyi Zhang 001; Padmanabhan Krishnan (ICFEM, 2017)

Refining autonomous agents with declarative beliefs and desires. - Qin Li 002; Graeme Smith 001 (Formal Aspects Comput., 2017)

Relating trace refinement and linearizability. - Graeme Smith 001; Kirsten Winter (Formal Aspects Comput., 2017)

A Wide-Spectrum Language for Verification of Programs on Weak Memory Models. - Robert J. Colvin; Graeme Smith 001 (FM, 2018)

Observational Models for Linearizability Checking on Weak Memory Models. - Kirsten Winter; Graeme Smith 001; John Derrick (TASE, 2018)

A sound and complete definition of linearizability on weak memory models. - Graeme Smith 001; Kirsten Winter; Robert J. Colvin (CoRR, 2018)

Correctness of Concurrent Objects under Weak Memory Models. - Graeme Smith 001; Kirsten Winter; Robert J. Colvin (Refine@FM, 2018)

A high-level operational semantics for hardware weak memory models. - Robert J. Colvin; Graeme Smith 001 (CoRR, 2018)

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

Specification with Class: A Brief History of Object-Z. - Graeme Smith 001; David J. Duke (FM Workshops (2), 2019)

Weakening Correctness and Linearizability for Concurrent Objects on Multicore Processors. - Graeme Smith 001; Lindsay Groves (FM Workshops (2), 2019)

Modelling concurrent objects running on the TSO and ARMv8 memory models. - Kirsten Winter; Graeme Smith 001; John Derrick (Sci. Comput. Program., 2019)

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

Linearizability on hardware weak memory models. - Graeme Smith 001; Kirsten Winter; Robert J. Colvin (Formal Aspects Comput., 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)

Declassification Predicates for Controlled Information Release. - Graeme Smith 001 (ICFEM, 2022)

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

A Dafny-based approach to thread-local information flow analysis. - Graeme Smith 001 (FormaliSE, 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)

Detecting Speculative Data Flow Vulnerabilities Using Weakest Precondition Reasoning. - Graeme Smith 001 (TASE, 2025)

On Formal Methods Thinking in Computer Science Education. - Brijesh Dongol; Catherine Dubois; Stefan Hallerstede; Eric C. R. Hehner; Carroll Morgan; Peter Müller 001; Leila Ribeiro 001; Alexandra Silva 001; Graeme Smith 001; Erik P. de Vink (Formal Aspects Comput., 2025)