A Categorical Basis for Robust Program Analysis
summary
A categorical framework characterizes robustness: programs and properties become concrete categories over a base of transformations, and robust analyses become structure-preserving concrete functors. The main theorem gives a lifting recipe that takes a sound, robust analysis on a sub‑Turing model D and produces a sound, robust analysis on general programs C when C admits best abstractions in D. Paper explains why inserting a summing variable breaks a polyhedral bound and why Ultimate Automizer times out when n becomes 4096, shows many loop‑summarization and termination tools are instances of the recipe, and proves algebraic analyses remain robust under loop unrolling and related stuttering simulations.
AI-written summary · about
chapters (7)
- 0:00Motivation for robustness
- 3:05Defining robustness
- 4:53Categorical framework
- 7:30Concrete categories
- 9:54Designing robust analyses
- 13:42Algebraic program analysis
- 16:00Discussion and Q&A
related talks
22mThe Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How t
25mA Semantic Approach to Robust Property Preservation
52mThink Abstractly, Work Concretely
31mNecessity Specifications for Robustness
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
45mA categorical view of computational effects
20mFormal framework for reasoning about the precision of dynamic analysis
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...