Despite the abundance of program analyzers and their ever-growing applications in software reliability, validating the correctness of their implementations remains challenging. In fact, such implementations are typically very complex and highly optimized to maximize performance and scalability.
In this talk, I will present two automatic testing approaches for finding correctness issues in core program-analysis components, namely SMT solvers and Datalog engines. Our testing tools found deep, critical issues in several mature solvers and engines. The detected issues may compromise soundness of any program analyzer that builds on these components; in other words, these issues could cause an analyzer to verify incorrect software. Developers of SMT solvers and Datalog engines have praised our techniques as being both practical and effective.