Associate Professor Mark Utting

Associate Professor in Software Eng

School of Information Technology and Electrical Engineering
Faculty of Engineering, Architecture and Information Technology
m.utting@uq.edu.au
+61 7 336 53310

Overview

Associate Professor Mark Utting's research interests include software correctness, model-based testing, and machine learning. He received his PhD from UNSW on the semantics of object-oriented languages, and since then has worked as an academic at several Queensland universities, as well as Waikato University in NZ and the University of Franche-Comte in France. He is passionate about designing and engineering good software that solves real-world problems, has extensive experience with managing software development projects and teams both in academia and industry, and has worked in industry, developing next generation genomics software and manufacturing software. He is author of the book ‘Practical Model-Based Testing: A Tools Approach’, as well as more than 80 publications on model-based testing, verification techniques for object-oriented and real-time software, and language design for parallel computing.

Research Interests

  • Software Verification
    Using automated and interactive theorem proving and static analysis tools to verify the correctness of software.
  • AI for Testing
    Using machine learning and model-based testing to partially automate the design and execution of software test suites.
  • Verification of Smart Contracts
    Formal verification of smart contracts for blockchain applications.

Qualifications

  • Doctor of Philosophy, University of New South Wales

Publications

  • Bernard, Elodie, Botella, Julien, Ambert, Fabrice, Legeard, Bruno and Utting, Mark (2020). Tool support for refactoring manual tests. 2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST), Porto, Portugal, 24-28 October 2020. Piscataway, NJ, United States: Institute of Electrical and Electronics Engineers. doi: 10.1109/icst46399.2020.00041

  • Utting, Mark, Legeard, Bruno, Dadeau, Frederic, Tamagnan, Frederic and Bouquet, Fabrice (2020). Identifying and generating missing tests using machine learning on execution traces. IEEE International Conference on Artificial Intelligence Testing (AITest), Oxford, United Kingdom, 3-6 August 2020. Piscataway, NJ, United States: IEEE. doi: 10.1109/aitest49225.2020.00020

  • Pearce, David J., Utting, Mark and Groves, Lindsay (2019). An introduction to software verification with Whiley. Third International School, SETSS 2017, Chongqing, China, 17-22 April 2017. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-030-17601-3_1

View all Publications

Grants

View all Grants

Available Projects

  • These two $40K PhD scholarships are part of a new project funded by Oracle Labs Australia to model and verify sophisticated compiler optimisations in the Graal Java compiler. Graal is a high-performance polyglot virtual machine (VM) that not only supports JVM-based languages such as Java, Scala, Kotlin and Groovy, and LLVM-based languages like C and C++, but also more dynamic languages like Python and JavaScript. This research project focuses on verifying optimization passes of the Graal compiler, using the Isabelle interactive theorem prover.

View all Available Projects

Publications

Book

Book Chapter

  • Utting, Mark, Legeard, Bruno, Bouquet, Fabrice, Fourneret, Elizabeta, Peureux, Fabien and Vernotte, Alexandre (2016). Recent advances in model-based testing. Advances in Computers. (pp. 53-120) Maryland Heights, MO, United States: Academic Press. doi: 10.1016/bs.adcom.2015.11.004

  • Utting, Mark (2011). How to design extended finite state machine test models in Java. Model-based testing for embedded systems. (pp. 1-24) Boca Raton, FL, United States: CRC Press. doi: 10.1201/b11321-7

  • Hayes, I. J. and Utting, M. (1998). Deadlines are termination. Programming Concepts and Methods PROCOMET ’98. (pp. 186-204) Boston, MA, United States: Springer. doi: 10.1007/978-0-387-35358-6_15

Journal Article

Conference Publication

  • Bernard, Elodie, Botella, Julien, Ambert, Fabrice, Legeard, Bruno and Utting, Mark (2020). Tool support for refactoring manual tests. 2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST), Porto, Portugal, 24-28 October 2020. Piscataway, NJ, United States: Institute of Electrical and Electronics Engineers. doi: 10.1109/icst46399.2020.00041

  • Utting, Mark, Legeard, Bruno, Dadeau, Frederic, Tamagnan, Frederic and Bouquet, Fabrice (2020). Identifying and generating missing tests using machine learning on execution traces. IEEE International Conference on Artificial Intelligence Testing (AITest), Oxford, United Kingdom, 3-6 August 2020. Piscataway, NJ, United States: IEEE. doi: 10.1109/aitest49225.2020.00020

  • Pearce, David J., Utting, Mark and Groves, Lindsay (2019). An introduction to software verification with Whiley. Third International School, SETSS 2017, Chongqing, China, 17-22 April 2017. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-030-17601-3_1

  • Utting, Mark, Pearce, David J. and Groves, Lindsay (2017). Making Whiley boogie!. 13th International Conference, Integrated Formal Methods 2017, Turin, Italy, 20 - 22 September 2017. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-319-66845-1_5

  • Weng, Min-Hsien, Pfahringer, Bernhard and Utting, Mark (2017). Static techniques for reducing memory usage in the C implementation of whiley programs. ACSW '17: Proceedings of the Australasian Computer Science Week Multiconference, Geelong, VIC Australia, January 2017. New York, NY USA: ACM Press. doi: 10.1145/3014812.3014827

  • Weng, Min-Hsien, Utting, Mark and Pfahringer, Bernhard (2016). Bound Analysis for Whiley Programs. Amsterdam, Netherlands: Elsevier. doi: 10.1016/j.entcs.2016.01.005

  • Drogemuller, R, Boulaire, F, Ledwich, G, Buys, L, Utting, M, Vine, D, Morris, P and Arefi, A (2014). Aggregating energy supply and demand. ECPPM 2014, 10th European Conference on Product and Process Modelling, Vienna, Austria, 17-19 September 2014. London, United Kingdom: CRC Press. doi: 10.1201/b17396-71

  • Boulaire, Fanny, Utting, Mark and Drogemuller, Robin (2014). Parallel ABM for electricity distribution grids: a case study. Euro-Par 2013: Parallel Processing Workshops, Aachen, Germany, 26 - 27 August 2013. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/978-3-642-54420-0_55

  • Boulaire, Fanny, Utting, Mark and Drogemuller, Robin (2013). MODAM: a modular agent-based modelling framework. 2nd International Workshop on Software Engineering Challenges for the Smart Grid (SE4SG), San Francisco, CA USA, 18 May 2013. Piscataway, NJ USA: Institute of Electrical and Electronics Engineers. doi: 10.1109/SE4SG.2013.6596109

  • Utting, Mark, Weng, Min-Hsien and Cleary, John G. (2013). The JStar language philosophy. 2013 International Workshop on Programming Models and Applications for Multicores and Manycores, Shenzhen, China, 23 February 2013. New York, NY USA: The Association for Computing Machinery . doi: 10.1145/2442992.2442996

  • Boulaire, Fanny, Utting, Mark, Drogemuller, Robin, Ledwich, Gerard and Ziari, Iman (2012). A hybrid simulation framework to assess the impact of renewable generators on a distribution network. 2012 Winter Simulation Conference, Berlin, Germany, 9-12 December 2012. doi: 10.1109/WSC.2012.6465000

  • Utting, Mark, Malik, Petra and Toyn, Ian (2009). Transformation rules for Z.

  • Aydal, Emine G., Paige, Richard F., Utting, Mark and Woodcock, Jim (2009). Putting formal specifications under the magnifying glass: Model-based testing for validation. doi: 10.1109/ICST.2009.20

  • Utting, Mark (2008). The role of model-based testing. doi: 10.1007/978-3-540-69149-5_56

  • Utting, Mark and Malik, Petra (2008). Unit testing of Z specifications. doi: 10.1007/978-3-540-87603-8_24

  • Aydal, Emine G., Utting, Mark and Woodcock, Jim (2008). A comparison of state-based modelling tools for model validation. 46th International Conference, TOOLS EUROPE 2008: Objects, Components, Models and Patterns, Zurich, Switzerland, June/July 2008. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/978-3-540-69824-1_16

  • Bouquet, F., Grandpierre, C., Legeard, B., Peureux, F., Vacelet, N. and Utting, M. (2007). A subset of precise UML for model-based testing. doi: 10.1145/1291535.1291545

  • Irvine, Sean A., Pavlinic, Tin, Trigg, Leonard, Cleary, John G., Inglis, Stuart and Utting, Mark (2007). Jumble java byte code to measure the effectiveness of unit tests. Mutation 2007 Conference, Windsor England, Sep 10-14, 2007. LOS ALAMITOS: IEEE. doi: 10.1109/TAICPART.2007.4344121

  • Bernard, Eddy, Bouquet, Fabrice, Charbonnier, Amandine, Legeard, Bruno, Peureux, Fabien, Utting, Mark and Torreborre, Eric (2006). Model-based testing from UML models.

  • Miller, Tim, Freitas, Leo, Malik, Petra and Utting, Mark (2005). CZT support for Z extensions. IFM 2005: Integrated Formal Methods, Eindhoven, The Netherlands, 29 November - 2 December 2005. Berlin, Germany: Springer. doi: 10.1007/11589976_14

  • Malik, Petra and Utting, Mark (2005). CZT: a framework for Z tools. ZB 2005: ZB 2005: Formal Specification and Development in Z and B, Guildford, United Kingdom, 13 - 15 April 2005. Berlin, Germany: Springer. doi: 10.1007/11415787_5

  • Bouquet, Fabrice, Dadeau, Frédéric, Legeard, Bruno and Utting, Mark (2005). JML-testing-tools: a symbolic animator for JML specifications using CLP. TACAS 2005: Tools and Algorithms for the Construction and Analysis of Systems, Edinburgh, United Kingdom, 4 - 8 April 2005. Heidelberg, Germany: Springer. doi: 10.1007/978-3-540-31980-1_37

  • Bouquet, F., Jaffuel, E., Legeard, B., Peureux, F. and Utting, M. (2005). Requirements traceability in automated test generation: application to smart card software validation. A-MOST '05: 1st international workshop on Advances in model-based testing, St Louis, MO, United States, 15 - 16 May 2005. New York, NY, United States: Association for Computing Machinery. doi: 10.1145/1083274.1083282

  • Bouquet, Fabrice, Dadeau, Frédéric, Legeard, Bruno and Utting, Mark (2005). Symbolic animation of JML specifications. FM 2005: FM 2005: Formal Methods, Newcastle, United Kingdom, 18 - 22 July 2005. Heidelberg, 69121 Germany: Springer. doi: 10.1007/11526841_7

  • Kosmatov, Nikolai, Legeard, Bruno, Peureux, Fabien and Utting, Mark (2004). Boundary coverage criteria for test generation from formal models. IEEE Computer Society. doi: 10.1109/issre.2004.12

  • Bouquet, Fabrice, Legeard, Bruno, Utting, Mark and Vacelet, Nicolas (2004). Faster analysis of formal specifications. ICFEM 2004: Formal Methods and Software Engineering, Seattle, WA, United States, 8 - 12 November 2004. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/978-3-540-30482-1_24

  • Utting, Mark and Wang, Shaochun (2003). Object orientation without extending Z. ZB 2003: Formal Specification and Development in Z and B, Turku, Finland, 4 - 6 June 2003. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-44880-2_20

  • Clayton, Roger, Cleary, John G., Pfahringer, Bernhard and Utting, Mark (2003). Tabling structures for bottom-up logic programming. LOPSTR 2002: Logic Based Program Synthesis and Transformation, Madrid, Spain, September 2002. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-45013-0_5

  • Utting, Mark, Toyn, Ian, Sun, Jing, Martin, Andrew, Dong, Jin Song, Daley, Nicholas and Currie, David (2003). ZML: XML support for standard Z. ZB 2003: ZB 2003: Formal Specification and Development in Z and B, Turku, Finland, 4 - 6 June 2003. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-44880-2_26

  • Legeard, Bruno, Peureux, Fabien and Utting, Mark (2002). A comparison of the BTT and TTF test-generation methods. ZB 2002: ZB 2002:Formal Specification and Development in Z and B, Grenoble, France, 23 - 25 January 2002. Berlin, Germany: Springer Verlag. doi: 10.1007/3-540-45648-1_16

  • Legeard, Bruno, Peureux, Fabien and Utting, Mark (2002). Automated boundary testing from Z and B. FME 2002: FME 2002:Formal Methods—Getting IT Right, Copenhagen, Denmark, 22 - 24 July 2002. Berlin, Germany: Springer Verlag. doi: 10.1007/3-540-45614-7_2

  • Groves, Lindsay, Nickson, Ray , Reeve, Greg, Reeves, Steve and Utting, Mark (2000). A survey of software development practices in the New Zealand software industry. 2000 Australian Software Engineering Conference, Canberra, ACT, Australia, 28 - 29 April 2000. Piscataway, NJ, United States: Institute of Electrical and Electronics Engineers. doi: 10.1109/aswec.2000.844576

  • Utting, Mark and Fidge, Colin (1996). A real-time refinement calculus that changes only time. BCS-FACS 7th Refinement Workshop, Bath, United Kingdom, 3 - 5 July 1996. United Kingdom: British Computer Society Learning & Development. doi: 10.14236/ewic/rw1996.14

  • Hayes, Ian and Utting, Mark (1996). Coercing real-time refinement: a transmitter. BCS-FACS Northern Formal Methods Workshop, Ilkley, United Kingdom, 23-24 September 1996. BCS Learning & Development. doi: 10.14236/ewic/fa1996.9

  • Fidge, C., Utting, M., Kearney, P. and Hayes, I. (1996). Integrating real-time scheduling theory and program refinement. 3rd International Symposium of Formal Methods Europe, FME 1996, Oxford, United Kingdom, 18-22 March 1996. Springer Verlag. doi: 10.1007/3-540-60973-3_95

  • Utting, M. (1995). Animating Z: Interactivity, transparency and equivalence. 1995 Asia Pacific Software Engineering Conference, Brisbane, QLD, Australia, 6-9 December 1995. Piscataway, NJ, United States: Institute of Electrical and Electronics Engineers. doi: 10.1109/APSEC.1995.496978

  • Fidge C., Kearney P. and Utting M. (1995). Interactively verifying a simple real-time scheduler. 7th International Conference on Computer Aided Verification, CAV 1995, Liège, Belgium, 3 - 5 July 1995. Cham, Switzerland: Springer Verlag.

  • Kearney, Peter and Utting, Mark (1994). A layered real-time specification of a RISC processor. FTRTFT 1994, ProCoS 1994: Formal Techniques in Real-Time and Fault-Tolerant Systems, Lübeck, Germany, 19 - 23 September 1994. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-58468-4_178

  • Utting, Mark and Robinson, Ken (1993). Modular reasoning in an object-oriented refinement calculus. MPC 1992: Mathematics of Program Construction, Oxford, United Kingdom, 29 June - 3 July 1992. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-56625-2_22

  • Groves, Lindsay, Nickson, Raymond and Utting, Mark (1992). A tactic driven refinement tool. 5th Refinement Workshop, London, United Kingdom, 8 - 10 January 1992. London, United Kingdom: Springer London. doi: 10.1007/978-1-4471-3550-0_14

Other Outputs

  • Hayes, Ian J. and Utting, Mark (1998). Deadlines are termination. Technical Report 98-01 St Lucia, QLD, Australia: Software Verification Research Centre, School of Information Technology, The University of Queensland.

Grants (Administered at UQ)

Possible Research Projects

Note for students: The possible research projects listed on this page may not be comprehensive or up to date. Always feel free to contact the staff for more information, and also with your own research ideas.

  • These two $40K PhD scholarships are part of a new project funded by Oracle Labs Australia to model and verify sophisticated compiler optimisations in the Graal Java compiler. Graal is a high-performance polyglot virtual machine (VM) that not only supports JVM-based languages such as Java, Scala, Kotlin and Groovy, and LLVM-based languages like C and C++, but also more dynamic languages like Python and JavaScript. This research project focuses on verifying optimization passes of the Graal compiler, using the Isabelle interactive theorem prover.