Building Better SMT Solvers using Syntax-Guided Synthesis

by Andrew Reynolds

Abstract
Satisfiability Modulo Theories (SMT) solvers have gained widespread popularity as reasoning engines in numerous formal methods applications, including in syntax-guided synthesis (SyGuS) applications. Previous work has also shown that SMT solvers, notably CVC4, can act as efficient stand-alone synthesis solvers.
In this talk, we focus on a emerging class of applications for syntax-guided synthesis, namely, the use of a SyGuS solver to (partially) automate further development and improvements to the solver itself. We describe several recent features in the SMT solver CVC4 that follow this paradigm. These include syntax-guided enumeration of rewrite rules, selection of test inputs, and discovery of solved forms for quantified constraints. For the latter, we describe how syntax-guided synthesis recently played a pivotal role in the development of a new algorithm for quantified bit-vector constraints based on invertibility conditions, and how this technique can be extended for similar algorithms that target quantified constraints in other theories, including the theory of floating points.

Bio
Andrew Reynolds is a research scientist at the University of Iowa, and one of the lead developers of the Satisfiability Modulo Theories (SMT) solver CVC4. His research spans various aspects of SMT solving, including approaches for (syntax-guided) synthesis conjectures, unbounded strings and regular expressions, and first-order theorem proving. His work in CVC4 has entered numerous competitions and has received awards spanning several automated reasoning communities, including SMT, automated theorem proving, and syntax-guided synthesis.

More information