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
1998
Other Outputs
Deadlines are termination
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.
1997
Journal Article
A formal method for building concurrent real-time software
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
1996
Conference Publication
Coercing real-time refinement: a transmitter
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
1996
Conference Publication
Integrating real-time scheduling theory and program refinement
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
1996
Conference Publication
A real-time refinement calculus that changes only time
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
1995
Conference Publication
Interactively verifying a simple real-time scheduler
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
1995
Conference Publication
Interactively verifying a simple real-time scheduler
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.
1995
Conference Publication
Animating Z: Interactivity, transparency and equivalence
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
1994
Book
Real time behaviour of a RISC processor: specification and computer-aided verification
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.
1994
Book
Pipeline specification of a MIPS R3000 CPU
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.
1994
Conference Publication
A layered real-time specification of a RISC processor
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
1993
Conference Publication
Modular reasoning in an object-oriented refinement calculus
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
1992
Book
Specification issues for real-time behaviour of RISC processors
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.
1992
Conference Publication
A tactic driven refinement tool
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
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: