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