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
08:30 - 09:30: PLDI Research Papers - Verification I at 229AB Chair(s): Chung-Kil HurSeoul National University | ||||||||||||||||||||||||||||||||||||||||||
| 08:30 - 08:50 Talk | Berkeley ChurchillStanford University, Oded PadonStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford University Media Attached | |||||||||||||||||||||||||||||||||||||||||
| 08: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 | |||||||||||||||||||||||||||||||||||||||||
| 09: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 | |||||||||||||||||||||||||||||||||||||||||