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
equivalence.

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

pldi-2019-papers
08:30 - 09:30: PLDI Research Papers - Verification I at 229AB
Chair(s): Chung-Kil HurSeoul National University
pldi-2019-papers08:30 - 08:50
Talk
Berkeley ChurchillStanford University, Oded PadonStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford University
Media Attached
pldi-2019-papers08:50 - 09:10
Talk
Andreas LööwChalmers University of Technology, Ramana KumarDeepMind, Yong Kiam TanCarnegie Mellon University, USA, Magnus O. MyreenChalmers University of Technology, Sweden, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Oskar AbrahamssonChalmers University of Technology, Sweden, Anthony FoxUniversity of Cambridge, UK
DOI Pre-print Media Attached
pldi-2019-papers09:10 - 09:30
Talk
Tej ChajedMassachusetts Institute of Technology, USA, Joseph TassarottiBoston College, M. Frans KaashoekMassachusetts Institute of Technology, USA, Nickolai ZeldovichMassachusetts Institute of Technology, USA
DOI Pre-print Media Attached