Formulog: Datalog for SMT-Based Static Analysis (Extended Version)

Aaron Bembenek, Michael Greenberg, Stephen Chong

Satisfiability modulo theories (SMT) solving has become a critical part of many static analyses, including symbolic execution, refinement type checking, and model checking. We prop…