Associate Professor Graeme Smith
Associate Professor
School of Electrical Engineering and Computer Science
Researcher biography
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.
Publications
Book
Smith, G. P. (1999). The Object-Z Specification Language. Boston: Kluwer Academic Publishers. doi: 10.1007/978-1-4615-5265-9
Book Chapters
Coughlin, Nicholas, Lam, Kait, Smith, Graeme and Winter, Kirsten (2024). Detecting Speculative Execution Vulnerabilities on Weak Memory Models. Lecture Notes in Computer Science. (pp. 482-500) Cham: Springer Nature Switzerland. doi: 10.1007/978-3-031-71162-6_25
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
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
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. (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
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 Articles
Dongol, Brijesh, Dubois, Catherine, Hallerstede, Stefan, Hehner, Eric, Morgan, Carroll, Müller, Peter, Ribeiro, Leila, Silva, Alexandra, Smith, Graeme and de Vink, Erik (2024). On Formal Methods Thinking in Computer Science Education. Formal Aspects of Computing. doi: 10.1145/3670419
Coughlin, Nicholas, Winter, Kirsten and Smith, Graeme (2023). Compositional reasoning for non-multicopy atomic architectures. Formal Aspects of Computing, 35 (2) 8, 1-30. doi: 10.1145/3574137
Coughlin, Nicholas and Smith, Graeme (2022). Compositional noninterference on hardware weak memory models. Science of Computer Programming, 217 102779, 1-23. doi: 10.1016/j.scico.2022.102779
Smith, Graeme, Coughlin, Nicholas and Murray, Toby (2021). Information-flow control on ARM and POWER multicore processors. Formal Methods in System Design, 58 (1-2), 251-293. doi: 10.1007/s10703-021-00376-2
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
Winter, Kirsten, Smith, Graeme and Derrick, John (2019). Modelling concurrent objects running on the TSO and ARMv8 memory models. Science of Computer Programming, 184 102308, 102308. doi: 10.1016/j.scico.2019.102308
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
Li, Qin and Smith, Graeme (2016). Refining autonomous agents with declarative beliefs and desires. Formal Aspects of Computing, 29 (2), 1-23. doi: 10.1007/s00165-016-0391-1
Derrick, John and Smith, Graeme (2012). Temporal-logic property preservation under Z refinement. Formal Aspects of Computing, 24 (3), 393-416. doi: 10.1007/s00165-011-0177-4
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
Fu, Zheng and Smith, Graeme (2011). Property transformation under specification change. Frontiers of Computer Science in China, 5 (1), 1-13. doi: 10.1007/s11704-010-0112-5
Boiten, Eerke, Butler, Michael, Derrick, John and Smith, Graeme (2010). Formal Aspects of Computing: Editorial. Formal Aspects of Computing, 22 (1), 1-1. doi: 10.1007/s00165-009-0147-2
Sanders, J. W. and Smith, Graeme (2009). Refining Emergent Properties. Electronic Notes in Theoretical Computer Science, 259 (C), 207-223. doi: 10.1016/j.entcs.2009.12.026
Smith, Graeme and Winter, Kirsten (2009). Model checking action system refinements. Formal Aspects of Computing, 21 (1-2), 155-186. doi: 10.1007/s00165-007-0053-4
Smith, Graeme and McComb, Tim (2008). Refactoring Real-time Specifications. Electronic Notes in Theoretical Computer Science, 214 (C), 359-380. doi: 10.1016/j.entcs.2008.06.016
Derrick, John and Smith, Graeme (2008). Using Model Checking to Automatically Find Retrieve Relations. Electronic Notes in Theoretical Computer Science, 201 (C), 155-175. doi: 10.1016/j.entcs.2008.02.019
Boiten, Eerke, Derrick, John and Smith, Graeme (2008). Preface. Electronic Notes in Theoretical Computer Science, 201 (C), 1. doi: 10.1016/j.entcs.2008.02.012
Smith, Graeme and Winter, Kirsten (2007). Simulation Machines for Checking Action System Refinements. Electronic Notes in Theoretical Computer Science, 187, 75-90. doi: 10.1016/j.entcs.2006.08.045
Boiten, E., Derrick, J. and Smith, G. (2005). Guest Editorial integrated formal methods. Formal Aspects of Computing, 17 (4), 389-389. doi: 10.1007/s00165-005-0078-5
Romijn, Judi, Smith, Graeme, Van De Pol, Jaco, Bert, Didier, Boiten, Eerke, Bowen, Jonathan, Butler, Michael, Curzon, Paul, Davies, Jim, Derrick, John, Dunne, Steve, Dong, Jin Song, Galloway, Andy, George, Chris, Grieskamp, Wolfgang, Habrias, Henri, Heisel, Maritta, Kim, Soon-Kyeong, Lemoine, Michel, Liu, Shaoying, Mery, Dominique, Merz, Stephan, Paige, Richard, Petre, Luigia, Santen, Thomas, Schneider, Steve, Schulte, Wolfram, Sere, Kaisa, Sinclair, Jane ... Woodcock, Jim (2005). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3771 LNCS
Derrick, John and Smith, Graeme (2004). Linear temporal logic and Z refinement. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3116, 117-131. doi: 10.1007/978-3-540-27815-3_13
Boiten, Eerke, Derrick, John and Smith, Graeme (2004). Preface. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2999, V-VI.
Winter, Kirsten and Smith, Graeme (2003). Compositional verification for Object-Z. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2651, 280-299.
Smith, Graeme and Winter, Kirsten (2003). Proving temporal properties of Z specifications using abstraction. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2651, 260-279.
Derrick, John and Smith, Graeme P. (2003). Structural refinement of systems specified in object-z and CSP. Formal Aspects of Computing, 15 (1), 1-27. doi: 10.1007/s00165-003-0002-9
Smith, G and Derrick, J (2001). Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP. Formal Methods In System Design, 18 (3), 249-284. doi: 10.1023/A:1011269103179
Smith, G. P. and Fidge, C. J. (2000). Incremental development of real-time requirements: The light control case study. Journal of Universal Computer Science, 6 (7), 704-730.
Duke, Roger, Bailes, Cecily and Smith, Graeme (1996). A blocking model for reactive objects. Formal Aspects of Computing, 8 (3), 347-368. doi: 10.1007/BF01214919
Duke R., Rose G. and Smith G. (1995). Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces, 17 (5-6), 511-533. doi: 10.1016/0920-5489(95)00024-O
Smith, Graeme (1995). A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing, 7 (3), 289-313. doi: 10.1007/BF01211075
Conference Papers
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
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
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
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
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
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
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
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
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
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
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
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 (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
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
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
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
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
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
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
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
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
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 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 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 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
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
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
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.
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
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
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
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
Sanders, J. W. and Smith, Graeme (2008). Formal ensemble engineering. Springer Verlag. doi: 10.1007/978-3-540-89437-7_8
Smith, Graeme (2008). Extending formal methods for software-intensive systems. Springer Verlag. doi: 10.1007/978-3-540-89437-7_10
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
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, 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
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 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. (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., 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). 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 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
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. (2002). Specifying mode requirements of embedded systems. 25th Australasian Computer Science Conference (ACSC 2002), Melbourne, VIC Australia, 28 January - 1 February 2002. Adelaide, SA Australia: Australian Computer Society.
Kassel, Geoff and Smith, Graeme (2001). Model checking object-Z classes: Some experiments with FDR. doi: 10.1109/apsec.2001.991513
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.
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
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, 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
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. 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. 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, 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, 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
Department Technical Reports
Smith, Graeme and Winter, Kirsten (2006). Simulation Machines or Checking Action System Refinements. Technical Report No. SSE-2006-03. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
McComb, Tim and Smith, Graeme (2006). Refactoring Object-Oriented Specifications: A Process for Deriving Designs. Technical Report SSE-2006-01. School of Information Technology and Electrical Engineering, The University of Queensland.
Winter, Kirsten and Smith, Graeme (2002). Compositional Verification for Object-Z. Technical Report 02-42. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Smith, Graeme (2001). State-Based Formal Methods for Distributed Processing: From Z to Object-Z. Technical Report 01-34. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Lindsay, P. and Smith, G. (2000). Safety Assurance of Commercial-Off-The-Shelf Software. Technical Report no. 00-17. Software Verification Research Centre, School of Information Technology, The University of Queensland.
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.
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.
Research Reports
McComb, T. J. and Smith, G. P. (2002). Using Z to animate Object-Z specifications. Brisbane, Australia: The University of Queensland.
Smith, G. P. (2001). Specifying mode requirements for embedded systems. Brisbane: Software Verification Research Cen. Univ of Qld.
Smith, G. P., Kammuller, F and Santen, T (2001). Encoding Object-Z in Isabelle-HOL. Brisbane: Software Verification Research Cen. Univ of Qld.
Kassel, G. D. and Smith, G. P. (2001). Model checking Object-Z classes: Some experiments with FDR. Brisbane: Software Verification Research Cen. Univ of Qld.
Smith, G. P. and Derrick, J. (2001). Specification, refinement and verification of concurrent systems: an integration of Object-Z and CSP. Brisbane: Software Verification Research Cen. Univ of Qld.
Smith, G. P. (2001). State-based formal methods for distributed processing: from Z to Object-Z. Brisbane: Software Verification Research Cen. Univ of Qld.