Analyzing Programs with SMT Solvers
summary
Uses Z3 with OCaml bindings and SMTML to compile a tiny IMP language into SMT formulas, generating Z3 with OCaml bindings expressions for literals, variables and operations and emitting assertions that tie SSA-renamed variables across time. Loops become bounded unrolling and SSA with an explicit bound and a fail assertion; verifier returns concrete counterexamples used for synthesis. Works well on small DSLs, embedded ISAs and was scaled experimentally to LLVM IR (project Super).
AI-written summary · about
chapters (10)
- 0:00Introduction to SMT solvers
- 1:31Satisfiability and structure
- 4:58Analyzing programs with SMT
- 7:46Formula compilation foundation
- 10:20Compiler construction logic
- 13:20Mapping interpreter to compiler
- 17:10Compiling commands and flow
- 20:16Control flow in SMT
- 21:59Advanced verification applications
- 25:09Real-world use cases and summary
related talks
21mTowards Compiler-Guided Static Analysis
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
18mCompiling with Abstract Interpretation
35mThe Mastermind behind Refinement Types
32mSatisfiability Modulo Custom Theories in Z3 (Tool Paper)
09mRetargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
46mMechanizing Abstract Interpretation
35mA Peek Inside SAT Solvers