tools-only Interval Analysis Techniques
Overview
Interval analysis is a static program analysis technique that computes safe approximations of the possible values that variables can take during program execution.
Fundamental Concepts
What is an Interval?
An interval is a continuous range of values represented as [min, max] where:
min: Lower bound (inclusive)max: Upper bound (inclusive)
Examples:
[0, 10]: Values from 0 to 10[-5, 5]: Values from -5 to 5[3.14, 3.14]: Single value (constant)[-∞, ∞]: Any value (unknown)
Interval Arithmetic
Operations on intervals produce result intervals:
Addition: [a, b] + [c, d] = [a+c, b+d]
[1, 3] + [2, 4] = [3, 7]
Subtraction: [a, b] - [c, d] = [a-d, b-c]
[5, 10] - [1, 3] = [2, 9]
Multiplication: [a, b] × [c, d] = [min(ac,ad,bc,bd), max(ac,ad,bc,bd)]
[2, 3] × [4, 5] = [8, 15]
[-1, 2] × [3, 4] = [-4, 8]
Division: [a, b] / [c, d] (if 0 ∉ [c, d])
[6, 12] / [2, 3] = [2, 6]
Analysis Methods
1. Static Interval Analysis
Compute intervals without executing the program.
Approach:
- Parse program into AST
- Initialize intervals for inputs
- Propagate intervals through operations
- Handle control flow (branches, loops)
- Compute fixed points for loops
Example:
def analyze(x):
# x: [0, 10] (given)
y = x + 5
# y: [0, 10] + [5, 5] = [5, 15]
z = y * 2
# z: [5, 15] × [2, 2] = [10, 30]
return z
Advantages:
- No execution needed
- Sound over-approximation
- Complete coverage
Limitations:
- May be imprecise
- Conservative estimates
- Difficult for complex code
2. Dynamic Interval Analysis
Observe actual value ranges during execution.
Approach:
- Instrument program to log values
- Run with test inputs
- Track min/max observed values
- Build interval database
Example:
# Instrumented code
def process(x):
log_value('x', x) # Log x
y = x * 2
log_value('y', y) # Log y
return y
# After running tests with x ∈ {1, 5, 10}:
# x: [1, 10] (observed)
# y: [2, 20] (observed)
Advantages:
- Precise for tested paths
- Easy to implement
- Reflects actual behavior
Limitations:
- Requires test suite
- Incomplete coverage
- Only observes tested values
3. Hybrid Analysis
Combine static and dynamic analysis.
Approach:
- Run dynamic analysis to get concrete intervals
- Use static analysis to extend coverage
- Refine static intervals with dynamic observations
- Validate static results with dynamic tests
Benefits:
- Better precision than pure static
- Better coverage than pure dynamic
- Validates static analysis results
Handling Control Flow
Conditional Branches
Refine intervals based on conditions:
x = [0, 100] # Initial interval
if x > 50:
# In this branch: x ∈ [51, 100]
y = x - 50
# y ∈ [1, 50]
else:
# In this branch: x ∈ [0, 50]
y = x + 50
# y ∈ [50, 100]
# After merge: y ∈ [1, 100]
Loops
Compute fixed points for loop variables:
x = 0 # x: [0, 0]
while x < 10:
# Iteration 1: x ∈ [0, 0]
# Iteration 2: x ∈ [0, 1]
# Iteration 3: x ∈ [0, 2]
# ...
# Fixed point: x ∈ [0, 10]
x = x + 1
# After loop: x ∈ [10, 10]
Widening: Accelerate convergence for complex loops:
If interval grows, widen to ∞:
[0, 10] → [0, 20] → [0, ∞]
Narrowing: Refine after fixed point:
Use loop condition to narrow:
[0, ∞] with condition x < 100 → [0, 99]
Advanced Techniques
Relational Analysis
Track relationships between variables:
x = [0, 10]
y = x + 5
# Relation: y = x + 5
# If x = 3, then y = 8 (not just y ∈ [5, 15])
Symbolic Intervals
Use symbolic bounds:
def process(n):
# n: [0, N] where N is symbolic
x = [0, n]
# x: [0, N]
y = x * 2
# y: [0, 2N]
Modular Intervals
Track values modulo some number:
x = [0, 100]
y = x % 10
# y: [0, 9] (modular arithmetic)
Precision vs. Performance
Precision Techniques
Narrower intervals (more precise):
- Path-sensitive analysis
- Relational analysis
- Symbolic execution
- SMT solvers
Cost: Higher computational complexity
Performance Techniques
Wider intervals (less precise):
- Flow-insensitive analysis
- Widening operators
- Abstract interpretation
- Simple interval arithmetic
Benefit: Faster analysis
Practical Applications
1. Overflow Detection
Check if intervals exceed type bounds:
# int32 range: [-2147483648, 2147483647]
x = [1000000, 2000000]
y = [1000000, 2000000]
z = x * y
# z: [1000000000000, 4000000000000]
# Overflow! Exceeds int32 max
2. Array Bounds Checking
Verify array indices are valid:
arr = [0] * 100 # Length 100
index = [0, 150] # Potential out of bounds!
# WARNING: index may exceed array length
3. Division by Zero
Detect potential division by zero:
x = [1, 10]
y = [-5, 5] # Contains 0!
z = x / y
# ERROR: Division by zero possible
4. Test Case Generation
Generate boundary test cases:
# Interval: x ∈ [0, 100]
# Test cases: 0, 1, 50, 99, 100
Implementation Considerations
Representation
Concrete intervals: [3, 7]
- Exact bounds
- Efficient operations
Symbolic intervals: [0, N]
- Parametric bounds
- More expressive
Floating-point intervals: [3.14, 3.15]
- Rounding considerations
- Precision issues
Soundness
Sound analysis: Never underestimates possible values
- May report false positives
- Safe for verification
Unsound analysis: May miss some values
- Fewer false positives
- Not safe for verification
Completeness
Complete analysis: Finds all possible values
- May be imprecise
- Conservative approximation
Incomplete analysis: May miss some values
- More precise
- Requires validation
Tools and Libraries
Python
- PyInterval: Interval arithmetic library
- Z3: SMT solver with interval support
- Pyta: Static analysis with intervals
C/C++
- APRON: Numerical abstract domains
- Frama-C: Static analyzer with value analysis
- CBMC: Bounded model checker
Java
- Soot: Program analysis framework
- WALA: Static analysis library
- Checker Framework: Pluggable type systems
Best Practices
- Start with dynamic analysis: Get concrete intervals from tests
- Use static analysis for coverage: Extend to untested paths
- Validate results: Check intervals against expected behavior
- Focus on critical variables: Prioritize safety-critical code
- Document assumptions: Record input interval assumptions
- Iterate and refine: Improve precision incrementally
- Automate analysis: Integrate into CI/CD pipeline
Common Pitfalls
Over-approximation
Problem: Intervals too wide to be useful
x = [0, ∞] # Too imprecise!
Solution: Use more precise analysis or add constraints
Under-approximation
Problem: Missing possible values
# Actual: x ∈ [0, 100]
# Computed: x ∈ [0, 50] # Missing values!
Solution: Use sound analysis techniques
Ignoring Overflow
Problem: Not checking type bounds
x = [1000000, 2000000]
y = x * x # Overflow not detected!
Solution: Always check against type limits
Imprecise Loop Analysis
Problem: Widening too aggressively
# Loop: for i in range(10)
# Computed: i ∈ [0, ∞] # Too wide!
Solution: Use narrowing or better loop analysis
References
- Cousot, P., & Cousot, R. (1977). "Abstract interpretation: a unified lattice model"
- Miné, A. (2006). "The octagon abstract domain"
- Blanchet, B., et al. (2003). "A static analyzer for large safety-critical software"