Satisfiability Modulo Theories (SMT) is a successful automated-
reasoning paradigm that combines boolean satisfiability with theory
reasoning. This talk starts with a "sales pitch." We discuss how modern
SMT solvers work, what they are good at, and what you need to know to
use them as backends in your own research.
In the second part, we discuss the proofs generated by SMT solvers for
unsatisfiable problems.
To allow independent verification, the calculus used in these proofs
should be formally specified and independent of solver implementation
details.
To address this issue, the SMT solver cvc5 uses the novel Eunoia
language designed to simplify the specification of SMT proof calculi
independent of specific solvers.
We present ongoing research in providing a formal, mechanized core for
Eunoia.
