Formulog: Datalog for SMT-based static analysis

Aaron Bembenek, Michael Greenberg, Stephen Chong

Research output: Contribution to journalArticlepeer-review

20 Scopus citations

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.

Original languageEnglish
Article number141
JournalProceedings of the ACM on Programming Languages
Volume4
Issue numberOOPSLA
DOIs
StatePublished - 13 Nov 2020

Keywords

  • Datalog
  • SMT solving

Fingerprint

Dive into the research topics of 'Formulog: Datalog for SMT-based static analysis'. Together they form a unique fingerprint.

Cite this