Project summary

Compilers are an essential ingredient of the computing base, and the GraalVM compiler is a widely-used optimizing compiler for Java and other languages. The focus of this project is on the verification of compiler optimization passes because these are commonly the source of compiler errors. The GraalVM compiler uses a sophisticated ‘sea of nodes’ intermediate representation (IR) that combines the control-flow and data-flow graphs, and optimizations are complex transformations of these IR graphs. We are modelling and verifying these optimizations using the Isabelle interactive theorem prover, to ensure that the optimizations preserve correctness under all circumstances.


View publications

Partner organization(s)


Project members

Lead investigator:

Emeritus Professor Ian Hayes

Emeritus Professor
School of Electrical Engineering and Computer Science

Other investigator(s):

Associate Professor Mark Utting

Associate Professor in Software Eng
School of Electrical Engineering and Computer Science

Mr Brae Webb

PhD Candidate