2 papers
cs.PL2020
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…
cs.PL2018
FormuLog: Datalog for static analysis involving logical formulae
Aaron Bembenek, Stephen Chong
Datalog has become a popular language for writing static analyses. Because Datalog is very limited, some implementations of Datalog for static analysis have extended it with new la…