A Rule-Based Approach for Designing and Composing Abstract Domains
summary
A rule-based language lets users specify how lattice elements from multiple abstract domains rewrite and combine, so the system generates projection, extent, call/proceed and generalize behaviors automatically; applied to Prolog-style examples (partition/quick-sort) it proves INF/SUP list bounds, multisets and permutation facts. The prototype implements and/or rewriting over pairs of stores, reduces the number of hand-written domain operations, and works functionally but is naive and needs heuristics and performance tuning.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:27Abstract interpretation basics
- 3:33Abstract domains and operations
- 5:42Rapid domain design goals
- 6:24Rule syntax and semantics
- 8:11Rewriting stores with rules
- 10:24Combining stores with rules
- 13:40Fix-point operations with rules
- 16:11Demo: rule-based approach
- 19:47Analysis results for partition
- 20:52Safety properties and permutations
- 21:14Benefits and challenges
- 21:57Future work
- 22:22Q&A
related talks
18mCompiling with Abstract Interpretation
20mThe Lands Platform: Lan.guages and D.omain S.yntax
35mDesigning Domain-Specific Languages: A Comparison of Three Approaches by Example
27mCompositional Embeddings of Domain-Specific Languages
24mThe Best of Abstract Interpretations
34mA Taste of Prolog
51mElpi: rule-based meta-languge for Rocq
35mRestaging Domain-Specific Languages: A Flexible Design Pattern for Rapid Development of(…)