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

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.

Qualifications

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

Publications

  • 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

  • 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 and Winter, Kirsten (2017). Relating trace refinement and linearizability. Formal Aspects of Computing, 29 (6), 1-16. doi: 10.1007/s00165-017-0418-2

  • 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

  • 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

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

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

  • 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. doi: 10.1007/3-540-45648-1_5

  • 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. doi: 10.1007/3-540-40911-4_12

  • 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

Grants (Administered at UQ)

PhD and MPhil Supervision

Current Supervision

  • Doctor Philosophy — Principal Advisor

Completed Supervision