# Formulog: Datalog for SMT-Based Static Analysis (Extended Version)

arXiv: https://arxiv.org/abs/2009.08361 · HTML: https://mlsanity.com/paper/2009.08361/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Sep 2020.

## Built on by (most cited first, 1 of 1)

- [Defeasible Reasoning via Datalog^neg](https://mlsanity.com/paper/2106.10946/) (2021)

## Abstract (arXiv)

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.