Invited Speakers


  • James Davenport (University of Bath)

    • "SMT Nonlinear Real Arithmetic and Computer Algebra: a Dialogue of the Deaf?"

    At a deep level, the problems which SMT's Nonlinear Real Arithmetic (NRA) and Computer Algebra's Cylindrical Algebraic Decomposition (CAD) wish to solve are the same: nevertheless the approaches are completely different, and are described in different languages. We give an NRA/CAD dictionary, explain the CAD process as it is traditionally presented (and some variants), then ask how NRA and CAD might have a more fruitful dialogue.​

  • Andrew Reynolds (University of Iowa)

    • "Quantifier Instantiation Beyond E-Matching"

    Modern SMT solvers are considered a mature technology for many fragments of quantifier-free constraints, and have recently shown considerable promise as tools for handling quantified constraints as well. Most of the early development in SMT solvers for handling quantified formulas focused on the development of efficient E-matching techniques. This talk surveys some of the recent advances in instantiation-based approaches for quantified formulas in SMT that go beyond E-matching. In particular, we show how approaches based on finding models and conflicts can accelerate the search for (un)satisfiability. We also cover recent techniques for quantified formulas in background theories such as linear arithmetic and bit-vectors, and future challenges in these directions.