TY - JOUR
T1 - Formulog
T2 - Datalog for SMT-based static analysis
AU - Bembenek, Aaron
AU - Greenberg, Michael
AU - Chong, Stephen
N1 - Publisher Copyright:
© 2020 Owner/Author.
PY - 2020/11/13
Y1 - 2020/11/13
N2 - Satisfiability modulo theories (SMT) solving has become a critical part of many static analyses, including symbolic execution, refinement type checking, and model checking. We propose Formulog, a domain-specific language that 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. Formulog extends the logic programming language Datalog with a first-order functional language and mechanisms for representing and reasoning about SMT formulas; a novel type system supports the construction of expressive formulas, while ensuring that neither normal evaluation nor SMT solving goes wrong. Our case studies demonstrate that a range of SMT-based analyses can naturally and concisely be encoded in Formulog, and that - thanks to this encoding - high-level Datalog-style optimizations can be automatically and advantageously applied to these analyses.
AB - Satisfiability modulo theories (SMT) solving has become a critical part of many static analyses, including symbolic execution, refinement type checking, and model checking. We propose Formulog, a domain-specific language that 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. Formulog extends the logic programming language Datalog with a first-order functional language and mechanisms for representing and reasoning about SMT formulas; a novel type system supports the construction of expressive formulas, while ensuring that neither normal evaluation nor SMT solving goes wrong. Our case studies demonstrate that a range of SMT-based analyses can naturally and concisely be encoded in Formulog, and that - thanks to this encoding - high-level Datalog-style optimizations can be automatically and advantageously applied to these analyses.
KW - Datalog
KW - SMT solving
UR - http://www.scopus.com/inward/record.url?scp=85097575819&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85097575819&partnerID=8YFLogxK
U2 - 10.1145/3428209
DO - 10.1145/3428209
M3 - Article
AN - SCOPUS:85097575819
VL - 4
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
IS - OOPSLA
M1 - 141
ER -