Graeme Smith


Associate Professor


School of Electrical Engineering and Computer Science
The University of Queensland 4072
Australia

email: g.smith1@uq.edu.au

Professional Activities

Editor

Science of Computer Programming, 2015-2023

Invited keynote speaker

24th International Conference on Software Engineering and Formal Methods (ICFEM 2023)
Presentation title: "Compositional reasoning at the software/hardware interface". Abstract on page xiii of Y. Li and S. Tahar, editors, 24th International Conference on Software Engineering and Formal Methods (ICFEM 2023). Springer-Verlag, 2023.

Programme co-chair

Cyber Defence Next Generation Technology and Science Conference (CDNG 2022)
Formal Methods Teaching Workshop and Tutorial (FMTea 2019)
International Refinement Workshop (Refine 2007)
International Conference on Integrated Formal Methods (IFM 2005, IFM 2004)
International Conference on Integrated Formal Methods (Doctoral Symposium) (IFM 2005 (Doctoral Symposium))

Guest editor

Formal Aspects of Computing (volume 22,number 1), 2010.
Electronic Notes in Theoretical Computer Science (volume 191), 2007.
Formal Aspects of Computing (volume 17, number 4), 2005.
L'Objet (volume 6, number 1), 1999.

Programme committee member

International Conference on Formal Methods in Software Engineering (FormaliSE 2027)
International Symposium on Formal Methods (FM 2026)
International Symposium on Formal Methods (Tutorials) (FM 2026 (Tutorials))
Formal Methods Teaching Workshop and Tutorial (FMTea 2026, FMTea 2024 FMTea 2023, FMTea 2021)

European Symposium on Programming (ESOP 2023)
International Conference on Software Engineering and Formal Methods (SEFM 2022, SEFM 2021, SEFM 2019, SEFM 2018, SEFM 2017, SEFM 2016, SEFM 2003)
International Conference on Integrated Formal Methods (PhD Symposium) (PhD-iFM2022)
Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2020)
International Refinement Workshop (Refine 2019, Refine 2018, Refine 2015, Refine 2013, Refine 2011)
International Conference on Formal Engineering Methods (ICFEM 2018, ICFEM2013, ICFEM 2012, ICFEM 2010, ICFEM 2004, ICFEM 2003)
International Workshop on Formal Methods for Safety-Critical Systems (FTSCS 2018)
International Symposium on Theoretical Aspects of Software Engineering (TASE 2018, TASE 2015, TASE 2013)
International Conference on Integrated Formal Methods (iFM 2017, iFM 2014, iFM 2013, iFM2012, iFM2010, iFM 2009, IFM 2007, IFM2002, IFM2000, IFM99)
International Symposium on Formal Methods (Doctoral Symposium) (FM 2015 (Doctoral Symposium), FM 2014 (Doctoral Symposium))
IEEE International Conference on Self-Adaptive and Self-Organizing Systems (SASO 2012, SASO 2011)
Workshop on Trustworthy Self-Organizing Systems (TSOS 2012, TSOS 2011, TSOS 2010)
Asia-Pacific Software Engineering Conference (APSEC 2012)
International Z User Meeting (ZUM 2006)
International Conference of Z and B Users (ZB 2005, ZB 2003, ZB 2002)

Other

FME Formal Methods Teaching Committee, 2018 - present
CSIRO's Data61 and DST Cyber Security Summer School organising committee, 2019-2022.
ERCIM InterLink Working Group on Software-Intensive Systems and New Computing Paradigms, 2007-2008
Z Standardisation Review Committee, 1999-2002
Object-Z webpage

Current Projects

Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT) (2023-2026) Funded by Engineering and Physical Sciences Research Council, UK (EPSRC)

Boogie Analysis of Secure Information flow Logics (BASIL) (2022-2026) Funded by Defence Science and Technology Group (DSTG)

Past Projects

Resilient and Secure systems through Verified security Policies (RSVP) (2025-2026) Funded by Defence Science and Technology Group (DSTG)

Automated Rely/Guarantee Generation (RG-Gen) (2023-2026) Funded by Defence Science and Technology Group (DSTG)

BAP ARMv8 Lifter Extension (2022) Funded by Defence Science and Technology Group (DSTG)

Automated Invariant Discovery Assistant (AIDA) (2021-2022) Funded by Defence Science and Technology Group (DSTG)

Trustworthiness of Symbolic Executors (2021) Funded by Defence Science and Technology Group (DSTG)

Verifiably correct transactional memory (2018-2021) Funded by Engineering and Physical Sciences Research Council, UK (EPSRC)

Verifying expressive information flow security for weak memory concurrent programs (2019-2021) Funded by Defence Science and Technology Group (DSTG)

Disassembly of ARM binaries for security vulnerability analysis (2019-2020) Funded by Defence Science and Technology Group (DSTG)

Relaxed correctness criteria for modern multi-core architectures (2016-2019) Funded by Australian Research Council (ARC)

A mechanized framework for weak memory model security (2019) Funded by Defence Science and Technology Group (DSTG)

Publications

Book

  1. G. Smith. The Object-Z Specification Language. Advances in Formal Methods Series. Kluwer Academic Publishers, 2000.

Edited Proceedings

  1. B. Dongol, L. Petre and G. Smith. Formal Methods Teaching Workshop and Tutorial (FMTea 2019), volume 11758 of Lecture Notes in Computer Science. Springer-Verlag, 2019.
  2. E. Boiten, J. Derrick and G. Smith, editors, International Refinement Workshop (Refine 2007), volume 201 of Electronic Notes Theoretical Computer Science. Elsevier, 2008.
  3. J. Romijn, G. Smith and J. van de Pol, editors, Integrated Formal Methods: 5th International Conference, IFM 2005, volume 3771 of Lecture Notes in Computer Science. Springer-Verlag, 2005.
  4. E.A. Boiten, J. Derrick and G. Smith, editors, Integrated Formal Methods: 4th International Conference, IFM 2004, volume 2999 of Lecture Notes in Computer Science. Springer-Verlag, 2004.

Book Chapters

  1. J. Derrick, G. Smith, L. Groves and B. Dongol. A proof method for linearizability on TSO architectures. In M. Hinchey, J.P. Bowen and E.-R. Olderog, editors, Provably Correct Systems. NASA Monographs in System and Software Engineering. Springer-Verlag. 2017.
  2. J.W. Sanders and G. Smith. Formal ensemble engineering. In M. Wirsing, J.-P. Banâtre, M. Hölzl and A. Rauschmayer, editors, Challenges for Software-Intensive Systems and New Computing Paradigms, volume 5380 of Lecture Notes in Computer Science, pp. 132-138. Springer-Verlag. 2008.
  3. G. Smith. Extending formal methods for software-intensive systems. In M. Wirsing, J.-P. Banâtre, M. Hölzl and A. Rauschmayer, editors, Challenges for Software-Intensive Systems and New Computing Paradigms, volume 5380 of Lecture Notes in Computer Science., pp.146-161. Springer-Verlag, 2008.
  4. G. Smith. State-based approaches: From Z to Object-Z. In H. Bowman and J. Derrick, editors, Formal Methods for Distributed Processing: A Survey of Object-Oriented Approaches, chapter 6, pages 105-125. Cambridge University Press, 2001.

Journal Publications

  1. B. Dongol, C. Dubois, S. Hallerstede, E. Hehner, C. Morgan, P. Müller, L. Ribeiro, A. Silva, G. Smith, E. de Vink. On Formal Methods Thinking in Computer Science Education. In Formal Aspects of Computing. ACM, 2024.
  2. N. Coughlin, K. Winter and G. Smith. Compositional reasoning for non-multicopy atomic architectures. In Formal Aspects of Computing. ACM, 2022. PDF
  3. N. Coughlin and G. Smith. Compositional noninterference on hardware weak memory models. In Science of Computer Programming. Elsevier, 2022. Selected for the FM 2023 Journal First Track. PDF
  4. G. Smith, N. Coughlin and T. Murray. Information-flow control on ARM and POWER multicore processors. In Formal Methods in System Design. Springer, 2021. PDF
  5. G. Smith, K. Winter and R.J. Colvin. Linearizability on hardware weak memory models. Formal Aspects of Computing, 32:1-32. Springer, 2020. PDF
  6. K. Winter, G. Smith and J. Derrick. Modelling concurrent objects running on the TSO and ARMv8 memory models. Science of Computer Programming, 184. Elsevier, 2019. PDF
  7. G. Smith and K. Winter. Relating trace refinement and linearizability. Formal Aspects of Computing, 29(6):935-950. Springer, 2017. PDF
  8. Q. Li and G. Smith. Refining autonomous agents with declarative beliefs and desires. Formal Aspects of Computing, 29(2):227-249. Springer, 2017. PDF
  9. Q. Li and G. Smith. Formal development of multi-agent systems using MAZE. Science of Computer Programming, 131:126-150. Elsevier, 2016. PDF
  10. G. Smith, J.W. Sanders and K. Winter. Designing adaptive systems using teleo-reactive agents. Transactions on Computational Collective Intelligence XVI, volume 8780 of Lecture Notes in Computer Science. Springer-Verlag, 2014. PDF
  11. J. Derrick and G. Smith. Temporal logic property preservation under Z refinement. Formal Aspects of Computing, 24(3):393-416. Springer-Verlag, 2012.
  12. J.W. Sanders and G. Smith. Emergence and refinement. Formal Aspects of Computing, 24(1):45-65. Springer-Verlag, 2012.
  13. Z. Fu and G. Smith. Property transformation under specification change. Frontiers of Computer Science in China, 5(1):1-13. Springer-Verlag, 2010.
  14. G. Smith and K. Winter. Model checking action system refinements. Formal Aspects of Computing, 21(1):155-186. Springer-Verlag, 2009.
  15. G. Smith and J. Derrick. Verifying data refinements using a model checker. Formal Aspects of Computing, 18(3):264-287. Springer-Verlag, 2006.
  16. J. Derrick and G. Smith. Structural refinement of systems specified in Object-Z and CSP. Formal Aspects of Computing, 15(1):1-27. Springer-Verlag, 2003.
  17. G. Smith and I.J. Hayes. An introduction to Real-Time Object-Z. Formal Aspects of Computing, 13(2):128-141. Springer-Verlag, 2002.
  18. G. Smith and J. Derrick. Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods in System Design, 18(3):249-284. Kluwer Academic Publishers, 2001.
  19. G. Smith and C. Fidge. Incremental development of real-time requirements: The light control case study. Journal of Universal Computer Science, 6(7):704-730. Springer-Verlag, 2000.
  20. R. Duke, C. Bailes and G. Smith. A blocking model for reactive objects. Formal Aspects of Computing, 8(3):347-368. Springer-Verlag, 1996.
  21. R. Duke, C. Bailes and G. Smith. A fully abstract model of reactive objects. Formal Aspects of Computing, 8(D):184-243. Springer-Verlag, 1996.
  22. G. Smith. A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing, 7(3):289-313. Springer-Verlag, 1995.
  23. G. Smith. A fully abstract semantics of classes for Object-Z (full paper). Formal Aspects of Computing, 7(E):30-66. Springer-Verlag, 1995.
  24. R. Duke, G. Rose and G. Smith. Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces, 17:511-533. North-Holland, 1995. (Updated version available as a technical report.)
  25. R. Duke and G. Smith. Temporal logic and Z Specifications. Australian Computer Journal, 21(2):62-66, 1989.

Fully Refereed Conference Publications

  1. J. Tobler and G. Smith. Generating Rely-Guarantee Conditions with the Conditional-Writes Domain. In International Symposium on Formal Methods (FM 2026). Lecture Notes in Computer Science. Springer-Verlag, 2026.
  2. G. Smith and H. Whitlock. Autograding Weakest Precondition Proofs and Dafny Specifications. In Formal Methods Teaching Workshop (FMTea 2026). Lecture Notes in Computer Science. Springer-Verlag, 2026. Winner of Best Paper Award.
  3. G. Smith. Detecting speculative data flow vulnerabilities using weakest precondition reasoning. In International Symposium on Theoretical Aspects of Software Engineering (TASE 2025). Lecture Notes in Computer Science. Springer-Verlag, 2025.
  4. N. Coughlin, K. Lam, G. Smith and K. Winter. Detecting speculative execution vulnerabilities on weak memory models. In International Symposium on Formal Methods (FM 2024). Lecture Notes in Computer Science. Springer-Verlag, 2024.
  5. G. Smith. A Dafny-based approach to thread-local information flow analysis. In International Conference on Formal Methods in Software Engineering (FormaliSE 2023). IEEE, 2023. PDF
  6. G. Smith. Declassification predicates for controlled information release. In International Conference on Formal Engineering Methods (ICFEM 2022). Lecture Notes in Computer Science. Springer-Verlag, 2022. PDF
  7. N. Coughlin, K. Winter and G. Smith. Rely/guarantee reasoning for multicopy atomic weak memory models. In International Symposium on Formal Methods (FM 2021). Lecture Notes in Computer Science. Springer-Verlag, 2021. Winner of Best Paper Award. Selected for the ICSE 2023 Showcase Track. PDF
  8. K. Winter, N. Coughlin and G. Smith. Backwards-directed information flow analysis for concurrent programs. In IEEE Computer Security Foundations Symposium (CSF 2021). IEEE, 2021. PDF
  9. N. Coughlin and G. Smith. Rely/Guarantee Reasoning for Noninterference in Non-Blocking Algorithms. In IEEE Computer Security Foundations Symposium (CSF 2020). IEEE, 2020. PDF
  10. G. Smith and L. Groves. Weakening correctness and linearizability for concurrent objects on multicore processors. In International Refinement Workshop (Refine 2019). Lecture Notes in Computer Science. Springer-Verlag, 2020. PDF
  11. G. Smith and D. Duke. Specification with class: A brief history of Object-Z. In History of Formal Methods Workshop (HFM 2019). Lecture Notes in Computer Science. Springer-Verlag, 2020.
  12. G. Smith, N. Coughlin and T. Murray. Value-dependent information-flow security on weak memory models. In International Symposium on Formal Methods (FM 2019). Lecture Notes in Computer Science. Springer-Verlag, 2019. PDF
  13. K. Winter, G. Smith and J. Derrick. Observational models for linearizability checking on weak memory models. In International Symposium on Theoretical Aspects of Software Engineering (TASE 2018). IEEE, 2018.
  14. G. Smith, K. Winter and R.J. Colvin. Correctness of concurrent objects under weak memory models. In Intenational Refinement Worskshop (Refine 2018). Electronic Proceeding in Theoretical Computer Science. Open Publishing Association, 2018.
  15. R.J. Colvin and G. Smith. A wide-spectrum language for verification of programs on weak memory models. In International Symposium on Formal Methods (FM 2018), volume 10951 of Lecture Notes in Computer Science. Springer-Verlag, 2018.
  16. P. Doolan, G. Smith, C. Zhang and P. Krishnan. Improving the Scalability of Automatic Linearizability Checking in SPIN. In International Conference on Formal Engineering Methods (ICFEM 2017), volume 10610 of Lecture Notes in Computer Science. Springer-Verlag, 2017. PDF
  17. J. Derrick and G. Smith. An observational approach to defining linearizability on weak memory models. In International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2017), volume 10321 of Lecture Notes in Computer Science. Springer-Verlag, 2017.
  18. G. Smith. Model checking simulation rules for linearizability. In International Conference on Software Engineering and Formal Methods (SEFM 2016), volume 9763 of Lecture Notes in Computer Science. Springer-Verlag, 2016. PDF
  19. G. Smith and J. Derrick. Invariant generation for linearizability proofs. In ACM Symposium on Applied Computing (SAC 2016). ACM, 2016.
  20. J. Derrick and G. Smith. A framework for correctness criteria on weak memory models. In International Symposium on Formal Methods (FM 2015), Lecture Notes in Computer Science. Springer-Verlag, 2015.
  21. B. Dongol, J. Derrick, L. Groves and G. Smith. Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. In European Conference on Object-Oriented Programming (ECOOP 2015), LIPIcs-Leibniz International Proceedings in Informatics. Dagstuhl Publishing, 2015.
  22. G. Smith, J.W. Sanders and Q. Li. A macro-level model for investigating the effect of directional bias on network coverage. In Australasian Computer Science Conference (ACSC 2015), volume 159 of Conferences in Research and Practice in Information Technology. Australian Computer Society, 2015.
  23. S. Moeiniyan Bagheri, G. Smith and J. Hanan. Using Z in the development and maintenance of computational models of real-world systems. In Human Oriented Formal Methods (HOFM 2014) , volume 8938 of Lecture Notes in Computer Science. Springer-Verlag, 2015. PDF
  24. G. Smith, J. Derrick and B. Dongol. Admit your weakness: Verifying correctness on TSO architectures. In International Symposium on Formal Aspects of Component Software (FACS 2014), volume 8997 of Lecture Notes in Computer Science. Springer-Verlag, 2015.
  25. J. Derrick, G. Smith, B. Dongol and L. Groves. Using coarse-grained abstractions to verify linearizability on TSO architectures. In Haifa Verification Conference (HVC 2014), volume 8855 of Lecture Notes in Computer Science. Springer-Verlag, 2014
  26. G. Smith, J.W. Sanders and Q. Li. On directional bias for network coverage. In International Conference on Biologically Inspired Computing:Theory and Applications (BIC-TA 2014), Communications in Computer and Information Science. Springer-Verlag, 2014. PDF
  27. B. Dongol, J. Derrick and G. Smith. Reasoning algebraically about refinement on TSO architectures. In International Colloquium on Theoretical Aspects of Computing (ICTAC 2014), volume 8687 of Lecture Notes in Computer Science. Springer-Verlag, 2014.
  28. J. Derrick, G. Smith and B. Dongol. Verifying linearizability on TSO architectures. In International Conference on Integrated Formal Methods (iFM 2014), volume 8739 of Lecture Notes in Computer Science. Springer-Verlag, 2014.
  29. Q. Li and G. Smith. A formal development approach for self-organising systems. In International Symposium on Theoretical Aspects of Software Engineering (TASE 2014). IEEE Computer Society Press, 2014. PDF
  30. G. Smith and Q. Li. MAZE: An extension of Object-Z for multi-agent systems. In International ABZ Conference (ABZ 2014), volume 8477 of Lecture Notes in Computer Science. Springer-Verlag, 2014.
  31. Q. Li and G. Smith. A refinement framework for autonomous agents. In Brazilian Symposium on Formal Methods (SBMF 2013), volume 8195 of Lecture Notes in Computer Science. Springer-Verlag, 2013. PDF
  32. Q. Li and G. Smith. Using bounded fairness to specify and verify ordered asynchronous multi-agent systems. In IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2013). IEEE Computer Society Press, 2013.
  33. G. Smith and K. Winter. Incremental development of multi-agent systems in Object-Z. In Software Engineering Workshop (SEW-35). IEEE Computer Society Press, 2012. The original publication is available at ieeexplore.ieee.org.
  34. G. Smith and J.W. Sanders. Using conventional reasoning techniques for self-organising systems. In Annual Conference on Privacy, Security and Trust (PST 2012). IEEE Computer Society Press, 2012. The original publication is available at ieeexplore.ieee.org.
  35. G. Smith, J.W. Sanders and K. Winter. Reasoning about adaptivity of agents and multi-agent systems. In IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012). IEEE Computer Society Press, 2012. The original publication is available at ieeexplore.ieee.org.
  36. G. Smith and S. Helke. Refactoring object-oriented specifications with inheritance-based polymorphism. In IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2011). IEEE Computer Society Press, 2011. The original publication is available at ieeexplore.ieee.org.
  37. J.W. Sanders and G. Smith. Assuring adaptive behaviour in self-organising systems. In IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshop (SASOW 2010). IEEE Computer Society Press, 2010. The original publication is available at ieeexplore.ieee.org.
  38. S. Eder and G. Smith. An approach to formal verification of free-flight separation. In IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshop (SASOW 2010). IEEE Computer Society Press, 2010. The original publication is available at ieeexplore.ieee.org.
  39. A. Sampson and G. Smith. Gravity points in potential-field approaches to self organisation. In IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshop (SASOW 2010). IEEE Computer Society Press, 2010. The original publication is available at ieeexplore.ieee.org.
  40. J.W. Sanders and G. Smith. Refining emergent properties. In International Refinement Workshop (Refine 2009), volume 259 of Electronic Notes in Theoretical Computer Science, pp. 207-233. Elsevier, 2009. The original paper is available at www.sciencedirect.com.
  41. G. Smith and J.W. Sanders. Formal development of self-organising systems. In International Conference on Autonomic and Trusted Computing (ATC-09), volume 5586 of Lecture Notes in Computer Science, pp. 90-104. Springer-Verlag, 2009. The original paper is available at www.springer.com.
  42. G. Smith and T. McComb. Refactoring real-time specifications. In International Refinement Workshop (Refine 2008), volume 214 of Electronic Notes in Theoretical Computer Science, pp. 359-380. Elsevier, 2008.
  43. Z. Fu and G. Smith. Towards more flexible development of Z specifications. In IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), pp. 281-288. IEEE Computer Society Press, 2008.
  44. T. McComb and G. Smith. A minimal set of refactoring rules for Object-Z. In International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2008), volume 5051 of Lecture Notes in Computer Science, pp. 170-184. Springer-Verlag, 2008.
  45. T. McComb and G. Smith. Introducing objects through refinement. In International Conference on Formal Methods (FM 2008), volume 5014 of Lecture Notes Computer Science, pp. 358-373. Springer-Verlag, 2008.
  46. J. Derrick and G. Smith. Using model checking to automatically find retrieve relations. In E. Boiten, J. Derrick and G. Smith, editors, International Refinement Workshop (Refine 2007), volume 201 of Electronic Notes in Theoretical Computer Science, pp. 155-175. Elsevier, 2008.
  47. L. Meinicke and G. Smith. A stepwise development process for reasoning about the reliability of real-time systems. In 6th International Conference on Integrated Formal Methods (IFM 2007), volume 4591 of Lecture Notes in Computer Science, pp. 439-458. Springer-Verlag, 2007.
  48. G. Smith and K. Winter. Simulation machines for checking action system refinements. In B. Aichernig, E. Boiten, J. Derrick and L. Groves, editors, International Refinement Workshop (Refine 2006), volume 187 of Electronic Notes in Theoretical Computer Science, pp. 75-90. Elsevier, 2007.
  49. T. McComb and G.Smith. Compositional class refinement in Object-Z. In Formal Methods (FM 2006). volume 4085 of Lecture Notes in Computer Science, pp. 205-220. Springer-Verlag, 2006.
  50. G. Smith and J. Derrick. Model checking downward simulations. In J. Derrick and E. Boiten, editors, International Refinement Workshop (Refine 2005), Issue 2, volume 137 of Electronic Notes in Theoretical Computer Science,pp.205-224. Elsevier, 2005.
  51. G. Smith and L. Wildman. Model checking Z specifications using SAL. In H. Treharne, S. King, M. Henson and S. Schneider, editors, International Conference of B and Z Users (ZB 2005), volume 3455 of Lecture Notes in Computer Science, pp.85-103. Springer-Verlag, 2005.
  52. J. Derrick and G. Smith. Linear Temporal Logic and Z refinement. In Algebraic Methodology and Software Technology (AMAST 2004), volume 3116 of Lecture Notes in Computer Science. Springer-Verlag, 2004.
  53. T. McComb and G. Smith. Architectural design in Object-Z. In Australian Software Engineering Conference (ASWEC 2004). IEEE Computer Society, 2004.
  54. G. Smith. A formal framework for modelling and analysing mobile systems. In Australasian Computer Science Conference (ACSC 2004), Australian Computer Society, 2004.
  55. T. McComb and G. Smith. Animation of Object-Z specifications using a Z animator. In International Conference on Software Engineering and Formal Methods (SEFM 2003), IEEE Computer Society, 2003.
  56. G. Smith and K. Winter. Proving temporal properties of Z specifications using abstraction. In D. Bert, J.P. Bowen, S. King and M. Walden, editors, 3rd International Conference of Z and B Users (ZB 2003), volume 2561 of Lecture Notes in Computer Science, pages 260-279. Springer-Verlag, 2003.
  57. K. Winter and G. Smith. Compositional verification for Object-Z. In D. Bert, J.P. Bowen, S. King and M. Walden, editors, 3rd International Conference of Z and B Users (ZB 2003), volume 2561 of Lecture Notes in Computer Science, pages 280-299. Springer-Verlag, 2003.
  58. G. Smith. Introducing reference semantics via refinement. In C. George and Huaikou Miao, editors, 4th International Conference on Formal Engineering Methods (ICFEM 2002), volume 2495 of Lecture Notes in Computer Science, pages 588-599. Springer-Verlag, 2002.
  59. G. Smith and J. Derrick. Abstract specification in Object-Z and CSP. In C. George and Huaikou Miao, editors, 4th International Conference on Formal Engineering Methods (ICFEM 2002), volume 2495 of Lecture Notes in Computer Science, pages 108-119. Springer-Verlag, 2002.
  60. G. Smith. An integration of Real-Time Object-Z and CSP for specifying concurrent real-time systems. In K. Sere and M. Butler, editors, 3rd International Conference on Integrated Formal Methods (IFM 2002), volume 2335 of Lecture Notes in Computer Science, pages 267-285. Springer-Verlag, 2002.
  61. G. Smith, F. Kammüller and T. Santen. Encoding Object-Z in Isabelle/HOL. In D. Bert, J.P. Bowen, M.C. Henson and K. Robinson, editors, 2nd International Conference of Z and B Users (ZB 2002), volume 2272 of Lecture Notes in Computer Science, pages 82-99. Springer-Verlag, 2002.
  62. G. Smith. Specifying mode requirements of embedded systems. In M. Oudshoorn, editor, 25th Australasian Computer Science Conference (ACSC 2002), Australian Computer Science Communications, volume 24(1): 251-258. Australian Computer Society, 2002.
  63. G. Kassel and G. Smith. Model checking Object-Z classes: Some experiments with FDR. In 8th Asia-Pacific Software Engineering Conference (APSEC 2001), pages 445-452. IEEE Computer Society Press, 2001.
  64. G. Smith. Introducing parallel composition to the Timed Refinement Calculus. In H. ElGindy and C. Fidge, editors, Parallel and Real-Time Systems (PART 2000), pages 139-148, Springer-Verlag, 2001.
  65. G. Smith and I.J. Hayes. Structuring Real-Time Object-Z specifications. In W. Grieskamp, T. Santen and B. Stoddart, editors, Integrated Formal Methods (IFM 00), volume 1945 of Lecture Notes in Computer Science, pages 97-115. Springer-Verlag, 2000.
  66. J. Derrick and G. Smith. Structural refinement in Object-Z/CSP. In W. Grieskamp, T. Santen and B. Stoddart, editors, Integrated Formal Methods (IFM 00), volume 1945 of Lecture Notes in Computer Science, pages 194-213. Springer-Verlag, 2000.
  67. P. Lindsay and G. Smith. Safety assurance of Commercial-Off-The-Shelf software. In A. Griffiths, editor, 5th Australian Workshop on Safety Critical Systems and Software, pages 43-51. Australian Computer Society, 2000.
  68. G. Smith. Recursive schema definitions in Object-Z. In J.P. Bowen, S. Dunne, A. Galloway and S. King, editors, 1st International Conference of Z and B Users (ZB 2000), volume 1878 of Lecture Notes in Computer Science, pages 42-58. Springer-Verlag, 2000.
  69. G. Smith. Stepwise development from ideal specifications. In J. Edwards, editor, 23rd Australasian Computer Science Conference (ACSC 2000), Australian Computer Science Communications, volume 22(1):227-233. IEEE Computer Society, 2000.
  70. G. Smith and I.J. Hayes. Towards Real-Time Object-Z. In K. Araki, A.Galloway and K. Taguchi, editors, Integrated Formal Methods (IFM 99), pages 49-65. Springer-Verlag, 1999.
  71. G. Smith. Specification and refinement of a real-time control system. In J. Edwards, editor, Australasian Computer Science Conference (ACSC'99), Australian Computer Science Communications, Vol. 21, No. 1, pages 360-371. Springer-Verlag, 1999.
  72. C. Fischer and G. Smith. Combining CSP and Object-Z: Finite trace or infinite trace semantics? In T. Mizuno, N. Shiratori, T. Higashino and A.Togashi, editors, Formal Description Techniques and Protocol Specification, Verification, and Testing (FORTE/PSTV'97), pages 503-518. Chapman & Hall, 1997.
  73. G. Smith and J. Derrick. Refinement and verification of concurrent systems specified in Object-Z and CSP. In First IEEE International Conference on Formal Engineering Methods (ICFEM'97), pages 293-302. IEEE Computer Press, 1997.
  74. G. Smith. A semantic integration of Object-Z and CSP for the specification of concurrent systems. In J. Fitzgerald, C.B. Jones and P. Lucas, editors, Formal Methods Europe (FME'97), volume 1313 of Lecture Notes in Computer Science, pages 62-81. Springer-Verlag, 1997.
  75. G. Smith. Reasoning about Object-Z specifications. In Proceedings Asia-Pacific Software Engineering Conference (APSEC '95), pages 489-497, IEEE Computer Society Press, 1995.
  76. G. Smith. Extending W for Object-Z. In J. Bowen and M. Hinchey, editors, 9th International Conference of Z Users (ZUM'95), volume 967 of Lecture Notes in Computer Science, pages 276-295. Springer-Verlag, 1995.
  77. G. Smith. Formal definitions of behavioural compatibility for active and passive objects. In Proceedings Asia-Pacific Software Engineering Conference (APSEC '94), pages 336-344, IEEE Computer Society Press, 1994.
  78. N. Lévy and G.Smith. A language-independent approach to specification construction. In D. Wile, editor, Proceedings ACM SIGSOFT Symposium on the Foundations of Software Engineering, Software Engineering Notes, 19(5):76-86, ACM Press, 1994.
  79. G. Smith. An object-oriented development framework for Z. In J. Bowen and J. Hall, editors, 8th Z User Meeting (ZUM'94), pages 89-107. Workshops in Computing, Springer-Verlag, 1994.
  80. G. Smith. A development framework for object-oriented specification and refinement. In B. Magnusson, B. Meyer, J.-M. Nerson and J.-F. Perrot, editors, Proceedings Technology of Object-Oriented Languages and Systems (TOOLS EUROPE '94), pages 173-183, 1994.
  81. G. Smith and R. Duke. Specifying concurrent systems using Object-Z. In Proceedings 15th Australian Computer Science Conference (ACSC-15), pages 859-871, 1992.
  82. R. Duke, P. King, G. Rose and G. Smith. The Object-Z Specification Language. In T. Korson, V. Vaishnavi and B. Meyer, editors, Technology of Object-Oriented Languages and Systems (TOOLS 5), pages 465-483. Prentice-Hall, 1991.
  83. R. Duke, P. King and G. Smith. Combining formal methods with object-oriented design: An emerging trend in software engineering. In Proceedings Australian Computer Conference (ACC'91 MOSAIC), pages 181-194, 1991.
  84. R. Duke, P. King and G. Smith. Formalising behavioural compatibility for reactive object-oriented systems. In Proceedings 14th Australian Computer Science Conference (ACSC-14), pages 11/1-11/11, 1991.
  85. R. Duke, G. Rose and G. Smith. Transferring formal techniques to industry: A case study. In J. Quemada, J. Manas and E. Vazquez, editors, Formal Description Techniques (FORTE'90), pages 279-286. North-Holland, 1990.
  86. P. King and G. Smith. Formalisation of behavioural and structural concepts for communications systems. In L. Logrippo, R. L. Probert and H. Ural, editors, Protocol Specification, Testing and Verification X (PSTV X), pages 1-18. North-Holland, 1990.
  87. D. Carrington and G. Smith. Extending Z for object-oriented specifications. In Proceedings 5th Australian Software Engineering Conference (ASWEC'90), pages 9-14, 1990.
  88. G. Smith and R. Duke. Modelling a cache coherence protocol using Object-Z. In Proceedings 13th Australian Computer Science Conference (ACSC-13), pages 352-361, 1990.
  89. D. Carrington, D. Duke, R. Duke, P. King, G. Rose and G. Smith. Object-Z: An object-oriented extension to Z. In S. Voung, editor, Formal Description Techniques (FORTE'89), pages 281-296. North-Holland, 1990.
  90. G. Smith. A formal specification of Signalling System No. 7 Telephone User Part. In Proceedings 1989 Singapore International Conference on Networks (SICON'89), pages 50-55, 1989.
  91. R. Duke and G. Smith. Temporal logic and Z Specifications. In Proceedings 12th Australian Computer Science Conference (ACSC-12), Appendix, pages 32-42, 1989. Selected by programme commitee for publication in the Australian Computer Journal.

Other Publications

  1. G. Smith. Detecting speculative data flow vulnerabilities using weakest precondition reasoning. CoRR, abs/2504.19128, 2025.
  2. G. Smith. Compositional reasoning at the software/hardware interface. Abstract of keynote presentation, page xiii of Y. Li and S. Tahar, editors, 24th International Conference on Software Engineering and Formal Methods (ICFEM 2023). Springer-Verlag, 2023.
  3. R. Colvin and G. Smith. A high-level operational semantics for hardware weak memory models. CoRR, abs/1812.00996, 2018.
  4. G. Smith, J.W. Sanders, and Q. Li. A macro-level model for investigating the effect of directional bias on network coverage. CoRR, abs/1407.5762, 2014.
  5. G. Smith. Incremental development of software-intensive systems. In, J.-P. Banâtre, M. Hölzl and M. Wirsing, editors, Opening InterLink Workshop: Thematic Area 1 (TA1/WG1) Software Intensive Systems and New Computing Paradigms. Technical Report, Institut fur Informatik, Ludwig-Maximilians-Universitat Munchen, 2007.
  6. J. Romijn, G. Smith and J. van de Pol, editors, IFM2005 Doctoral Symposium on Integrated Formal Methods. CS-Report 05-29, Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, 2005.
  7. P. Lindsay and G. Smith. Safety assurance of Commercial-Off-The-Shelf software. In Software Engineering Australia (SEA 2000), 2000.
  8. G. Smith. From ideal to realisable real-time specifications. In N. Leslie, editor, Fifth New Zealand Formal Program Development Colloquium, IIMS Technical Report 99-1, Institute of Information and Mathematical Sciences, Massey University at Albany, 1999.
  9. G. Smith. Integrating Object-Z and CSP for the specification of object-oriented concurrent systems, Contribution 7 of R. Bastide and D. Buchs, Models, Formalisms and Methods for Object-Oriented Distributed Computing. In S. Mitchell and J. Bosch, editors, European Conference on Object-Oriented Programming (ECOOP'97) Workshop Reader, volume 1357 of Lecture Notes in Computer Science. Springer-Verlag, 1997.
  10. G. Smith. Formal Verification of Object-Z Specifications. Technical Report 95-55, Software Verification Research Centre, University of Queensland, 1995.
  11. G. Smith. A Logic for Object-Z (Additional Rules). Technical Report 95-26, Software Verification Research Centre, University of Queensland, 1995.
  12. G. Smith. An Object-Oriented Approach to Formal Specification, Department of Computer Science, University of Queensland, 1993.

On This Site