VERIMAG
5 mars 2009 - 14h00
Precise Relational Invariants Through Strategy Iteration
par Thomas Gawlitza de Technische Universität München
Abstract: 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 two
linear programming problems for each selected strategy. We apply our
technique to compute the abstract least fixpoint semantics of affine
programs over the interval domain as well as over the relational
domain given through template constraint matrices. In particular, we
thus obtain practical algorithms for computing the abstract least
fixpoint semantics over the zone and octagon abstract domain.
(joint work with Helmut Seidl)
