Title: Automatic BlackBox Equivalence Checking

Speaker: Sorav Bansal    (bio) (bio)

Sorav Bansal is an Associate Professor and Microsoft Chair Professor at the CS department at IIT Delhi, and works in the areas of programming languages and operating systems. His primary research interests involve investigating superoptimization-based compiler design. His research papers have appeared at PLDI, ASPLOS, SOSP, OSDI, OOPSLA, SAT, etc. Sorav obtained his B.Tech. from IIT Delhi, and Ph.D. from Stanford University.

When: Tuesday, 07 September 2021 at 1900 hrs (IST)  

Abstract:
Several important verification problems can be cast as equivalence checking problems. A large number of these equivalence proofs can be completed through bisimulation relation constructions. I will present our recently proposed algorithm, called Counter, to automatically compute equivalence (bisimulation) proofs across two programs, potentially written in different syntaxes, without prior knowledge of the exact differences between the two programs (blackbox). Counter has been successfully used to validate translations of C programs to highly optimized x86 assembly generated through modern compilers. Counter has also been used to verify C library implementations. Through our experiments, we have automatically generated proofs across complex compiler transformations and found several bugs in popular open source programs and general-purpose compilers. I will also briefly discuss the subtleties of checking equivalence for LLVM programs. Finally I will outline our recent efforts at automatic verification of C programs through the Counter algorithm.

This talk will be based on work published at APLAS 2017, HVC 2017, SAT 2018, PLDI 2020, and OOPSLA 2020. It will also include some of our ongoing work.