Unconstrained Variable Oracles for Faster Static Analyses
summary
Proposes a lightweight pre-analysis that marks variables likely to be unconstrained and rewrites their assignments to nondeterministic havoc in the Crab IR, implemented as modules in clam/crab. Offers four heuristics (relational vs no-relational oracle, and existential propagation vs universal) and reports simplifying 4–82% of statements (average ~3–4%), average runtime speedup 2.61× with peaks ~8.2%, small precision loss on intervals (~4% of invariants) and retaining ≈90% of polyhedral constraints.
AI-written summary · about
chapters (19)
- 0:00Unconstrained variable oracles intro
- 1:27Core propagation idea
- 3:11Data flow analysis variants
- 6:20Formalizing non-relational oracles
- 8:07Program transformation step
- 14:51Experimental setup and benchmarks
- 17:20AVOC analysis pipeline
- 18:23Statement simplification results
- 20:11Precision loss with intervals
- 20:34Polyhedra domain precision
- 21:18Measured speed-ups
- 22:42Conclusions and future work
- 23:46Q&A: False positives/negatives
- 24:30Q&A: Loops and invariants
- 25:13Q&A: Assignment transformation
- 25:53Q&A: Inter-procedural scope
- 26:38Q&A: Likely-unconstrained variables
- 27:19Q&A: CRAM diff precision
- 28:45Q&A: Octagons domain
related talks
30mAutomatic Inference of Relational Object Invariants
31mGenerating Constraint Programs for Variability Model Reasoning: A DSL and Solver-...
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
23mSpecifying and Verifying Future Conditions
26mTowards Efficient Model Comparison Using Automated Program Rewriting
22mExecution Time Program Verification With Tight Bounds
15mThread-modular Analysis of Release-Acquire Concurrency
20mFormal framework for reasoning about the precision of dynamic analysis