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.
Supervision
Availability
- Associate Professor Mark Utting is:
- Available for supervision
Looking for a supervisor? Read our advice on how to choose 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), 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
Evaluating and Improving Type Inference Models for Web Application Reverse Engineering
Principal Advisor
Other advisors: Professor Ryan Ko
-
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
Continuous Code Analysis for Rapidly Evolving Software
Associate Advisor
Other advisors: Dr Guowei Yang
-
Doctor Philosophy
Verified Secure Compilation for C-like Programs
Associate Advisor
Other advisors: Associate Professor Graeme Smith
Completed supervision
-
2025
Doctor Philosophy
Verifying GraalVM Compiler Optimizations
Principal Advisor
Other advisors: Emeritus Professor Ian Hayes
Media
Enquiries
For media enquiries about Associate Professor Mark Utting's areas of expertise, story ideas and help finding experts, contact our Media team: