4 citations · 8 across the 6 of their papers we have counts for
Showing 2022Show all
2 papers · 1 filter
cs.PL2022★ 2 cited
Verifying term graph optimizations using Isabelle/HOL
Brae J. Webb, Ian J. Hayes, Mark Utting
Our objective is to formally verify the correctness of the hundreds of expression optimization rules used within the GraalVM compiler. When defining the semantics of a programming…
cs.LO2022★ 1 cited
Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper)
Mark Utting, Brae J. Webb, Ian J. Hayes
We want to verify the correctness of optimization phases in the GraalVM compiler, which consist of many thousands of lines of complex Java code performing sophisticated graph trans…