Sun 15 - Sat 21 November 2020 Online Conference
Mon 16 Nov 2020 15:20 - 15:40 at SPLASH-I - M-5 Chair(s): Leonidas Lampropoulos, Jonathan Aldrich
Tue 17 Nov 2020 03:20 - 03:40 at SPLASH-I - M-5 Chair(s): Bernardo Toninho, Xiangzhe Xu

Automatic translation validation across the unoptimized
intermediate representation (IR) of the original source code
and the optimized executable assembly code is a desirable
capability, and has the potential to compete with existing approaches
to verified compilation such as CompCert.
A difficult subproblem is the automatic
identification of the correlations across the transitions between
the two programs' respective locations.
We present a counterexample-guided
algorithm to identify these correlations in a robust and
scalable manner. Our algorithm
has both theoretical and empirical advantages over prior work
in this problem space.