Making Formulog Fast: An Argument for Unconventional Datalog Evaluation (Extended Version)

Aaron Bembenek, Michael Greenberg, Stephen Chong

By combining Datalog, SMT solving, and functional programming, the language Formulog provides an appealing mix of features for implementing SMT-based static analyses (e.g., refinem…