zbMATH — the first resource for mathematics

A policy iteration algorithm for computing fixed points in static analysis of programs. (English) Zbl 1081.68616
Etessami, Kousha (ed.) et al., Computer aided verification. 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27231-3/pbk). Lecture Notes in Computer Science 3576, 462-475 (2005).
Summary: We present a new method for solving the fixed point equations that appear in the static analysis of programs by abstract interpretation. We introduce and analyze a policy iteration algorithm for monotone self-maps of complete lattices. We apply this algorithm to the particular case of lattices arising in the interval abstraction of values of variables. We demonstrate the improvements in terms of speed and precision over existing techniques based on Kleene iteration, including traditional widening/narrowing acceleration mecanisms.
For the entire collection see [Zbl 1078.68004].

68Q60 Specification and verification (program logics, model checking, etc.)
68N99 Theory of software
Full Text: DOI