Synthesizing Abstract Transformers
summary
Method synthesizes an abstract transformer from (i) a concrete semantics for op, (ii) an abstract domain A, and (iii) a DSL L, producing an AMURTH output that is a most-precise L-transformer when expressible. Algorithm runs a dual counterexample-guided loop: one loop generates soundness counterexamples, the other precision counterexamples, and the synthesizer shrinks candidates to satisfy both. Implementation replaces manual transformers in two analyzers with matching analysis performance and uncovers four existing unsound transformers found in prior engines.
AI-written summary · about
chapters (14)
- 0:00Start
- 0:22Abstract Interpretation
- 1:05Abstract Transformer
- 2:45Motivation
- 3:49Challenges
- 4:29Best L-transformer
- 5:17Problem statement (revised)
- 6:13Who cares?
- 6:59Algorithm Overview
- 9:59AMURTH in action!
- 13:22Evaluation: Domains and Operations
- 14:11Evaluation: Methodology
- 14:40Comparison with manual operations
- 19:39Conclusions
related talks
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
22mSAIL: Sound Abstract Interpreters with LLMs
20mOptimal Program Synthesis via Abstract Interpretation
14mSynthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE(…)
30mFormal Metatheory of Second-Order Abstract Syntax
31mLetting users do the undecidable: lessons from program synthesis
18mCompiling with Abstract Interpretation
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)