Associate Professor Mark Utting
Associate Professor in Software Eng
School of Electrical Engineering and Computer Science
+61 7 336 52386
Researcher biography
Associate Professor Mark Utting's research interests include software verification, model-based testing, theorem proving and automated reasoning, programming language design and implementation. 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, software verification, and language design and implementation. His current research focus is on using software verification to give strong guarantees about the correctness of compilers, correctness of blockchain smart contracts, freedom from information leaks of ARM64 binary programs, and the correctness of AI-generated code.
Publications
Books
Utting, Mark and Legeard, Bruno (2007). Practical model-based testing. Amsterdam, Netherlands: Elsevier. doi: 10.1016/b978-0-12-372501-1.x5000-5
Utting, Mark and Legeard, Bruno (2006). Practical model-based testing: A tools approach. Elsevier. doi: 10.1016/B978-0-12-372501-1.X5000-5
Book Chapters
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) edited by Atif Memon. Cambridge, MA, 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 Articles
Pearce, David J., Utting, Mark and Groves, Lindsay (2022). Verifying Whiley programs with Boogie. Journal of Automated Reasoning, 66 (4), 1-57. doi: 10.1007/s10817-022-09619-1
Weng, Min-Hsien, Malik, Robi and Utting, Mark (2021). Automatic proofs of memory deallocation for a Whiley-to-C Compiler. Formal Methods in System Design, 57 (3), 429-472. doi: 10.1007/s10703-021-00378-0
Boulaire, Fanny, Utting, Mark and Drogemuller, Robin (2015). Impact of technology uptake on an Australian electricity distribution network. Environmental Modelling and Software, 69, 196-213. doi: 10.1016/j.envsoft.2015.03.019
Boulaire, Fanny, Utting, Mark and Drogemuller, Robin (2015). Dynamic agent composition for large-scale agent-based models. Complex Adaptive Systems Modeling, 3 (1) 1. doi: 10.1186/s40294-015-0007-2
Utting, Mark, Weng, Min-Hsien and Cleary, John G. (2014). The JStar language philosophy. Parallel Computing, 40 (SI2), 35-50. doi: 10.1016/j.parco.2013.11.004
Utting, Mark, Pretschner, Alexander and Legeard, Bruno (2012). A taxonomy of model-based testing approaches. Software Testing Verification and Reliability, 22 (5), 297-312. doi: 10.1002/stvr.456
Mugridge, Rick, Utting, Mark and Streader, David (2011). Evolving web-based test automation into agile business specifications. Future Internet, 3 (2), 159-174. doi: 10.3390/fi3020159
Utting, Mark (2006). Un panorama du test à partir de modèles formels. Techniques et sciences informatiques, 25 (1), 133-139. doi: 10.3166/tsi.25.133-139
Bouquet, F., Jaffuel, E., Legeard, B., Peureux, F. and Utting, M. (2005). Requirements traceability in automated test generation: application to smart card software validation. ACM SIGSOFT Software Engineering Notes, 30 (4), 1-7. doi: 10.1145/1082983.1083282
Legeard, Bruno, Peureux, Fabien and Utting, Mark (2004). Controlling test case explosion in test generation from B formal models. Software Testing Verification and Reliability, 14 (2), 81-103. doi: 10.1002/stvr.287
Utting, M., Robinson, P. J. and Nickson, R. (2002). ERGO 6: A generic proof engine that uses prolog proof technology. Journal of Computation and Mathematics, 5, 194-219. doi: 10.1112/s1461157000000759
Utting, Mark and Reeves, Steve (2001). Teaching formal methods lite via testing. Software Testing Verification and Reliability, 11 (3), 181-195. doi: 10.1002/stvr.223
Hayes, I. J. and Utting, M. (2001). A sequential real-time refinement calculus. Acta Informatica, 37 (6), 385-448. doi: 10.1007/PL00013311
Fidge, Colin, Kearney, Peter and Utting, Mark (1997). A formal method for building concurrent real-time software. IEEE Software, 14 (2), 99-106. doi: 10.1109/52.582979
Conference Papers
Cumming, Daniel, Utting, Mark, Cassez, Franck, Dong, Naipeng, Bayat Tork, Sadra and Risius, Marten (2024). EVM-Vale: formal verification of EVM bytecode using vale. 7th International Symposium, SDLT 2023, Brisbane, QLD, Australia, 30 November - 1 December 2023. Heidelberg, Germany: Springer. doi: 10.1007/978-981-97-0006-6_3
Utting, Mark, Webb, Brae J. and Hayes, Ian J. (2023). Differential testing of a verification framework for compiler optimizations (Case study). IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), Melbourne, VIC Australia, 14-15 May 2023. Piscataway, NJ United States: Institute of Electrical and Electronics Engineers.. doi: 10.1109/formalise58978.2023.00015
Scarsbrook, Joshua D., Utting, Mark and Ko, Ryan K. L. (2023). TypeScript’s evolution: an analysis of feature adoption over time. IEEE/ACM 20th International Conference on Mining Software Repositories (MSR), Melbourne, VIC, Australia, 15-16 May 2023. Piscataway, NJ, United States: IEEE. doi: 10.1109/msr59073.2023.00027
Webb, Brae J., Hayes, Ian J. and Utting, Mark (2023). Verifying term graph optimizations using Isabelle/HOL. 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'23), Boston, MA, United States, 16-17 January 2023. New York, NY, United States: ACM. doi: 10.1145/3573105.3575673
Hayes, Ian J., Utting, Mark and Webb, Brae J. (2023). Verifying compiler optimisations (invited paper). 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, 21–24 November 2023. Singapore, Singapore: Springer Nature Singapore. doi: 10.1007/978-981-99-7584-6_1
Cumming, Daniel Keith, Utting, Mark, Dong, Naipeng, Cassez, Frank, Tork, S. B. and Risius, Marten (2022). Verification of EVM Bytecode with Vale. 6th Symposium on Distributed Ledger Technology 2022 (SDLT 2022), Gold Coast, QLD Australia, 22 November 2022.
Webb, Brae J., Utting, Mark and Hayes, Ian J. (2021). A formal semantics of the GraalVM intermediate representation. 19th International Symposium, ATVA 2021, Gold Coast, QLD Australia, 18-22 October 2021. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-030-88885-5_8
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
Weng, Min-Hsien, Pfahringer, Bernhard and Utting, Mark (2017). Static techniques for reducing memory usage in the C implementation of Whiley programs. ACSW '17: Australasian Computer Science Week Multiconference, Geelong, VIC Australia, January 30-February 03, 2017. New York, NY USA: ACM Press. doi: 10.1145/3014812.3014827
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, 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
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
Bouquet, F., Grandpierre, C., Legeard, B., Peureux, F., Vacelet, N. and Utting, M. (2007). A subset of precise UML for model-based testing. New York, NY, USA: ACM. doi: 10.1145/1291535.1291545
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
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
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
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
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
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
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
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
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
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
Fidge, Colin, Kearney, Peter and Utting, Mark (1995). Interactively verifying a simple real-time scheduler. CAV 1995: Computer Aided Verification, Liège, Belgium, 3-5 July 1995. Heidelberg, Germany: Springer. doi: 10.1007/3-540-60045-0_65
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.
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
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
Working Paper
Abeysooriya, Sasenka, Akhlaghpour, Saeed, Bongiovanni, Ivano, Dowsett, Dallas, Grotowski, Joseph, Holm, Mike, Kim, Dan, Ko, Ryan, Phillips, Andelka M., Slapnicar, Sergeja, Stockdale, David, Swinson, John, Thonon, Geoffroy, Utting, Mark, Walker-Munro, Brendan and Willoughby, Shannon (2023). Discussion Paper: 2023-2030 Australian Cyber Security Strategy. UQ CYBER and AUSCERT.
Patent
Cleary, John Gerald and Utting, Barry Mark (2015). Method of evaluating genomic sequences. US9165253B2.
Research Report
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.
Department Technical Reports
Kearney, Peter, Utting, Mark and Whitwell, Keith (1994). Real time behaviour of a RISC processor: specification and computer-aided verification. SVRC Technical Report, 92-10. Software Verification Research Centre, Department of Computer Science, The University of Queensland.
Utting, Mark and Kearney, Peter (1994). Pipeline specification of a MIPS R3000 CPU. SVRC Technical Report, 92-6. Software Verification Research Centre, Department of Computer Science, The University of Queensland.
Utting, Mark and Kearney, Peter (1992). Specification issues for real-time behaviour of RISC processors. SVRC Technical Report, 92-5. Software Verification Research Centre, Department of Computer Science, The University of Queensland.