Formulog: Datalog for SMT-Based Static Analysis (Extended Version)
Abstract
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.
Cite
@article{arxiv.2009.08361,
title = {Formulog: Datalog for SMT-Based Static Analysis (Extended Version)},
author = {Aaron Bembenek and Michael Greenberg and Stephen Chong},
journal= {arXiv preprint arXiv:2009.08361},
year = {2020}
}
Comments
Please cite the official published version of this work: Aaron Bembenek, Michael Greenberg, and Stephen Chong. 2020. Formulog: Datalog for SMT-Based Static Analysis. Proc. ACM Program. Lang. 4, OOPSLA, Article 141 (November 2020), 31 pages. https://doi.org/10. 1145/3428209