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

Qualifications

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

Publications

View all Publications

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. The Object-Z Specification Language. Boston: Kluwer Academic Publishers, 1999.

  • 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

  • Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2014). Designing adaptive systems using teleo-reactive agents. In Ryszard Kowalczyk and Ngoc Thanh Nguyen (Ed.), Transactions on Computational Collective Intelligence XVI (pp. 34-61) Heidelberg, Germany: Springer. doi:10.1007/978-3-662-44871-7_2

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

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

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

Journal Article

Conference Publication

  • Smith, Graeme and Derrick, John (2016). Invariant generation for linearizability proofs. In: Proceedings of the ACM Symposium on Applied Computing. 31st Annual ACM Symposium on Applied Computing, SAC 2016, Pisa, Italy, (1694-1699). 4 - 8 April 2016. doi:10.1145/2851613.2851837

  • Smith, Graeme (2016). Model checking simulation rules for linearizability. In: Rocco De Nicola and Eva Kühn, Software Engineering and Formal Methods - 14th International Conference, SEFM 2016 Held as Part of STAF 2016, Proceedings. 14th International Conference on Software Engineering and Formal Methods, SEFM 2016, Vienna, Austria, (188-203). 4-8 July 2016. doi:10.1007/978-3-319-41591-8_13

  • Derrick, John and Smith, Graeme (2015). A framework for correctness criteria on weak memory models. In: Nikolaj Bjørner and Frank de Boer, FM 2015: Formal Methods. 20th International Symposium on Formal Methods, FM 2015, Oslo, Norway, (178-194). 25-26 June 2015. 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. In: David Parry, Proceedings of the 38th Australasian Computer Science Conference (ACSC 2015). 38th Australasian Computer Science Conference (ACSC 2015), Sydney, Australia, (73-81). 27-30 January 2015.

  • Smith, Graeme, Derrick, John and Dongol, Brijesh (2015). Admit your weakness: Verifying correctness on TSO architectures. In: Ivan Lanese and Eric Madelaine, Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Revised Selected Papers. 11th International Symposium on Formal Aspects of Component Software, FACS 2014, Bertinoro, Italy, (364-383). 10 - 12 September 2014. 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. In: John Tang Boyland, 29th European Conference on Object-Oriented Programming, ECOOP 2015. 29th European Conference on Object-Oriented Programming, ECOOP 2015, Prague, Czech Republic, (470-494). 5-10 July 2015. 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. In: Carlos Canal and Akram Idani, Software Engineering and Formal Methods: SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Revised Selected Papers. 12th International Conference on Software Engineering and Formal Methods, Grenoble, France, (36-53). 1 - 2 September 2014. doi:10.1007/978-3-319-15201-1_3

  • Li, Q. and Smith, G. (2014). A formal development approach for self-organising systems. In: Theoretical Aspects of Software Engineering Conference (TASE), 2014. 8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014, Changsha, Hunan, China, (209-212). 1-3 September 2014. doi:10.1109/TASE.2014.11

  • Smith, Graeme and Li, Qin (2014). MAZE: An extension of object-Z for multi-agent systems. In: Yamine Ait Ameur and Klaus-Dieter Schewe, Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings. 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014, Toulouse, France, (72-85). June 2, 2014-June 6, 2014. doi:10.1007/978-3-662-43652-3_6

  • Smith, Graeme, Sanders, J. W. and Li, Qin (2014). On directional bias for network coverage. In: Linqiang Pan, Gheorghe Păun, Mario J. Pérez-Jiménez and Tao Song, Bio-Inspired Computing - Theories and Applications, Bic-Ta 2014. Bio-Inspired Computing - Theories and Applications, Wuhan, China, (384-388). 16-19 October 2014. doi:10.1007/978-3-662-45049-9_62

  • Dongol, Brijesh, Derrick, John and Smith, Graeme (2014). Reasoning algebraically about refinement on TSO architectures. In: Gabriel Ciobanu and Dominique Méry, Theoretical Aspects of Computing – ICTAC 2014. International Colloquium on Theoretical Aspects of Computing, Bucharest, Romania, (151-168). 17-19 September 2014. 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. In: Eran Yahav, Hardware and Software: Verification and Testing. 10th International Haifa Verification Conference (HVC), Haifa, Israel, (1-16). 18 - 20 November 2014. doi:10.1007/978-3-319-13338-6_1

  • Derrick, John, Smith, Graeme and Dongol, Brijesh (2014). Verifying linearizability on TSO architectures. In: Elvira Albert and Emil Sekerinski, Integrated Formal Methods - 11th International Conference, IFM 2014, Proceedings. 11th International Conference on Integrated Formal Methods, IFM 2014, Bertinoro, Italy, (341-356). 9 - 11 September 2014. doi:10.1007/978-3-319-10181-1_21

  • Li, Qin and Smith, Graeme (2013). A refinement framework for autonomous agents. In: Juliano Iyoda and Leonardo de Moura, Formal Methods: Foundations and Applications. 16th Brazilian Symposium: Proceedings. SBMF 2013: 16th Brazilian Symposium on Formal Methods, Brasilia, Brazil, (163-178). 29 September-4 October, 2013. 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. In: Proceedings: 2013 International Conference on Engineering of Complex Computer Systems, ICECCS 2013. ICECCS 2013: 18th International Conference on Engineering of Complex Computer Systems, Mt Elizabeth, Singapore, (111-120). 17-19 July, 2013. doi:10.1109/ICECCS.2013.24

  • Smith, Graeme and Winter, Kirsten (2012). Incremental development of multi-agent systems in Object-Z. In: 35th Annual IEEE Software Engineeering Workshop (SEW-35): Proceedings. Software Engineering Workshop (SEW-35), Heraklion, Crete, Greece, (120-129). 12-13 October 2012. doi:10.1109/SEW.2012.19

  • Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2012). Reasoning about adaptivity of agents and multi-agent systems. In: CESAMES, Seventeenth IEEE International Conference on Engineering of Complex Computer Systems. IEEE Intenational Conference on Engineering of Complex Computer Systems, Paris, France, (341-350). 18-20 July 2012. doi:10.1109/ICECCS.2012.32

  • Smith, Graeme and Sanders, J. W. (2012). Using conventional reasoning techniques for self-organising systems. In: Nora Cuppens-Boulahia, Philip Fong, Joaquin Garcia-Alfaro, Stephen Marsh and Jan-Philipp Steghöfer, Tenth Annual International Conference on Privacy, Security and Trust proceedings. 2012 Tenth Annual International Conference on Privacy, Security and Trust, Paris, France, (238-243). 16-18 July 2012. doi:10.1109/PST.2012.6297952

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

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

  • Sanders, J.W. and Smith, Graeme (2010). Assuring adaptive behaviour in self-organising systems. In: Fourth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshop (SASOW), 2010. Workshop on Trustworthy Self-Organizing Systems, Budapest, Hungary, (172-177). 27-28 September, 2010. doi:10.1109/SASOW.2010.36

  • Sampson, Aaron and Smith, Graeme (2010). Gravity points in potential-field approaches to self organisation. In: Proceedings 2010 Fourth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshop: SASOW 2010. SASO 2010: Fourth IEEE International Conference on Self-Adaptive and Self-Organizing Systems, Budapest, Hungary, (110-115). 27-28 September 2010. doi:10.1109/SASOW.2010.24

  • Smith, Graeme and Sanders, J. W. (2009). Formal development of self-organising systems. In: Juan Gonzalez Nieto, Wolfgang Reif, Guojun Wang and Jadwiga Indulska, Autonomic and Trusted Computing. 6th International Conference on Autonomic and Trusted Computing (ATC 2009), Brisbane, Australia, (90-104). 7 - 9 July 2009.

  • Sanders, J. W. and Smith, Graeme (2009). Refining emergent properties. In: Eerke Boiten, John Derrick and Steve Reeves, Proceedings of the 14th BAC-FACS International Refinement Workshop (Refine 2009). International Refinement Workshop (Refine 2009), Eindhoven, The Netherlands, (207-233). 3 November 2009.

  • McComb, T. and Smith, G (2008). A Minimal Set of Refactoring Rules for Object-Z. In: Barthe, G. and de Boer, F.S., Formal Methods for Open Object-based Distributed Systems. International Symposium on Formal Methods (FM 2008), Oslo, Norway, (170-184). 4-6 June, 2008.

  • McComb, T. and Smith, G (2008). Introducing objects through refinement. In: Cuellar, J., Maibaum, T. and Sere, K., FM 2008: Formal Methods. International Symposium on Formal Methods (FM 2008), Turku, Finland, (358-373). 26-30 May, 2008.

  • Smith, Greame and McComb, Tim (2008). Refactoring real-time specifications. In: J. Derrick, E. Boiten and G. Schellhorn, Proceedings of the 13th BAC-FACS Refinement Workshop (Refine 2008). International Refinement Workshop (Refine 2008), Turku, Finland, (359-380). 27 May, 2008. doi:10.1016/j.entcs.2008.06.016

  • Fu, Z. and Smith, G. (2008). Towards more flexible development of Z specifications. In: J. Davies and X. Li, Theoretical Aspects of Software Engineering 2008 (TASE '08). 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering 2008 (TASE '08), Nanjing, China, (281-288). 17-19 June 2008. doi:10.1109/TASE.2008.20

  • Derrick, J. and Smith, G. (2008). Using Model Checking to Automatically Find Retrieve Relations. In: Derrick, J., Boiten, E. and Smith, G, Proceedings of the BAC-FACS Refinement Workshop (Refine 2007). International Refinement Workshop (Refine 2007), Oxford, UK, (155-175). 2 July, 2007. 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. In: J. Davies and J. Gibbons, Integrated Formal Methods 2007. 6th International Conference: IFM 2007 - Integrated Formal Methods, Oxford, U.K., (439-458). 2-5 July 2007. doi:10.1007/978-3-540-73210-5_23

  • Smith, G. and Winter, K. (2007). Simulation machines for checking action system refinements. In: Aichernig, B., Boiten, E., Derrick, J. and Groves, L., Proceedings of the 11th Refinement Workshop (REFINE 2006). 11th Refinement Workshop (REFINE 2006), Macao, China, (75-90). 31 October 2006. doi:10.1016/j.entcs.2006.08.045

  • McComb, Tim and Smith, Graeme (2006). Compositional class refinement in object-Z. In: J. Mishra, T. Nipkow and E. Sekerinski, FProceedings of 14th International Symposium on Formal Methods. FM 2006: Formal Methods, Hamilton, Canada, (205-220). 21-27 August 2006. doi:10.1007/11813040

  • Smith, Graeme and Wildman, Luke (2005). Model checking Z specifications using SAL. In: H. Treharne, S. King, M. Henson and S. Schneider, ZB 2005: Formal Specification and Development in Z and B. 4th Informational Conference of B and Z Users, Guildford, UK, (85-103). 13-15 April 2005. doi:10.1007/11415787_6

  • Smith, G. P. and Derrick, J. (2005). Model checking downward simulations. In: J. Derrick and E. Boiten, Proceedings of the REFINE 2005 Workshop. REFINE 2005, Guildford, UK, (205-224). 12 April, 2005. doi:10.1016/j.entcs.2005.04.032

  • Smith, G. P. (2004). A formal framework for modelling and analysing mobile systems. In: V. Estivill-Castro, Proceedings of the Twenty-Seventh Australasian Computer Science Conference (ACSC'04). The Twenty-Seventh Australasian Computer Science Conference (ACSC'04), Dunedin, New Zealand, (193-202). 18-22 January, 2004. doi:10.1145/980000/979946/p193-smith.pdf?key1=979946

  • McComb, T. J. and Smith, G. P. (2004). Architectural design in object-z. In: P. Strooper, Proceedings of the 2004 Australian Software Engineering Conference (ASWEC 2004). The 2004 Australian Software Engineering Conference (ASWEC 2004), Melbourne, Australia, (77-86). 13-16 April 2004. doi:10.1109/ASWEC.2004.1290460

  • Smith, G. P. and Derrick, J. (2004). Linear temporal logic and z refinement. In: C. Rattray, S. Maharaj and C. Shankland, Lecture Notes in Computer Science: Algebraic Methodology and Software Technology. The Tenth International Conference on Algebraic Methodology and Software Technology, Stirling, Scotland, (117-131). 12th - 16th July, 2004. doi:10.1007/b98770

  • McComb, T. J. and Smith, G. P. (2003). Animation of object-z specifications using a Z animator. In: A. Cerone and P. Lindsay, Proceedings of the First International Conference on Software Engineering and Formal Methods. The First International Conference on Software Engineering and Formal Methods, Brisbane, Australia, (191-200). 25-26 September 2003. doi:10.1109/SEFM.2003.1236221

  • Winter, Kirsten and Smith, Graeme P. (2003). Compositional verification for object-Z. In: D. Bert, J. Bowen, S. King and M. Walden, Lecture Notes in Computer Science: Proceedings of the 3rd International Conference on B and Z Users. The 3rd International Conference on B and Z Users, Turku, Finland, (280-299). 4-6 June, 2003. doi:10.1007/3-540-44880-2_18

  • Smith, Graeme and Winter, Kirsten (2003). Proving Temporal Properties of Z Specifications Using Abstraction. In: D. Bert, J. P. Bowen, S. King and M. Waldén, ZB 2003: Formal Specification and Development in Z and B: Third International Conference of B and Z Users Turku, Finland, June 4–6, 2003 Proceedings. ZB 2003: Formal Specification and Development in Z and B : Third International Conference of B and Z Users, Turku, Finland, (260-279). 4–6 June 2003. doi:10.1007/3-540-44880-2_17

  • Smith, G. P. and Derrick, J. (2002). Abstract specification in Object-Z and CSP. In: C. George and H. Miao, Formal Methods And Software Engineering, Proceedings. 4th International Conference on Formal Engineering Methods, ICFEM 2002, Shanghai, China, (108-119). 21-25 October, 2002.

  • Smith, G. P. (2002). An integration of real-time object-Z and CSP for specifying concurrent real-time systems. In: M. Butler, L. Petre and K. Sere, Integrated Formal Methods Third International Conference, IFM 2002. IFM 2002, Turku, Finland, (267-285). 15-18 May, 2002.

  • Smith, G. P., Kammuller, F. and Santen, T. (2002). Encoding Object-Z in Isabelle/HOL. In: D. Bert, J. P. Bowen, M. C. Henson and K. Robinson, 2nd International Conference of B and Z Users. ZB 2002: Formal Specification and Development in Z and B, Grenoble, France, (82-99). 23-25 January, 2002.

  • Smith, G. P. (2002). Introducing reference semantics via refinement. In: C. George and H. Miao, Lecture Notes in Computer Science: Formal Methods and Software Engineering. 4th International Conference on Formal Engineering Methods, ICFEM 2002, Shanghai, China, (588-599). 21-25 October, 2002. doi:10.1007/3-540-36103-0_60

  • Smith, G.P. (2002). Specifying mode requirements of embedded systems. In: M. Oudshoorn, proceedings of 25th Australasian Computer Science Conference (ACSC 2002). 25th Australasian Computer Science Conference (ACSC 2002), Monash University, Melbourne, Victoria, (251-258). 28 January-1 February, 2002.

  • Smith, G. P. (2001). Introducing parallel composition to the timed refinement calculus. In: H. ElGindy and C. Fidge, Proceedings of the 7th Australiasian Conference on Parallel and Real-Time Systems. PART 2000, Sydney, (139-148). 29-30 November 2000.

  • Smith, G. P. (2000). Recursive schema definitions in Object-Z. In: J. P. owen, S. Dunne, A. Galloway and S. King, Lecture notes in computer science: ZB 2000 - Formal Specification and Development in Z and B. International Conference of B and Z Users (ZB 2000), York, UK, (42-58). 29 August - 2 September 2000.

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

  • Smith, Graeme (2000). Stepwise development from ideal specifications. In: J. Edwards, Proceedings of IEEE: 23rd Australasian Computer Science Conference (ACSC 2000). ACSC 2000, Canberra, (227-233). 31 January - 3 February 2000. doi:10.1109/ACSC.2000.824408

  • Derrick, J. and Smith, G. P. (2000). Structural refinement in Object-Z / CSP. In: W. Grieskamp, T. Santen and B. Stoddart, Lecture notes in computer science: Integrated Formal Methods. Integrated Formal Methods: Second International Conference, IFM 2000, Schloss Dagstuhl, Germany, (194-213). 1-3 November, 2000.

  • Smith, G. P. and Hayes, I. J. (2000). Structuring real-time Object-Z specifications. In: W. Grieskamp, T. Santen and B. Stoddart, Lecture notes in computer science: Integrated Formal Methods. Integrated Formal Methods: Second International Conference, IFM 2000, Schloss Dagstuhl, Germany, (97-115). 1-3 November, 2000.

  • Smith, G and Hayes, I (2000). Structuring real-time Object-Z specifications. In: Lecture Notes in Computer Science 1945. Integrated Formal Methods: Second International Conference, IFM 2000,, Dagstuhl Castle, Germany, (97-115). November 2000.

  • Smith, G. P. (1999). From ideal to realisable real-time specifications. In: N. Leslie, IIMS Technical Report: Fifth New Zealand Formal Program Development Colloquium. New Zealand Formal Program Development Colloquium, Auckland, NZ, (7-7). 22 Jan, 1999.

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

  • Smith, G. P. and Hayes, I. J. (1999). Towards real-time Object-Z. In: K. Araki, A. Galloway and K. Taguchi, Proceedings of the 1st International Conference on Integrated Formal Methods. Integrated Formal Methods IFM'99, York, UK, (49-65). 28-29 June, 1999.

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