Thomas Gawlitza and Helmut Seidl. Precise Relational Invariants Through Strategy Iteration. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, volume 4646 of Lecture Notes in Computer Science, pages 23-40, Lausanne, Switzerland, September 2007. Springer.

We present a practical algorithm for computing exact least solutions of systems of equations over the rationals with addition, multiplication with positive constants, minimum and maximum. The algorithm is based on strategy improvement combined with solving linear programming problems for each selected strategy. We apply our technique to compute the abstract least fixpoint semantics of affine programs over the relational template constraint matrix domain [20]. In particular, we thus obtain practical algorithms for computing the abstract least fixpoint semantics over the zone and octagon abstract domain.

Download: PDF Reference: Bibtex The original publication is available at