CTL
9 March 2010 - 10h00
Combining Strategy Iteration with Semidefinite Programming for Abstract Interpretation
by Thomas GAWLITZA from verimag
Abstract: We present a practical strategy improvement algorithm for computing least solutions of fixpoint equation systems, whose right-hand sides use order-concave operators and the maximum operator. These equation systems strictly generalize systems of rational equations. We use our algorithm for computing precise numerical invariants of programs by abstract interpretation. Thereby we consider the abstract domain of quadratic zones introduced by Adjé et al. We use an relaxed abstract semantics which is at least as precise as the relaxed abstract semantics used by Adjé et al. Using our strategy improvement algorithm, we are able to compute our relaxed abstract semantics precisely.
