Prof. Mark Utting

Title: An Introduction to Software Verification with Whiley

Biography

Dr. Mark Utting is a Senior Lecturer in ICT at the University of the Sunshine Coast (USC), in Queensland, Australia. Prior to joining USC, he worked at UQ, QUT, and Waikato University in academic positions, and he has also worked in industry, developing next generation genomics software and manufacturing software.

Mark is passionate about designing and engineering good software that solves real-world problems, and has extensive experience with managing software development projects and teams both in academia and industry. He is author of the book ‘Practical Model-Based Testing: A Tools Approach’, as well as more than 50 publications on model-based testing, verification techniques for object-oriented and real-time software, and language design for parallel computing.


Abstract

This course will introduce you to the fundamental ideas of software verification for imperative programming. We will cover basic specification techniques, how to use preconditions and postconditions, the relationship between specifications and code, techniques for verifying conditional code, loops, arrays, records, and functions. The course will include a series of hands-on verification exercises using the Whiley programming language and its online verification tool.

Course material:

Please bring your own laptops and have internet access, so that you can do the verification exercises, which will be online.