FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition

Authors: Shubhani Gupta, Aseem Saxena, Anmol Mahajan and Sorav Bansal

Paper Information

Title:Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Authors:Shubhani Gupta, Aseem Saxena, Anmol Mahajan and Sorav Bansal
Proceedings:SAT Proceedings
Editors: Christoph M. Wintersteiger and Olaf Beyersdorff
Keywords:SMT, Invariants, Counterexample-guided Algorithms, Verification, Compilers, Binary Analysis
Abstract:

ABSTRACT. Program equivalence checking is a fundamental problem in computer science with applications to translation validation and automatic synthesis of compiler optimizations. Modern equivalence checkers employ SMT solvers to discharge proof obligations generated by their equivalence checking algorithm. Equivalence checkers also involve algorithms to infer invariants that relate the intermediate states of the two programs being compared for equivalence. We present a new algorithm, called {\em invariant-sketching} that allows the inference of the required invariants through the generation of counter-examples using SMT solvers. We also present an algorithm, called {\em query-decomposition} that allows effective use of SMT solvers for application to equivalence checking. Both invariant-sketching and query-decomposition help us prove equivalence across program transformations that could not be handled by previous equivalence checking algorithms.

Pages:19
Talk:Jul 12 11:00 (Session 74E: SMT)
Paper: