Scaling up logico-numerical strategy iteration (extended version).
David P. Monniaux, Peter Schrammel · arXiv (Cornell University) · 2014
Abstract. We introduce an efficient combination of polyhedral analy-sis and predicate partitioning. Template polyhedral analysis abstracts numerical variables inside a program by one polyhedron per control lo-cation, with a priori fixed directions for the faces. The strongest induc-tive invariant in such an abstract domain may be computed by upward strategy iteration. If the transition relation includes disjunctions and ex-istential quantifiers (a succinct representation for an exponential set of paths), this invariant can be computed by a combination of strategy it-eration and satisfiability modulo theory (SMT) solving. Unfortunately, the above approaches lead to unacceptable space and time costs if ap-plied to a program whose control states have been partitioned according to predicates. We therefore propose a modification of the strategy itera-tion algorithm where the strategies are stored succinctly, and the linear programs to be solved at each iteration step are simplified according to an equivalence relation. We have implemented the technique in a proto-type tool and we demonstrate on a series of examples that the approach performs significantly better than previous strategy iteration techniques.