SPLASH 2020 (series) / OOPSLA /
Counterexample-Guided Correlation Algorithm for Translation Validation
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
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.
Mon 16 Nov Times are displayed in time zone: Central Time (US & Canada) change
Mon 16 Nov
Times are displayed in time zone: Central Time (US & Canada) change
15:00 - 16:20: M-5OOPSLA at SPLASH-I +12h Chair(s): Leonidas LampropoulosUniversity of Maryland, College Park, Jonathan AldrichCarnegie Mellon University | |||
15:00 - 15:20 Talk | CAMP: Cost-Aware Multiparty Session Protocols OOPSLA Link to publication DOI Media Attached | ||
15:20 - 15:40 Talk | Counterexample-Guided Correlation Algorithm for Translation Validation OOPSLA Link to publication DOI Media Attached | ||
15:40 - 16:00 Talk | Multiparty Motion Coordination: From Choreographies to Robotics Programs OOPSLA Link to publication DOI Media Attached | ||
16:00 - 16:20 Talk | On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers OOPSLA Link to publication DOI Media Attached |
Tue 17 Nov Times are displayed in time zone: Central Time (US & Canada) change
Tue 17 Nov
Times are displayed in time zone: Central Time (US & Canada) change
03:00 - 04:20: M-5OOPSLA at SPLASH-I Chair(s): Bernardo ToninhoNova University of Lisbon / NOVA-LINCS, Xiangzhe XuNanjing University | |||
03:00 - 03:20 Talk | CAMP: Cost-Aware Multiparty Session Protocols OOPSLA Link to publication DOI Media Attached | ||
03:20 - 03:40 Talk | Counterexample-Guided Correlation Algorithm for Translation Validation OOPSLA Link to publication DOI Media Attached | ||
03:40 - 04:00 Talk | Multiparty Motion Coordination: From Choreographies to Robotics Programs OOPSLA Link to publication DOI Media Attached | ||
04:00 - 04:20 Talk | On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers OOPSLA Link to publication DOI Media Attached |