OR

Browse By

Associate Professor Graeme Smith

Associate Professor

School of Electrical Engineering and Computer Science
Faculty of Engineering, Architecture and Information Technology
smith@eecs.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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

View all Publications

Grants

View all Grants

Supervision

View all Supervision

Publications

Featured Publications

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

Book

  • Stepwise development from ideal specifications

    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.

  • Towards real-time object-Z

    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.

  • 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

  • The object-Z specification language: version 1

    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

  • 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

  • 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

  • Extending Formal Methods for Software-Intensive Systems

    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

  • Formal Ensemble Engineering

    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

  • State-Based Approaches: From Z to Object-Z

    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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

  • 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

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

  • 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

  • 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

  • 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

  • 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

  • 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

  • On directional bias for network coverage

    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

  • Reasoning algebraically about refinement on TSO architectures

    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

  • 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

  • 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

  • A refinement framework for autonomous agents

    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

  • Using bounded fairness to specify and verify ordered asynchronous multi-agent systems

    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

  • Incremental development of multi-agent systems in Object-Z

    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

  • Reasoning about adaptivity of agents and multi-agent systems

    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

  • Using conventional reasoning techniques for self-organising systems

    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

  • Refactoring object-oriented specifications with inheritance-based polymorphism

    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

  • An approach to formal verification of free-flight separation

    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

  • Assuring adaptive behaviour in self-organising systems

    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

  • Gravity points in potential-field approaches to self organisation

    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

  • Formal development of self-organising systems

    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

  • Refining emergent properties

    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.

  • A Minimal Set of Refactoring Rules for Object-Z

    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

  • Formal ensemble engineering

    Sanders, J. W. and Smith, Graeme (2008). Formal ensemble engineering. Springer Verlag. doi: 10.1007/978-3-540-89437-7_8

  • Introducing objects through refinement

    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

  • Refactoring real-time specifications

    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

  • Towards more flexible development of Z specifications

    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

  • Using Model Checking to Automatically Find Retrieve Relations

    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

  • A stepwise development process for reasoning about the reliability of real-time systems

    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

  • Simulation machines for checking action system refinements

    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

  • Compositional class refinement in object-Z

    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

  • Verifying data refinements using a model checker

    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

  • Model checking Z specifications using SAL

    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

  • Model checking downward simulations

    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

  • A formal framework for modelling and analysing mobile systems

    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

  • Architectural design in object-z

    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

  • Linear temporal logic and z refinement

    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

  • Animation of object-z specifications using a Z animator

    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

  • Compositional verification for object-Z

    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

  • Proving Temporal Properties of Z Specifications Using Abstraction

    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

  • Abstract specification in Object-Z and CSP

    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. doi: 10.1007/3-540-36103-0_14

  • An integration of real-time object-Z and CSP for specifying concurrent real-time systems

    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

  • An introduction to real-time Object-Z

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

  • Encoding Object-Z in Isabelle/HOL

    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

  • Introducing reference semantics via refinement

    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

  • Specifying mode requirements of embedded systems

    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.

  • Model checking object-Z classes: Some experiments with FDR

    Kassel, Geoff and Smith, Graeme (2001). Model checking object-Z classes: Some experiments with FDR. doi: 10.1109/apsec.2001.991513

  • Introducing parallel composition to the timed refinement calculus

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

  • Recursive schema definitions in Object-Z

    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.

  • Safety assurance of Commercial-Off-The-Shelf software

    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.

  • Stepwise development from ideal specifications

    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

  • Structural refinement in Object-Z / CSP

    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

  • Structuring real-time Object-Z specifications

    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

  • From ideal to realisable real-time specifications

    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.

  • Specification and refinement of a real-time control system

    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.

  • Towards real-time Object-Z

    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

  • Refinement and verification of concurrent systems specified in Object-Z and CSP

    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.

  • A semantic integration of object-Z and CSP for the specification of concurrent systems

    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

  • Extending W for object-Z

    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.

  • Formal definitions of behavioural compatibility for active and passive objects

    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

Completed Supervision

This staff member is a UQ Expert for media in the following fields:

Formal methods, Mathematical modelling, Software-intensive systems, Multi-agent systems, Self-adaptive systems

They are happy to lend their expertise to your articles or broadcasts and share their research discoveries and insights with the community via media channels.

For additional assistance with story ideas, general advice and information or help with seeking further experts, please email the UQ Media Team or telephone (07) 3365 1120.

Links

ResearcherID: F-9960-2014

ORCID: 0000-0003-1019-4761

Scopus ID: 56504168900

Google Scholar ID: JRxfQowAAAAJ

Personal Profile: Link

Unit Links
Other Media

Related Resources

Similar Staff
Researchers in Associated Units
Fields of Research