Open Collections

From Local Search to Quantifier Elimination for Bit-Vectors in SMT

Banff International Research Station for Mathematical Innovation and Discovery

Many applications in hardware and software verification rely on Satisfiability Modulo Theories (SMT) solvers for bit-precise reasoning. For solving quantifier-free bit-vector formulas, current state-of-the-art is a technique called bit-blasting, which eagerly translates a given formula into propositional logic (SAT). Bit-blasting is efficient in practice, but may not scale if the input size can not be reduced sufficiently during preprocessing. For quantified bit-vector logics, the majority of solvers employ instantiation-based techniques, which aim to find conflicting ground instances of quantified formulas. For that, it is crucial to select good instantiations for the universal variables, or else the solver may be overwhelmed by the number of ground instances generated. In this talk I will present a complete propagation-based local search approach for quantifier-free bit-vector formulas. It utilizes conditional inverse value computation on concrete assignments for down-propagation. Computing inverse values of bit-vector operators is not always possible, but we can derive conditions that precisely characterize when bit-vector constraints are invertible. We utilized syntax-guided synthesis techniques to aid in establishing these conditions and verified them independently by using several SMT solvers. I will show how such invertibility conditions can be embedded into quantifier instantiations using Hilbert choice expressions.

Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science

video/mp4

Author affiliation: Stanford University

2019-04-06

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/69501

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/