Overview
Background
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.
Availability
- Associate Professor Mark Utting is:
- Available for supervision
Fields of research
Qualifications
- Doctor of Philosophy, University of New South Wales
Research interests
-
Software Verification
Using automated and interactive theorem proving and static analysis tools to verify the correctness of software.
-
Verification of Smart Contracts
Formal verification of smart contracts for blockchain applications.
-
AI for Testing
Using model-based testing and other test discovery algorithms to partially automate the design and execution of software test suites.
-
Software Engineering and Language Engineering
The design, implementation, analysis, and usage of secure programming languages.
Works
Search Professor Mark Utting’s works on UQ eSpace
2006
Journal Article
Un panorama du test à partir de modèles formels
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
2005
Journal Article
Requirements traceability in automated test generation: application to smart card software validation
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
2005
Conference Publication
Requirements traceability in automated test generation: application to smart card software validation
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
2005
Conference Publication
CZT: a framework for Z tools
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
2005
Conference Publication
CZT support for Z extensions
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
2005
Conference Publication
JML-testing-tools: a symbolic animator for JML specifications using CLP
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
2005
Conference Publication
Symbolic animation of JML specifications
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
2004
Journal Article
Controlling test case explosion in test generation from B formal models
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
2004
Conference Publication
Boundary coverage criteria for test generation from formal models
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
2004
Conference Publication
Faster analysis of formal specifications
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
2003
Conference Publication
Object orientation without extending Z
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
2003
Conference Publication
ZML: XML support for standard Z
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
2003
Conference Publication
Tabling structures for bottom-up logic programming
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
2002
Conference Publication
Automated boundary testing from Z and B
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
2002
Journal Article
ERGO 6: A generic proof engine that uses prolog proof technology
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
2002
Conference Publication
A comparison of the BTT and TTF test-generation methods
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
2001
Journal Article
Teaching formal methods lite via testing
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
2001
Journal Article
A sequential real-time refinement calculus
Hayes, I. J. and Utting, M. (2001). A sequential real-time refinement calculus. Acta Informatica, 37 (6), 385-448. doi: 10.1007/PL00013311
2000
Conference Publication
A survey of software development practices in the New Zealand software industry
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
1998
Book Chapter
Deadlines are termination
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
Supervision
Availability
- Associate Professor Mark Utting is:
- Available for supervision
Before you email them, read our advice on how to contact a supervisor.
Available projects
-
Verifying compiler optimization passes
We have an on-going project 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/HOL interactive theorem prover.
-
Smart Contract Tools for Blockchains - correctness and bug-finding
I am interested in supervising projects relating to the analysis and verification of smart contracts, for blockchains such as Ethereum, Algorand, Aptos (and other Move-powered blockchains), etc.
This could involve developing static analysis algorithms to prove simple correctness properties, automated verification (using SMT solvers like Z3) of deeper properties, or full verification of more complex properties using interactive provers such as Isabelle/HOL. It would also be interesting to explore the use of automated test generation (black box or fuzzing) to try and find bugs in smart contracts and counter-examples to properties that they are expected to satisfy.
-
Improved program development tools.
I am interested in supervising projects on better methods of programming - tools that help programmers develop secure programs, correct programs. There are many ways of working towards this goal, including improved IDEs, automated analysis tools, light-weight proof tools, automated assertion checking, wide-spectrum languages that include specification constructs as well as executable code, gray-box fuzzing to find interesting counter-examples, etc.
-
Generative programming and correctness
Recently there has been a big jump in the capabilities of AI-based program generators, such as CoPilot (https://github.com/features/copilot) and ChatGPT, which can generate code from English descriptions. But how can a programmer know if the suggested code is correct? Does it have the desired behaviour for the most common use case? What does it do for all those edge cases? This project will explore ways of increasing the programmer confidence in the correctness of suggested code. For example, this could involve various kinds of automated test generation, counter-example generation, runtime invariant checking, or light-weight automated software verification.
-
Verifying compiler optimization passes
We have an on-going project 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/HOL interactive theorem prover.
-
Smart Contract Tools for Blockchains - correctness and bug-finding
I am interested in supervising projects relating to the analysis and verification of smart contracts, for blockchains such as Ethereum, Algorand, Aptos (and other Move-powered blockchains), etc.
This could involve developing static analysis algorithms to prove simple correctness properties, automated verification (using SMT solvers like Z3) of deeper properties, or full verification of more complex properties using interactive provers such as Isabelle/HOL. It would also be interesting to explore the use of automated test generation (black box or fuzzing) to try and find bugs in smart contracts and counter-examples to properties that they are expected to satisfy.
-
Improved program development tools.
I am interested in supervising projects on better methods of programming - tools that help programmers develop secure programs, correct programs. There are many ways of working towards this goal, including improved IDEs, automated analysis tools, light-weight proof tools, automated assertion checking, wide-spectrum languages that include specification constructs as well as executable code, gray-box fuzzing to find interesting counter-examples, etc.
-
Generative programming and correctness
Recently there has been a big jump in the capabilities of AI-based program generators, such as CoPilot (https://github.com/features/copilot), ChatGPT, and other large language models (LLMs), which can generate code from English descriptions. But how can a programmer know if the suggested code is correct? Does it have the desired behaviour for the most common use case? What does it do for all those edge cases? This project will explore ways of increasing the programmer confidence in the correctness of suggested code. For example, this could involve various kinds of automated test generation, counter-example generation, runtime invariant checking, or light-weight automated software verification.
Supervision history
Current supervision
-
Doctor Philosophy
Verifying GraalVM Compiler Optimizations
Principal Advisor
Other advisors: Emeritus Professor Ian Hayes
-
Doctor Philosophy
Verifying Compiler Optimisation Passes
Principal Advisor
Other advisors: Emeritus Professor Ian Hayes
-
Doctor Philosophy
A Trustworthy Compiler for Ethereum Smart Contracts
Principal Advisor
Other advisors: Dr Naipeng Dong
-
Master Philosophy
Optimizing Software Development: Hierarchical Formal Specification Integration for Enhanced Unit Testing and Agile Synergy
Principal Advisor
Other advisors: Dr Guowei Yang
-
Doctor Philosophy
Evaluating and Improving Type Inference Models for Web Application Reverse Engineering
Associate Advisor
Other advisors: Professor Michael Bruenig, Professor Ryan Ko
-
Doctor Philosophy
Continuous Code Analysis for Rapidly Evolving Software
Associate Advisor
Other advisors: Associate Professor Guangdong Bai, Dr Guowei Yang
-
Doctor Philosophy
Verified Secure Compilation for C-like Programs
Associate Advisor
Other advisors: Associate Professor Graeme Smith
Media
Enquiries
For media enquiries about Associate Professor Mark Utting's areas of expertise, story ideas and help finding experts, contact our Media team: