Overview
Background
Associate Professor Graeme Smith has over 100 publications in the area of formal, i.e., mathematically based, design and analysis of software and software-based systems. His seminal work on formal object-oriented modelling has found application in the telecommunications and railways sectors, and that on real-time embedded systems in the Defence sector. He has worked at the Software Verification Research Centre (Australia), GMD First (Germany), the Technical University of Berlin (Germany), and the Centre de Recherche en Informatique de Nancy (France). Since his current appointment at The University of Queensland, he has led 3 ARC Discovery Grants on formal design and analysis of fault-tolerant systems, distributed autonomous systems, and lock-free concurrent algorithms, respectively. He currently leads a research cell of the Defence Science and Technology Group focussed on formal security analysis of concurrent code.
Availability
- Associate Professor Graeme Smith is:
- Available for supervision
- Media expert
Fields of research
Qualifications
- Bachelor (Honours) of Engineering, The University of Queensland
- Doctor of Philosophy, The University of Queensland
Research interests
-
Formal Methods
Formal, i.e., mathematically based, design and analysis of software and software-based systems. Primary expertise lies in the application of formal techniques to functional correctness and security of concurrent programs. In particular, techniques based on refinement for functional correctness, and information flow for security. Secondary expertise lies in the formal design and analysis of component-based systems, including highly distributed systems such as self-organising and multi-agent systems, and object-oriented programs where expertise extends to formal refactoring techniques for improving object-oriented designs.
Research impacts
Associate Professor Graeme Smith’s research has had the following impact outside of academia:
His research on formal obejct-oriented modelling has been used
-
to specify and verify the design of a fault-tolerant telecommunications platform for the Overseas Telecommunications Corporation, Australia, in 1989
-
in business process specifications at Bellcore, New Jersey, USA, in 1994
-
in the description of the ISO standard, PREMO (Presentation Environments for Multimedia Objects) in 1994
-
in software engineering projects at Motorola, Arizona, USA, in 1999
-
in a Queensland Rail project for documenting design specifications for interlocking systems in 2003
His research into modelling continuous, real-time systems was used to improve the quality of the documentation of requirements for the flight control unit of the Nulka Active Missile Decoy being developed by BAE Systems, Australia, in 2000.
His ARC Discovery Grant research on fault-tolerant systems was adopted by the Defence Signals Directorate, Australia, for verifying a fault-tolerant security device in 2007.
His ARC Discovery Grant research on model checking concurrent objects was the subject of a joint patent application with Oracle Labs, Australia, in 2016.
Works
Search Professor Graeme Smith’s works on UQ eSpace
Featured
2019
Journal Article
Linearizability on hardware weak memory models
Smith, Graeme, Winter, Kirsten and Colvin, Robert J. (2019). Linearizability on hardware weak memory models. Formal Aspects of Computing, 32 (1), 1-32. doi: 10.1007/s00165-019-00499-8
Featured
2019
Conference Publication
Value-dependent information-flow security on weak memory models
Smith, Graeme, Coughlin, Nicholas and Murray, Toby (2019). Value-dependent information-flow security on weak memory models. Third World Congress, FM 2019, Porto, Portugal, 7-11 October 2019. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-30942-8_32
Featured
2018
Conference Publication
A wide-spectrum language for verification of programs on weak memory models
Colvin, Robert J. and Smith, Graeme (2018). A wide-spectrum language for verification of programs on weak memory models. 22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 15-17 July 2018. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-95582-7_14
Featured
2017
Journal Article
Relating trace refinement and linearizability
Smith, Graeme and Winter, Kirsten (2017). Relating trace refinement and linearizability. Formal Aspects of Computing, 29 (6), 1-16. doi: 10.1007/s00165-017-0418-2
Featured
2016
Journal Article
Formal development of multi-agent systems using MAZE
Li, Qin and Smith, Graeme (2016). Formal development of multi-agent systems using MAZE. Science of Computer Programming, 131, 126-150. doi: 10.1016/j.scico.2016.04.008
Featured
2012
Journal Article
Emergence and refinement
Sanders, J. W. and Smith, Graeme (2012). Emergence and refinement. Formal Aspects of Computing, 24 (1), 45-65. doi: 10.1007/s00165-011-0190-7
Featured
1999
Book
The Object-Z Specification Language
Smith, G. P. (1999). The Object-Z Specification Language. Boston: Kluwer Academic Publishers. doi: 10.1007/978-1-4615-5265-9
2024
Book Chapter
Detecting Speculative Execution Vulnerabilities on Weak Memory Models
Coughlin, Nicholas, Lam, Kait, Smith, Graeme and Winter, Kirsten (2024). Detecting Speculative Execution Vulnerabilities on Weak Memory Models. Lecture Notes in Computer Science. (pp. 482-500) Cham: Springer Nature Switzerland. doi: 10.1007/978-3-031-71162-6_25
2024
Journal Article
On Formal Methods Thinking in Computer Science Education
Dongol, Brijesh, Dubois, Catherine, Hallerstede, Stefan, Hehner, Eric, Morgan, Carroll, Müller, Peter, Ribeiro, Leila, Silva, Alexandra, Smith, Graeme and de Vink, Erik (2024). On Formal Methods Thinking in Computer Science Education. Formal Aspects of Computing. doi: 10.1145/3670419
2023
Journal Article
Compositional reasoning for non-multicopy atomic architectures
Coughlin, Nicholas, Winter, Kirsten and Smith, Graeme (2023). Compositional reasoning for non-multicopy atomic architectures. Formal Aspects of Computing, 35 (2) 8, 1-30. doi: 10.1145/3574137
2023
Conference Publication
A Dafny-based approach to thread-local information flow analysis
Smith, Graeme (2023). A Dafny-based approach to thread-local information flow analysis. IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), Melbourne, VIC, Australia, 14-15 May 2023. Piscataway, NJ, United States: IEEE. doi: 10.1109/formalise58978.2023.00017
2022
Journal Article
Compositional noninterference on hardware weak memory models
Coughlin, Nicholas and Smith, Graeme (2022). Compositional noninterference on hardware weak memory models. Science of Computer Programming, 217 102779, 1-23. doi: 10.1016/j.scico.2022.102779
2022
Conference Publication
Declassification predicates for controlled information release
Smith, Graeme (2022). Declassification predicates for controlled information release. 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, 24-27 October 2022. Heidelberg, Germany: Springer. doi: 10.1007/978-3-031-17244-1_18
2021
Journal Article
Information-flow control on ARM and POWER multicore processors
Smith, Graeme, Coughlin, Nicholas and Murray, Toby (2021). Information-flow control on ARM and POWER multicore processors. Formal Methods in System Design, 58 (1-2), 251-293. doi: 10.1007/s10703-021-00376-2
2021
Conference Publication
Backwards-directed information flow analysis for concurrent programs
Winter, Kirsten, Coughlin, Nicholas and Smith, Graeme (2021). Backwards-directed information flow analysis for concurrent programs. Computer Security Foundations Symposium, Dubrovnik, Croatia, 21-25 June 2021. Piscataway, NJ, United States: IEEE. doi: 10.1109/csf51468.2021.00017
2021
Conference Publication
Rely/guarantee reasoning for multicopy atomic weak memory models
Coughlin, Nicholas, Winter, Kirsten and Smith, Graeme (2021). Rely/guarantee reasoning for multicopy atomic weak memory models. 24th International Symposium on Formal Methods (FM), Virtual, 20-26 November 2021. Cham, Switzerland: Springer Science and Business Media Deutschland. doi: 10.1007/978-3-030-90870-6_16
2020
Conference Publication
Rely/guarantee reasoning for noninterference in non-blocking algorithms
Coughlin, Nicholas and Smith, Graeme (2020). Rely/guarantee reasoning for noninterference in non-blocking algorithms. 33rd IEEE Computer Security Foundations Symposium (CSF), Boston, MA, United States, 22-26 June 2020. Piscataway, NJ, United States: IEEE. doi: 10.1109/csf49147.2020.00034
2020
Conference Publication
Specification with class: a brief history of object-Z
Smith, Graeme and Duke, David J. (2020). Specification with class: a brief history of object-Z. 23rd Symposium on Formal Methods, FM 2019, Porto, Portugal, 7-11 October 2019. Cham, Switzerland: Springer Cham. doi: 10.1007/978-3-030-54997-8_4
2020
Conference Publication
Weakening correctness and linearizability for concurrent objects on multicore processors
Smith, Graeme and Groves, Lindsay (2020). Weakening correctness and linearizability for concurrent objects on multicore processors. Formal Methods. FM 2019 International Workshops, Porto, Portugal, 7-11 October 2019. Heidelberg, Germany: Springer. doi: 10.1007/978-3-030-54997-8_22
2019
Journal Article
Modelling concurrent objects running on the TSO and ARMv8 memory models
Winter, Kirsten, Smith, Graeme and Derrick, John (2019). Modelling concurrent objects running on the TSO and ARMv8 memory models. Science of Computer Programming, 184 102308, 102308. doi: 10.1016/j.scico.2019.102308
Funding
Supervision
Availability
- Associate Professor Graeme Smith is:
- Available for supervision
Before you email them, read our advice on how to contact a supervisor.
Supervision history
Current supervision
-
Doctor Philosophy
Verified Secure Compilation for C-like Programs
Principal Advisor
Other advisors: Associate Professor Mark Utting
Completed supervision
-
2012
Master Philosophy
FORMAL PROPERTY PRESERVATION AND TRANSFORMATION IN SOFTWARE EVOLUTION
Principal Advisor
Other advisors: Emeritus Professor Ian Hayes
-
2007
Doctor Philosophy
Formal Derivation of Object-Oriented Designs
Principal Advisor
-
2007
Doctor Philosophy
A Behaviour-based methodology for fault tree generation.
Associate Advisor
-
2005
Doctor Philosophy
ANIMATION AND VISUALISATION OF REFINEMENTS
Associate Advisor
Media
Enquiries
Contact Associate Professor Graeme Smith directly for media enquiries about:
- Formal methods
- Mathematical modelling
- Multi-agent systems
- Self-adaptive systems
- Software-intensive systems
Need help?
For help with finding experts, story ideas and media enquiries, contact our Media team: