Wed 26 Jun 2019 08:30 - 08:50 at 229AB - Verification I Chair(s): Chung-Kil Hur

We introduce a robust semantics-driven technique for program
equivalence checking. Given two functions we find a trace
alignment over a set of concrete executions of both programs and
construct a product program particularly amenable to checking

We demonstrate that our algorithm is applicable to challenging
equivalence problems beyond the scope of existing techniques. For
example, we verify the correctness of the hand-optimized vector
implementation of strlen that ships as part of the GNU C
Library, as well as the correctness of vectorization optimizations
for 56 benchmarks derived from the Test Suite for
Vectorizing Compilers.

Wed 26 Jun

Displayed time zone: Tijuana, Baja California change

08:30 - 09:30
Verification IPLDI Research Papers at 229AB
Chair(s): Chung-Kil Hur Seoul National University
Semantic Program Alignment for Equivalence Checking
PLDI Research Papers
Berkeley Churchill Stanford University, Oded Padon Stanford University, Rahul Sharma Microsoft Research, Alex Aiken Stanford University
Media Attached
Verified Compilation on a Verified Processor
PLDI Research Papers
Andreas Lööw Chalmers University of Technology, Ramana Kumar DeepMind, Yong Kiam Tan Carnegie Mellon University, USA, Magnus O. Myreen Chalmers University of Technology, Sweden, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, Oskar Abrahamsson Chalmers University of Technology, Sweden, Anthony Fox University of Cambridge, UK
DOI Pre-print Media Attached
Argosy: Verifying Layered Storage Systems with Recovery Refinement
PLDI Research Papers
Tej Chajed Massachusetts Institute of Technology, USA, Joseph Tassarotti Boston College, M. Frans Kaashoek Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts Institute of Technology, USA
DOI Pre-print Media Attached