Verifying GraalVM Optimization Passes

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.