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 Times are displayed in time zone: Tijuana, Baja California change
Wed 26 Jun
Times are displayed in time zone: Tijuana, Baja California change
08:30 - 09:30: Verification IPLDI Research Papers at 229AB Chair(s): Chung-Kil HurSeoul National University | |||
| 08:30 - 08:50 Talk | Semantic Program Alignment for Equivalence Checking PLDI Research Papers Berkeley ChurchillStanford University, Oded PadonStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford University Media Attached | ||
| 08:50 - 09:10 Talk | Verified Compilation on a Verified Processor PLDI Research Papers 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 | Argosy: Verifying Layered Storage Systems with Recovery Refinement PLDI Research Papers 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 | ||