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
2019
Edited Outputs
Formal methods teaching: Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings
Brijesh Dongol, Luigia Petre and Graeme Smith eds. (2019). Formal methods teaching: Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings. Formal Methods Teaching: Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, 7 October 2019. Cham, Switzerland: Springer International Publishing.
2019
Conference Publication
Preface
Dongol, Brijesh, Petre, Luigia and Smith, Graeme (2019). Preface. Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, Porto, Portugal, 7 October 2019. Cham, Switzerland: Springer.
2018
Conference Publication
Correctness of concurrent objects under weak memory models
Smith, Graeme, Winter, Kirsten and Colvin, Robert J. (2018). Correctness of concurrent objects under weak memory models. 18th Refinement Workshop, Refine 2018, Oxford, United Kingdom, 18 July 2018. SYDNEY: Open Publishing Association. doi: 10.4204/EPTCS.282.5
2018
Conference Publication
Observational models for linearizability checking on weak memory models
Winter, Kirsten, Smith, Graeme and Derrick, John (2018). Observational models for linearizability checking on weak memory models. International Symposium on Theoretical Aspects of Software Engineering (TASE), Guangzhou, China, 29-31 August 2018. Piscataway, NJ United States: IEEE. doi: 10.1109/TASE.2018.00021
2017
Conference Publication
An observational approach to defining linearizability on weak memory models
Derrick, John and Smith, Graeme (2017). An observational approach to defining linearizability on weak memory models. Formal Techniques for Distributed Objects, Components, and Systems, Neuchâtel, Switzerland, 19–22 June 2017. Heidelberg, Germany: Springer . doi: 10.1007/978-3-319-60225-7_8
2017
Conference Publication
Improving the Scalability of Automatic Linearizability Checking in SPIN
Doolan, Patrick, Smith, Graeme, Zhang, Chenyi and Krishnan, Padmanabhan (2017). Improving the Scalability of Automatic Linearizability Checking in SPIN. 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an,, November 13, 2017-November 17, 2017. Cham, Switzerland: Springer Verlag. doi: 10.1007/978-3-319-68690-5_7
2017
Book Chapter
A proof method for linearizability on TSO architectures
Derrick, John, Smith, Graeme, Groves, Lindsay and Dongol, Brijesh (2017). A proof method for linearizability on TSO architectures. Provably correct systems. (pp. 61-91) edited by Mike Hinchey, Jonathan P. Bowen and Ernst-Rüdiger Olderog. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-319-48628-4
2016
Journal Article
Refining autonomous agents with declarative beliefs and desires
Li, Qin and Smith, Graeme (2016). Refining autonomous agents with declarative beliefs and desires. Formal Aspects of Computing, 29 (2), 1-23. doi: 10.1007/s00165-016-0391-1
2016
Conference Publication
Model checking simulation rules for linearizability
Smith, Graeme (2016). Model checking simulation rules for linearizability. 14th International Conference on Software Engineering and Formal Methods, SEFM 2016, Vienna, Austria, 4-8 July 2016. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-41591-8_13
2016
Conference Publication
Invariant generation for linearizability proofs
Smith, Graeme and Derrick, John (2016). Invariant generation for linearizability proofs. 31st Annual ACM Symposium on Applied Computing, SAC 2016, Pisa, Italy, 4 - 8 April 2016. New York, NY, United States: Association for Computing Machinery. doi: 10.1145/2851613.2851837
2015
Conference Publication
A framework for correctness criteria on weak memory models
Derrick, John and Smith, Graeme (2015). A framework for correctness criteria on weak memory models. 20th International Symposium on Formal Methods, FM 2015, Oslo, Norway, 25-26 June 2015. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-19249-9_12
2015
Conference Publication
A macro-level model for investigating the effect of directional bias on network coverage
Smith, Graeme, Sanders, J. W. and Li, Qin (2015). A macro-level model for investigating the effect of directional bias on network coverage. 38th Australasian Computer Science Conference (ACSC 2015), Sydney, Australia, 27-30 January 2015. Sydney, Australia: Australian Computer Society.
2015
Conference Publication
Admit your weakness: Verifying correctness on TSO architectures
Smith, Graeme, Derrick, John and Dongol, Brijesh (2015). Admit your weakness: Verifying correctness on TSO architectures. 11th International Symposium on Formal Aspects of Component Software, FACS 2014, Bertinoro, Italy, 10 - 12 September 2014. Heidelberg, Germany: Springer Verlag. doi: 10.1007/978-3-319-15317-9_22
2015
Conference Publication
Defining correctness conditions for concurrent objects in multicore architectures
Dongol, Brijesh, Derrick, John, Groves, Lindsay and Smith, Graeme (2015). Defining correctness conditions for concurrent objects in multicore architectures. 29th European Conference on Object-Oriented Programming, ECOOP 2015, Prague, Czech Republic, 5-10 July 2015. Wadern, Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. doi: 10.4230/LIPIcs.ECOOP.2015.470
2015
Conference Publication
Using Z in the development and maintenance of computational models of real-world systems
Moeiniyan Bagheri, Shahrzad, Smith, Graeme and Hanan, Jim (2015). Using Z in the development and maintenance of computational models of real-world systems. 12th International Conference on Software Engineering and Formal Methods, Grenoble, France, 1 - 2 September 2014. Heidelberg, Germany: Springer Verlag. doi: 10.1007/978-3-319-15201-1_3
2014
Book Chapter
Designing adaptive systems using teleo-reactive agents
Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2014). Designing adaptive systems using teleo-reactive agents. Transactions on Computational Collective Intelligence XVI. (pp. 34-61) edited by Ryszard Kowalczyk and Ngoc Thanh Nguyen. Heidelberg, Germany: Springer. doi: 10.1007/978-3-662-44871-7_2
2014
Conference Publication
A formal development approach for self-organising systems
Li, Q. and Smith, G. (2014). A formal development approach for self-organising systems. 8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014, Changsha, Hunan, China, 1-3 September 2014. Los Alamitos, CA United States: IEEE Computer Society. doi: 10.1109/TASE.2014.11
2014
Conference Publication
MAZE: An extension of object-Z for multi-agent systems
Smith, Graeme and Li, Qin (2014). MAZE: An extension of object-Z for multi-agent systems. 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014, Toulouse, France, June 2, 2014-June 6, 2014. Heidelberg, Germany: Springer. doi: 10.1007/978-3-662-43652-3_6
2014
Conference Publication
Verifying linearizability on TSO architectures
Derrick, John, Smith, Graeme and Dongol, Brijesh (2014). Verifying linearizability on TSO architectures. 11th International Conference on Integrated Formal Methods, IFM 2014, Bertinoro, Italy, 9 - 11 September 2014. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-10181-1_21
2014
Conference Publication
Using coarse-grained abstractions to verify linearizability on TSO architectures
Derrick, John, Smith, Graeme, Groves, Lindsay and Dongol, Brijesh (2014). Using coarse-grained abstractions to verify linearizability on TSO architectures. 10th International Haifa Verification Conference (HVC), Haifa, Israel, 18 - 20 November 2014. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-13338-6_1
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: