Formulog
Datalog + SMT + FP for writing SMT-based static analyses
Formulog ties together the logic programming language Datalog and off-the-shelf SMT solvers. It is designed for writing SMT-based static analyses in a way that is both close to their formal specifications, and amenable to high-level optimizations and efficient evaluation.