Automatic Synthesis of Data-Flow Analyzers
summary
A tool called DFASy automatically synthesizes intraprocedural, path‑insensitive data‑flow analyzers from a CFG plus expected before/after facts, producing flow direction, meet operator, and transfer functions expressed in a bespoke DSL for transfer functions. Two pruning strategies—abstraction-guided pruning and brevity-guided pruning—cut the search dramatically; DFASy solves 14 benchmark problems (7 classic, 7 custom) in 21.8s on average and is implemented in Java using Soot and Jimple.
AI-written summary · about
chapters (9)
- 0:00Intro
- 1:38Program Synthesis
- 2:05Problem Statement
- 3:49Challenges
- 6:57Example (Reaching Definitions)
- 8:53A DSL for Synthesizing Transfer Functions
- 9:41Search Space Pruning
- 10:54DFASy Algorithm
- 11:55Evaluation
related talks
36mStatic Analysis of APL for Tooling and Compliance
13mMetamorph: Synthesizing Large Objects from Dafny Specifications
22mProgram Synthesis for Artifacts beyond Programs
17mExploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-...
38mStatic Code Analysis - A Behind-the-scenes Look
21mProgram Synthesis From Partial Traces
19mVerifying Dafny Contract Integrity
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools