Graeme Smith


Associate Professor
Study Abroad Coordinator
Software Engineering Plan Director


School of Information Technology and Electrical Engineering
The University of Queensland 4072
Australia

email: smith@itee.uq.edu.au

Professional Activities

Editor

Science of Computer Programming

Programme co-chair

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 Software Engineering and Formal Methods (SEFM 2016, SEFM 2003)
International Refinement Workshop (Refine 2015, Refine 2013, Refine 2011)

International Symposium on Theoretical Aspects of Software Engineering (TASE 2015, TASE 2013)
International Symposium on Formal Methods (Doctoral Symposium) (
FM 2015 (Doctoral Symposium), FM 2014 (Doctoral Symposium))
International Conference on Integrated Formal Methods (iFM 2014, iFM 2013, iFM2012, iFM2010, iFM 2009, IFM 2007, IFM2002, IFM2000, IFM99)
International Conference on Formal Engineering Methods (ICFEM2013, ICFEM 2012, ICFEM 2010, ICFEM 2004, ICFEM 2003)

IEEE International Conference on Self-Adaptive and Self-Organizing Systems (SASO 2012, SASO 2011)
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

Member of ERCIM InterLink Working Group on Software-Intensive Systems and New Computing Paradigms, 2007-2008

Member of Z Standardisation Review Committee, 1999-2002

Object-Z webpage

Current Projects

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

This project seeks to lay groundwork for fully exploiting the potential of multicore computers. Multicore computers have become ubiquitous over the last decade, now being standard in everything from laptops to mobile phones. Their benefits are clear – better performance leading to more sophisticated applications. Key to ensuring those benefits are complex, and often subtle, algorithms that exploit the parallelism that multicore computers offer. This project aims to lay foundations for extending those benefits to applications where high reliability is a concern. It plans to do so by developing theoretical results about the correctness of algorithms on standard multicore computers, and practical tools and techniques to help programmers of multicore computers to better understand the behaviour of their code.

Verifying concurrent algorithms on weak memory models (2015-2018) Funded by Engineering and Physical Sciences Research Council, UK (EPSRC)

Verifiably correct high-performance libraries for multi-core architectures (2016-2017) Funded by Engineering and Physical Sciences Research Council, UK (EPSRC)

Publications

Book

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

Edited Proceedings

  1. E. Boiten, J. Derrick and G. Smith, editors, International Refinement Workshop (Refine 2007), volume 201 of Electronic Notes Theoretical Computer Science. Elsevier, 2008.
  2. 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.
  3. 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. To appear in M. Hinchey, J.P. Bowen and E.-R. Olderog, editors, Provably Correct Systems. NASA Monographs in System and Software Engineering. Springer-Verlag. 2016.
  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. Q. Li and G. Smith. Refining autonomous agents with declarative beliefs and desires. To appear in Formal Aspects of Computing. Springer, 2016.
  2. Q. Li and G. Smith. Formal development of multi-agent systems using MAZE. Science of Computer Programming. Elsevier, 2016.
  3. 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.
  4. J. Derrick and G. Smith. Temporal logic property preservation under Z refinement. Formal Aspects of Computing, 24(3):393-416. Springer-Verlag, 2012.
  5. J.W. Sanders and G. Smith. Emergence and refinement. Formal Aspects of Computing, 24(1):45-65. Springer-Verlag, 2012. The final publication is available at www.springer.com.
  6. Z. Fu and G. Smith. Property transformation under specification change. Frontiers of Computer Science in China, 5(1):1-13. Springer-Verlag, 2010.
  7. G. Smith and K. Winter. Model checking action system refinements. Formal Aspects of Computing, 21(1):155-186. Springer-Verlag, 2009.
  8. G. Smith and J. Derrick. Verifying data refinements using a model checker. Formal Aspects of Computing, 18(3):264-287. Springer-Verlag, 2006.
  9. 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.
  10. G. Smith and I.J. Hayes. An introduction to Real-Time Object-Z. Formal Aspects of Computing, 13(2):128-141. Springer-Verlag, 2002.
  11. 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.
  12. 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.
  13. R. Duke, C. Bailes and G. Smith. A blocking model for reactive objects. Formal Aspects of Computing, 8(3):347-368. Springer-Verlag, 1996.
  14. 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.
  15. G. Smith. A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing, 7(3):289-313. Springer-Verlag, 1995.
  16. G. Smith. A fully abstract semantics of classes for Object-Z (full paper). Formal Aspects of Computing, 7(E):30-66. Springer-Verlag, 1995.
  17. 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.)
  18. R. Duke and G. Smith. Temporal logic and Z Specifications.Australian Computer Journal, 21(2):62-66, 1989.

Fully Refereed Conference Publications

  1. 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.
  2. G. Smith and J. Derrick. Invariant generation for linearizability proofs. In ACM Symposium on Applied Computing (SAC 2016). ACM, 2016.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. Q. Li and G. Smith. A refinement framework for autonomous agents. InBrazilian Symposium on Formal Methods (SBMF 2013), volume 8195 of Lecture Notes in Computer Science. Springer-Verlag, 2013.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. 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.

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

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

  29. 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.
  30. 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.
  31. 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.
  32. 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.
  33. 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.
  34. 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.
  35. 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.
  36. T. McComb and G. Smith. Architectural design in Object-Z. In Australian Software Engineering Conference (ASWEC 2004). IEEE Computer Society, 2004.
  37. G. Smith. A formal framework for modelling and analysing mobile systems. In Australasian Computer Science Conference (ACSC 2004), Australian Computer Society, 2004.
  38. 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.
  39. G. Smith and K. Winter. Proving temporal properties of Z specifications using abstraction. In D. Bert, J.P. Bowen, S. King and M. Waldén, 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.
  40. K. Winter and G. Smith. Compositional verification for Object-Z. In D. Bert, J.P. Bowen, S. King and M. Waldén, 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.
  41. 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.
  42. 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.
  43. 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.
  44. 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.
  45. 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.
  46. 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.
  47. 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.
  48. 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.
  49. 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.
  50. 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.
  51. 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.
  52. 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.
  53. 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.
  54. 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.
  55. 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.
  56. 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.
  57. 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.
  58. G. Smith. Reasoning about Object-Z specifications. In Proceedings Asia-Pacific Software Engineering Conference (APSEC '95), pages 489-497, IEEE Computer Society Press, 1995.
  59. 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.
  60. 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.
  61. 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.
  62. 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.
  63. 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.
  64. G. Smith and R. Duke. Specifying concurrent systems using Object-Z. In Proceedings 15th Australian Computer Science Conference (ACSC-15), pages 859-871, 1992.
  65. 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.
  66. 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.
  67. 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.
  68. R. Duke, G. Rose and G. Smith. Transferring formal techniques to industry: A case study. In J. Quemada, J. Mañas and E. Vazquez, editors, Formal Description Techniques (FORTE'90), pages 279-286. North-Holland, 1990.
  69. 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.
  70. D. Carrington and G. Smith. Extending Z for object-oriented specifications. In Proceedings 5th Australian Software Engineering Conference (ASWEC'90), pages 9-14, 1990.
  71. 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.
  72. 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.
  73. 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.
  74. 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, 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.
  2. 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 für Informatik, Ludwig-Maximilians-Universität Munchen, 2007.
  3. 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.
  4. P. Lindsay and G. Smith. Safety assurance of Commercial-Off-The-Shelf software. In Software Engineering Australia (SEA 2000), 2000.
  5. 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.
  6. G. Smith. Integrating Object-Z and CSP for the specification of object-oriented concurrent systems. 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.

PhD Thesis

  1. G. Smith. An Object-Oriented Approach to Formal Specification, Department of Computer Science, University of Queensland, 1993.

Selected Technical Reports (not published elsewhere)

  1. G. Smith. Formal Verification of Object-Z Specifications. Technical Report 95-55, Software Verification Research Centre, University of Queensland, 1995.
  2. G. Smith. A Logic for Object-Z (Additional Rules). Technical Report 95-26, Software Verification Research Centre, University of Queensland, 1995.