zbMATH — the first resource for mathematics

Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition. (English) Zbl 06916317
Beyersdorff, Olaf (ed.) et al., Theory and applications of satisfiability testing – SAT 2018. 21st international conference, SAT 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer (ISBN 978-3-319-94143-1/pbk; 978-3-319-94144-8/ebook). Lecture Notes in Computer Science 10929, 365-382 (2018).
Summary: Program equivalence checking is a fundamental problem in computer science with applications to translation validation and automatic synthesis of compiler optimizations. Contemporary 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 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 query-decomposition, that allows a more capable 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.
For the entire collection see [Zbl 1390.68015].
68Q25 Analysis of algorithms and problem complexity
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI