Formulog: Datalog for SMT-Based Static Analysis
summary
Formulog is a DSL that combines Datalog, an ML-like term fragment, and SMT solving and a prototype runtime implements it. The authors implement three analyses (refinement type checker, bottom-up points-to, symbolic LLVM evaluator) each 1–1.5k LOC, and compare the symbolic evaluator to KLEE and CBMC: exhaustive run times are 27 minutes vs ~3 minutes vs ~3 minutes; goal-directed queries make Formulog faster than KLEE and slightly faster than CBMC. The runtime is naive but automatic parallelization and goal-directed rewrites work and yield practical speedups.
AI-written summary · about
chapters (15)
- 0:00Intro
- 1:13Ex: symbolic evaluation
- 1:40Encoding the input
- 2:18Encoding evaluator state With ML fragment
- 3:23Encoding evaluation
- 6:27Takeaways
- 8:11Datalog + ML + SMT Design in a nutshell
- 8:53Retain power of Datalog
- 9:28Retain power of SMT solving
- 10:17Guarantee safety
- 10:47Prototype Can design be basis of realistic tool?
- 11:09Wrote 3 substantial analyses Each 1-1.5K LOC of Formulog
- 11:38Results are promising
- 12:21Symbolic evaluator comparison On sorting benchmark
- 14:30Formulog Datalog for SMT-Based Static Analysis
related talks
30mAnalyzing Programs with SMT Solvers
53mSemantics-based program manipulation in the age of LLMs
21mTowards Compiler-Guided Static Analysis
13mProgram Analysis via Efficient Symbolic Abstraction
11mFormally Verifying YUL Level Static Analyses and Optimization with Coq
22mOptimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…)
45mLogic Meta Programming for Functional Languages
30mTrustworthy Formal Natural Language Specifications