Logico-Numerical Max-Strategy Iteration⋆

Abstract. Strategy iteration methods are used for solving fixed point equations. It has been shown that they improve precision in static anal-ysis based on abstract interpretation and template abstract domains, e.g. intervals, octagons or template polyhedra. However, they are limited to numerical programs. In this paper, we propose a method for apply-ing max-strategy iteration to logico-numerical programs, i.e. programs with numerical and Boolean variables, without explicitly enumerating the Boolean state space. The method is optimal in the sense that it com-putes the least fixed point w.r.t. the abstract domain; in particular, it does not resort to widening. Moreover, we give experimental evidence about the efficiency and precision of the approach