Presentation at SYNCHRON'12
Policy Iterations as Traditional Abstract Domains
Pierre Roux, ONERA
Among precise abstract interpretation methods developed during the last
decade, policy iterations is one of the most promising. Despite its
efficiency, it has not yet seen a broad usage in static analyzers. We
believe the main explanation to this restrictive use, beside the novelty
of the technique, lies in its lack of integration in the traditional
abstract domain framework. This prevents an easy integration in existing
static analyzers based on the classical abstract interpretation
framework and collaboration with other, already implemented, abstract
domains through reduced product. This paper aims at providing a
traditional abstract domain interface to policy iterations. Usage of semi-definite programming to infer quadratic invariants on
linear systems is one of the most appealing use of policy iteration.
Combined with a template generation heuristic inspired from existing
methods from control theory, this gives a fully automatic abstract
domain to infer quadratic invariants on linear systems with guards.
Those systems often constitute the core of embedded control systems and
are hard, when not impossible, to analyze with traditional linear
abstract domains. The method has been implemented and applied to some
benchmark systems, giving good results.