Formulog: Datalog for SMT-based static analysis
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Nov 13, 2020
- Source ID
- 10.1145/3428209
Entities
People
- Aaron Bembenek
- Michael Greenberg
- Stephen Chong
Organizations
- Defense Advanced Research Projects Agency
- Harvard University
- Pomona College