Title: Automatic BlackBox Equivalence Checking
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.