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
2024
Book
Distributed Ledger Technology: 7th International Symposium, SDLT 2023, Brisbane, QLD, Australia, November 30 – December 1, 2023, Revised Selected Papers
Naipeng Dong, Babu Pillai, Guangdong Bai and Mark Utting eds. (2024). Distributed Ledger Technology: 7th International Symposium, SDLT 2023, Brisbane, QLD, Australia, November 30 – December 1, 2023, Revised Selected Papers. Communications in Computer and Information Science, Heidelberg, Germany: Springer. doi: 10.1007/978-981-97-0006-6
2024
Conference Publication
EVM-Vale: formal verification of EVM bytecode using vale
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
2023
Conference Publication
TypeScript’s evolution: an analysis of feature adoption over time
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
2023
Conference Publication
Differential testing of a verification framework for compiler optimizations (Case study)
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
2023
Other Outputs
Discussion Paper: 2023-2030 Australian Cyber Security Strategy
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.
2023
Conference Publication
Verifying term graph optimizations using Isabelle/HOL
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
2023
Conference Publication
Verifying compiler optimisations (invited paper)
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
2022
Conference Publication
Verification of EVM Bytecode with Vale
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.
2022
Journal Article
Verifying Whiley programs with Boogie
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
2021
Journal Article
Automatic proofs of memory deallocation for a Whiley-to-C Compiler
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
2021
Conference Publication
A formal semantics of the GraalVM intermediate representation
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
2020
Conference Publication
Tool support for refactoring manual tests
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
2020
Conference Publication
Identifying and generating missing tests using machine learning on execution traces
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
2019
Conference Publication
An introduction to software verification with Whiley
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
2017
Conference Publication
Static techniques for reducing memory usage in the C implementation of Whiley programs
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
2017
Conference Publication
Making Whiley boogie!
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
2016
Conference Publication
Bound Analysis for Whiley Programs
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
2016
Book Chapter
Recent advances in model-based testing
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
2015
Other Outputs
Method of evaluating genomic sequences
Cleary, John Gerald and Utting, Barry Mark (2015). Method of evaluating genomic sequences. US9165253B2.
2015
Journal Article
Impact of technology uptake on an Australian electricity distribution network
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
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.
Supervision history
Current supervision
-
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
Verifying Compiler Optimisation Passes
Principal Advisor
Other advisors: Emeritus Professor Ian Hayes
-
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
-
Doctor Philosophy
Evaluating and Improving Type Inference Models for Web Application Reverse Engineering
Associate Advisor
Other advisors: Professor Michael Bruenig, Professor Ryan Ko
Media
Enquiries
For media enquiries about Associate Professor Mark Utting's areas of expertise, story ideas and help finding experts, contact our Media team: