Accelerated Data-Flow Analysis
arXiv:0812.2011 · doi:10.1007/978-3-540-74061-2_12
Abstract
Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states. Even if no termination guarantee is provided in theory, successful results were obtained in practice by different tools implementing this framework. In this paper, the acceleration framework is extended to data-flow analysis. Compared to a classical widening/narrowing-based abstract interpretation, the loss of precision is controlled here by the choice of the abstract domain and does not depend on the way the abstract value is computed. Our approach is geared towards precision, but we don't loose efficiency on the way. Indeed, we provide a cubic-time acceleration-based algorithm for solving interval constraints with full multiplication.
Cited by in corpus (6)
- Automatic Modular Abstractions for Template Numerical Constraints
- Improving Strategies via SMT Solving
- Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs
- Transfer Function Synthesis without Quantifier Elimination
- Abstract Fixpoint Computations with Numerical Acceleration Methods
- Convex Hull of Arithmetic Automata