Abstract acceleration of general linear loops
From MaRDI portal
Abstract: We present abstract acceleration techniques for computing loop invariants for numerical programs with linear assignments and conditionals. Whereas abstract interpretation techniques typically over-approximate the set of reachable states iteratively, abstract acceleration captures the effect of the loop with a single, non-iterative transfer function applied to the initial states at the loop head. In contrast to previous acceleration techniques, our approach applies to any linear loop without restrictions. Its novelty lies in the use of the Jordan normal form decomposition of the loop body to derive symbolic expressions for the entries of the matrix modeling the effect of n>=0 iterations of the loop. The entries of such a matrix depend on through complex polynomial, exponential and trigonometric functions. Therefore, we introduces an abstract domain for matrices that captures the linear inequality relations between these complex expressions. This results in an abstract matrix for describing the fixpoint semantics of the loop. Our approach integrates smoothly into standard abstract interpreters and can handle programs with nested loops and loops containing conditional branches. We evaluate it over small but complex loops that are commonly found in control software, comparing it with other tools for computing linear loop invariants. The loops in our benchmarks typically exhibit polynomial, exponential and oscillatory behaviors that present challenges to existing approaches. Our approach finds non-trivial invariants to prove useful bounds on the values of variables for such loops, clearly outperforming the existing approaches in terms of precision while exhibiting good performance.
Recommendations
- Toward a sound analysis of guarded LTI loops with inputs by abstract acceleration
- Numerical invariants via abstract machines
- A calculus for modular loop acceleration
- Invariant generation through strategy iteration in succinctly represented control flow graphs
- Applying abstract acceleration to (co-)reachability analysis of reactive programs
Cited in
(18)- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
- Backward symbolic execution with loop folding
- Extending abstract acceleration methods to data-flow programs with numerical inputs
- Lower runtime bounds for integer programs
- Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
- ABC: algebraic bound computation for loops
- Applying abstract acceleration to (co-)reachability analysis of reactive programs
- A calculus for modular loop acceleration
- Termination of linear loops over the integers
- Toward a sound analysis of guarded LTI loops with inputs by abstract acceleration
- Termination of linear loops under commutative updates
- Loop summarization with rational vector addition systems
- Invariant relations for affine loops
- Linear loop synthesis for quadratic invariants
- Poles-based invariant generation for verifying the BIBO stability of digital filters
- Satisfiability modulo exponential integer arithmetic
- ParSAT: parallel solving of floating-point satisfiability
- \textsc{Diffy}: inductive reasoning of array programs using difference invariants
This page was built for publication: Abstract acceleration of general linear loops
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408447)
