FormaliSE 2023
Dates to be announced Melbourne, Australia
co-located with ICSE 2023
Sun 14 May 2023 16:15 - 16:45 at Meeting Room 102 - Testing Chair(s): Cristian Cadar

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 May

Displayed time zone: Hobart change

15:45 - 17:15
TestingFormaliSE 2023 at Meeting Room 102
Chair(s): Cristian Cadar Imperial College London, UK
15:45
30m
Paper
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
30m
Paper
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
30m
Paper
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