Differential Testing of a Verification Framework for Compiler Optimizations (Case Study)
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 transformations. We have built high-level models of the data structures and operations of the code using the Isabelle/HOL theorem prover, and can formally verify the correctness of those high-level operations. But the remaining challenge is: how can we be sure that those high-level operations accurately reflect what the Java is doing? This paper addresses that issue by applying several different kinds of differential testing to validate that the formal model and the Java code have the same semantics. The lessons learned from applying these validation techniques should be applicable to other projects that are building formal models of real-world code.
Sun 14 MayDisplayed time zone: Hobart change
15:45 - 17:15 | |||
15:45 30mPaper | Mutant Equivalence as Monotonicity in Parametric Timed Games FormaliSE 2023 Davide Basile Formal Methods and Tools lab, ISTI-CNR, Pisa, Italy, Maurice ter Beek ISTI-CNR, Pisa, Italy, Hendrik Göttmann Technical University of Darmstadt, Malte Lochau University of Siegen | ||
16:15 30mPaper | Differential Testing of a Verification Framework for Compiler Optimizations (Case Study) FormaliSE 2023 Mark Utting The University of Queensland, Brae J. Webb The University of Queensland, Ian J. Hayes The University of Queensland | ||
16:45 30mPaper | Formalizing Symbolic Execution Path Explosion for Recursive Functions via Asymptotic Path Complexity FormaliSE 2023 Eli Pregerson Harvey Mudd College, Shaheen Cullen-Baratloo Harvey Mudd College, David Chen Harvey Mudd College, Duy Lam Harvey Mudd College, Max Szostak Harvey Mudd College, Lucas Bang Harvey Mudd College |