Associate Professor Graeme Smith

Associate Professor

School of Information Technology and Electrical Engineering
Faculty of Engineering, Architecture and Information Technology
smith@itee.uq.edu.au
+61 7 336 51625

Overview

Associate Professor Graeme Smith's research interests are in formal methods: mathematical notations for modelling software systems; automated tool-support for analysing such models; and development of software systems from such models.

He received his PhD from the University of Queensland in 1993. Since then he has worked at universities and research institutes in France, Australia and Germany. His past research has focused on the development of the object-oriented formal specification language Object-Z, and its integration with other formal specification languages and techniques to facilitate the modelling of concurrent and real-time systems. Currently he is investigating the use of formal methods for verifying lock-free algorithms running on modern multicore architectures.

Research Interests

  • Formal Methods
    Formal specification, verification and refinement, i.e., development from specification to code, of software systems. Primary expertise lies in the verification and refinement of concurrent programs, especially those running under hardware weak memory models such as x86-TSO (used by Intel and AMD processors), ARM (used by most mobile devices) and IBM POWER (used in IBM mainframes and supercomputers). Secondary expertise lies in the specification, verification and refinement 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. Emerging expertise is in the application of formal techniques, in particular information-flow logics, to security.

Qualifications

  • Doctor of Philosophy, The University of Queensland
  • Bachelor of Engineering (Honours1), The University of Queensland

Publications

View all Publications

Grants

View all Grants

Supervision

View all Supervision

Publications

Featured Publications

Book

  • Smith, Graeme (1999). Stepwise development from ideal specifications. SVRC Technical Report, 99-35. Software Verification Research Centre, School of Information Technology and Electrical Engineering, The University of Queensland.

  • Smith, Graeme and Hayes, Ian (1999). Towards real-time object-Z. Technical Report SSE, 99-10. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.

  • Smith, G. P. (1999). The Object-Z Specification Language. Boston: Kluwer Academic Publishers.

  • Duke, Roger, King, Paul, Rose, Gordon and Smith, Graeme (1991). The object-Z specification language: version 1. SVRC Technical Report, 91-1. Software Verification Research Centre, Department of Computer Science, The University of Queensland.

Book Chapter

  • 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.Berlin/Heidelberg: Springer International Publishing. doi:10.1007/978-3-319-48628-4

  • 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

  • Smith, G. (2008). Extending Formal Methods for Software-Intensive Systems. Software-Intensive Systems and New Computing Paradigms: Challenges and Visions. (pp. 146-161) edited by Wirsing, M., Banâtre, J.P., Hölzl, M. and Rauschmayer, A..Heidleberg Berlin: Springer. doi:10.1007/978-3-540-89437-7-10

  • Sanders, J.W. and Smith, G. (2008). Formal Ensemble Engineering. Software-Intensive Systems and New Computing Paradigms: Challenges and Visions. (pp. 132-138) edited by Wirsing, M., Banâtre, J.P., Hölzl, M. and Rauschmayer, A..Heidelberg, Germany: Springer. doi:10.1007/978-3-540-89437-7-8

  • Smith, G. P. (2001). State-Based Approaches: From Z to Object-Z. Formal Methods for Distributed Processing: A Survey of Object-Orientated Approaches. (pp. 105-125) edited by H. Bowman and J. Derrick.Cambridge, UK: Cambridge University Press.

Journal Article

Conference Publication

  • 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.

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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.

  • 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

  • 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

  • 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

  • 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

  • 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

  • Smith, Graeme, Sanders, J. W. and Li, Qin (2014). On directional bias for network coverage. Bio-Inspired Computing - Theories and Applications, Wuhan, China, 16-19 October 2014. Berlin & Heidelberg, Germany :Springer Berlin Heidelberg. doi: 10.1007/978-3-662-45049-9_62

  • Dongol, Brijesh, Derrick, John and Smith, Graeme (2014). Reasoning algebraically about refinement on TSO architectures. International Colloquium on Theoretical Aspects of Computing, Bucharest, Romania, 17-19 September 2014. Cham, Switzerland :Springer. doi: 10.1007/978-3-319-10882-7_10

  • 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

  • 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

  • Li, Qin and Smith, Graeme (2013). A refinement framework for autonomous agents. SBMF 2013: 16th Brazilian Symposium on Formal Methods, Brasilia, Brazil, 29 September-4 October, 2013. Heidelberg, Germany :Springer. doi: 10.1007/978-3-642-41071-0_12

  • Li, Qin and Smith, Graeme (2013). Using bounded fairness to specify and verify ordered asynchronous multi-agent systems. ICECCS 2013: 18th International Conference on Engineering of Complex Computer Systems, Mt Elizabeth, Singapore, 17-19 July, 2013. Piscataway, NJ, United States :IEEE Computer Society Conference Publishing Services (CPS). doi: 10.1109/ICECCS.2013.24

  • Sanders, J. W. and Smith, Graeme (2012). Emergence and refinement. Guildford, Surrey, U.K. :Springer. doi: 10.1007/s00165-011-0190-7

  • Smith, Graeme and Winter, Kirsten (2012). Incremental development of multi-agent systems in Object-Z. Software Engineering Workshop (SEW-35), Heraklion, Crete, Greece, 12-13 October 2012. Piscataway, NJ, United States :IEEE Computer Society Press. doi: 10.1109/SEW.2012.19

  • Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2012). Reasoning about adaptivity of agents and multi-agent systems. IEEE Intenational Conference on Engineering of Complex Computer Systems, Paris, France, 18-20 July 2012. Piscataway, NJ, United States :IEEE Computer Society. doi: 10.1109/ICECCS.2012.32

  • Smith, Graeme and Sanders, J. W. (2012). Using conventional reasoning techniques for self-organising systems. 2012 Tenth Annual International Conference on Privacy, Security and Trust, Paris, France, 16-18 July 2012. Piscataway, NJ, United States :IEEE. doi: 10.1109/PST.2012.6297952

  • Smith, Graeme and Helke, Steffen (2011). Refactoring object-oriented specifications with inheritance-based polymorphism. 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011, Xi'an, Shaanxi, China, 29-31 August 2011. Piscataway, NJ, United States :IEEE. doi: 10.1109/TASE.2011.31

  • Eder, Sebastian and Smith, Graeme (2010). An approach to formal verification of free-flight separation. Fourth IEEE International Conference on Self-Adaptive and Self-Organizing Systems 2010, Budapest, Hungary, 27-28 September 2010. Piscataway, NJ, United States :IEEE. doi: 10.1109/SASOW.2010.35

  • Sanders, J.W. and Smith, Graeme (2010). Assuring adaptive behaviour in self-organising systems. Workshop on Trustworthy Self-Organizing Systems, Budapest, Hungary, 27-28 September, 2010. Piscatawa, NJ, U.S.A. :IEEE - Computer Society. doi: 10.1109/SASOW.2010.36

  • Sampson, Aaron and Smith, Graeme (2010). Gravity points in potential-field approaches to self organisation. SASO 2010: Fourth IEEE International Conference on Self-Adaptive and Self-Organizing Systems, Budapest, Hungary, 27-28 September 2010. Piscataway, NJ, U.S.A. :Institute of Electrical and Electronic Engineers (IEEE). doi: 10.1109/SASOW.2010.24

  • Smith, Graeme and Sanders, J. W. (2009). Formal development of self-organising systems. 6th International Conference on Autonomic and Trusted Computing (ATC 2009), Brisbane, Australia, 7 - 9 July 2009. Heidelberg, Germany :Springer. doi: 10.1007/978-3-642-02704-8_8

  • Sanders, J. W. and Smith, Graeme (2009). Refining emergent properties. International Refinement Workshop (Refine 2009), Eindhoven, The Netherlands, 3 November 2009. Amsterdam , The Netherlands :Elsevier.

  • McComb, T. and Smith, G (2008). A Minimal Set of Refactoring Rules for Object-Z. International Symposium on Formal Methods (FM 2008), Oslo, Norway, 4-6 June, 2008. Heidelberg, Germany :Springer. doi: 10.1007/978-3-540-68863-1_11

  • McComb, T. and Smith, G (2008). Introducing objects through refinement. International Symposium on Formal Methods (FM 2008), Turku, Finland, 26-30 May, 2008. Heidelberg, Germany :Springer. doi: 10.1007/978-3-540-68237-0_25

  • Smith, Greame and McComb, Tim (2008). Refactoring real-time specifications. International Refinement Workshop (Refine 2008), Turku, Finland, 27 May, 2008. Amsterdam, The Netherlands :Elsevier. doi: 10.1016/j.entcs.2008.06.016

  • Fu, Z. and Smith, G. (2008). Towards more flexible development of Z specifications. 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering 2008 (TASE '08), Nanjing, China, 17-19 June 2008. Piscataway, NJ, U.S.A. :IEEE - Institute of Electrical Electronics Engineers Inc.. doi: 10.1109/TASE.2008.20

  • Derrick, J. and Smith, G. (2008). Using Model Checking to Automatically Find Retrieve Relations. International Refinement Workshop (Refine 2007), Oxford, UK, 2 July, 2007. Amsterdam, The Netherlands :Elseiver. doi: 10.1016/j.entcs.2008.02.019

  • Meinicke, L. and Smith, G. (2007). A stepwise development process for reasoning about the reliability of real-time systems. 6th International Conference: IFM 2007 - Integrated Formal Methods, Oxford, U.K., 2-5 July 2007. Berlin, Germany :Springer-Verlag. doi: 10.1007/978-3-540-73210-5_23

  • Smith, G. and Winter, K. (2007). Simulation machines for checking action system refinements. 11th Refinement Workshop (REFINE 2006), Macao, China, 31 October 2006. USA :Elseiver BV. doi: 10.1016/j.entcs.2006.08.045

  • McComb, Tim and Smith, Graeme (2006). Compositional class refinement in object-Z. FM 2006: Formal Methods, Hamilton, Canada, 21-27 August 2006. Berlin, Germany :Springer. doi: 10.1007/11813040

  • Smith, Graeme and Derrick, John (2006). Verifying data refinements using a model checker. Surrey, United Kingdom :Springer U. K.. doi: 10.1007/s00165-006-0002-7

  • Smith, Graeme and Wildman, Luke (2005). Model checking Z specifications using SAL. 4th Informational Conference of B and Z Users, Guildford, UK, 13-15 April 2005. Berlin, Germany :Springer. doi: 10.1007/11415787_6

  • Smith, G. P. and Derrick, J. (2005). Model checking downward simulations. REFINE 2005, Guildford, UK, 12 April, 2005. Amsterdam, The Netherlands :Elsevier. doi: 10.1016/j.entcs.2005.04.032

  • Smith, G. P. (2004). A formal framework for modelling and analysing mobile systems. The Twenty-Seventh Australasian Computer Science Conference (ACSC'04), Dunedin, New Zealand, 18-22 January, 2004. Sydney :Australian Computer Society. doi: 10.1145/980000/979946/p193-smith.pdf?key1=979946

  • McComb, T. J. and Smith, G. P. (2004). Architectural design in object-z. The 2004 Australian Software Engineering Conference (ASWEC 2004), Melbourne, Australia, 13-16 April 2004. Los Alamitos, California, U.S.A. :IEEE Computer Society. doi: 10.1109/ASWEC.2004.1290460

  • Smith, G. P. and Derrick, J. (2004). Linear temporal logic and z refinement. The Tenth International Conference on Algebraic Methodology and Software Technology, Stirling, Scotland, 12th - 16th July, 2004. Berlin :Springer-Verlag. doi: 10.1007/b98770

  • McComb, T. J. and Smith, G. P. (2003). Animation of object-z specifications using a Z animator. The First International Conference on Software Engineering and Formal Methods, Brisbane, Australia, 25-26 September 2003. Los Alamitos, CA, U.S.A. :IEEE Computer Society. doi: 10.1109/SEFM.2003.1236221

  • Winter, Kirsten and Smith, Graeme P. (2003). Compositional verification for object-Z. The 3rd International Conference on B and Z Users, Turku, Finland, 4-6 June, 2003. Berlin :Springer-Verlag. doi: 10.1007/3-540-44880-2_18

  • Smith, Graeme and Winter, Kirsten (2003). Proving Temporal Properties of Z Specifications Using Abstraction. ZB 2003: Formal Specification and Development in Z and B : Third International Conference of B and Z Users, Turku, Finland, 4–6 June 2003. Heidelberg Germany :Springer - Verlag. doi: 10.1007/3-540-44880-2_17

  • Smith, G. P. and Derrick, J. (2002). Abstract specification in Object-Z and CSP. 4th International Conference on Formal Engineering Methods, ICFEM 2002, Shanghai, China, 21-25 October, 2002. Heidelberg :Springer-Verlag.

  • Smith, G. P. (2002). An integration of real-time object-Z and CSP for specifying concurrent real-time systems. IFM 2002, Turku, Finland, 15-18 May, 2002. Berlin :Springer-Verlag. doi: 10.1007/3-540-47884-1_15

  • Smith, G. P. and Hayes, I. J. (2002). An introduction to real-time Object-Z. London :Springer-Verlag. doi: 10.1007/s001650200003

  • Smith, G. P., Kammuller, F. and Santen, T. (2002). Encoding Object-Z in Isabelle/HOL. ZB 2002: Formal Specification and Development in Z and B, Grenoble, France, 23-25 January, 2002. Heidelberg :Springer-Verlag.

  • Smith, G. P. (2002). Introducing reference semantics via refinement. 4th International Conference on Formal Engineering Methods, ICFEM 2002, Shanghai, China, 21-25 October, 2002. Heidelberg :Springer-Verlag. doi: 10.1007/3-540-36103-0_60

  • Smith, G.P. (2002). Specifying mode requirements of embedded systems. 25th Australasian Computer Science Conference (ACSC 2002), Monash University, Melbourne, Victoria, 28 January-1 February, 2002. Australian Computer Society.

  • Kassel, Geoff and Smith, Graeme (2001). Model checking object-Z classes: Some experiments with FDR.

  • Smith, G. P. (2001). Introducing parallel composition to the timed refinement calculus. PART 2000, Sydney, 29-30 November 2000. Hong Kong :Springer Verlag.

  • Smith, G. P. (2000). Recursive schema definitions in Object-Z. International Conference of B and Z Users (ZB 2000), York, UK, 29 August - 2 September 2000. Berlin :Springer Verlag.

  • Lindsay, P. A. and Smith, G. P. (2000). Safety assurance of Commercial-Off-The-Shelf software. 5th Australian Workshop on Safety Critical Systems & Software, Melbourne, Australia, 24 November, 2000. Melbourne, Australia :Australian Computer Society.

  • Smith, Graeme (2000). Stepwise development from ideal specifications. ACSC 2000, Canberra, 31 January - 3 February 2000. Los Alamitos, California, USA :IEEE Computer Society. doi: 10.1109/ACSC.2000.824408

  • Derrick, J. and Smith, G. P. (2000). Structural refinement in Object-Z / CSP. Integrated Formal Methods: Second International Conference, IFM 2000, Schloss Dagstuhl, Germany, 1-3 November, 2000. Berlin :Springer Verlag.

  • Smith, G and Hayes, I (2000). Structuring real-time Object-Z specifications. Integrated Formal Methods: Second International Conference, IFM 2000,, Dagstuhl Castle, Germany, November 2000. Berlin, Germany :Springer. doi: 10.1007/3-540-40911-4_7

  • Smith, G. P. (1999). From ideal to realisable real-time specifications. New Zealand Formal Program Development Colloquium, Auckland, NZ, 22 Jan, 1999. NZ :Inst Information & Mathematical Sciences, Massey Uni, NZ.

  • Smith, G. P. (1999). Specification and refinement of a real-time control system. 22nd Australasian Computer Science Conference, Auckland, NZ, 18-21 Jan, 1999. Auckland, NZ :Springer Verlag.

  • Smith, G. P. and Hayes, I. J. (1999). Towards real-time Object-Z. Integrated Formal Methods IFM'99, York, UK, 28-29 June 1999. London :Springer-Verlag. doi: 10.1007/978-1-4471-0851-1_4

  • Smith, Graeme and Derrick, John (1997). Refinement and verification of concurrent systems specified in Object-Z and CSP. Proceedings of the 1997 1st International Conference on Formal Engineering Methods, ICFEM, , , November 12, 1997-November 14, 1997. IEEE Comp Soc.

  • Smith, Graeme (1997). A semantic integration of object-Z and CSP for the specification of concurrent systems. 4th International Symposium of Formal Methods Europe, FME 1997, Graz, , September 15, 1997-September 19, 1997. Springer Verlag. doi: 10.1007/3-540-63533-5_4

  • Smith, Graeme (1995). Extending W for object-Z. 9th International Conference of Z Users Meeting, ZUM 1995, Limerick, , September 7, 1995-September 9, 1995. Springer Verlag.

  • Smith, G. (1994). Formal definitions of behavioural compatibility for active and passive objects. 1st Asia-Pacific Software Engineering Conference, APSEC 1994, Tokyo, Japan, 7 - 9 December 1994. Piscataway, NJ United States :IEEE Computer Society. doi: 10.1109/APSEC.1994.465246

Edited Outputs

Other Outputs

PhD and MPhil Supervision

Completed Supervision

  • (2012) Master Philosophy — Principal Advisor

    Other advisors:

  • (2007) Doctor Philosophy — Principal Advisor

  • (2007) Doctor Philosophy — Associate Advisor

  • (2005) Doctor Philosophy — Associate Advisor