View on GitHub

Formulog

Datalog + SMT

Formulog extends the logic programming language Datalog with mechanisms for constructing and reasoning about SMT formulas. In doing so, it makes it possible to write a range of SMT-based static analyses in a way that is both close to their formal specifications and amenable to high-level optimizations and efficient evaluation.

Publications

Formulog: Datalog for SMT-Based Static Analysis (link)
Aaron Bembenek, Michael Greenberg, and Stephen Chong
OOPSLA 2020

Datalog-Based Systems Can Use Incremental SMT Solving (link)
Aaron Bembenek, Michael Ballantyne, Michael Greenberg, and Nada Amin
Extended abstract
ICLP 2020