Disjunctive Interval Analysis
summary
Proposes range decision diagrams (RDDs) as a compact Boxes implementation that avoids constraint substitution and no dependence on a theory solver, and that directly supports non‑linear expressions. Implements RDDs in Crab, adds algorithms for widening, variable hoisting and arithmetic transformers, and compares against LDD‑based Boxes on 190 instances from SVCOMP. RDDs run faster with fewer timeouts/memouts and prove 510 assertions proved out of 628, versus just under 500 (dynamic LDD) and slightly more for static LDD.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:25Why Disjunctive Analysis?
- 1:45The Boxes Abstract Domain
- 2:32Linear Decision Diagrams (LDDs)
- 5:42Range Decision Diagrams (RDDs)
- 6:36RDD Operations
- 7:32Assignments: A Non-Linear Example
- 10:20Variable Hoisting: Calculations
- 11:36Variable Hoisting: Result
- 11:53Evaluation: Benchmarks
- 12:34Evaluation: Analyses Compared
- 13:09Performance: LDDs (Dynamic) vs RDDs
- 13:46Precision: LDDs (Static, Dynamic) and RDDs
- 14:19Summary
related talks
13mDCR Graphs as Co-created Executable Models of the Law
30mUnconstrained Variable Oracles for Faster Static Analyses
28mReasoning about Distributed Reconfigurable Systems
50mRecent Advances in Floating-point (Static) Analyses
33mData-Dependent Confidentiality in DCR Graphs
14mQuantified Underapproximation via Labeled Bunches
49mThe Journey of Box Building
30mAutomatic Inference of Relational Object Invariants