Formulog: Datalog for SMT-based Static Analysis
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.
Fri 22 OctDisplayed time zone: Central Time (US & Canada) change
13:50 - 15:10
|Gradual Verification of Recursive Heap Data Structures|
|Formulog: Datalog for SMT-based Static Analysis|
|Compiling Symbolic Execution with Staging and Algebraic Effects|
|Automated Policy Synthesis for System Call Sandboxing|
Shankara Pailoor University of Texas at Austin, Xinyu Wang University of Michigan, Hovav Shacham University of Texas at Austin, Isil Dillig University of Texas at AustinDOI
|Discussion, Questions and Answers|