Thomas Martin Gawlitza ; David Monniaux - Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs

lmcs:689 - Logical Methods in Computer Science, September 30, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:29)2012
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow GraphsArticle

Authors: Thomas Martin Gawlitza ; David Monniaux

    We consider the problem of computing numerical invariants of programs, for instance bounds on the values of numerical program variables. More specifically, we study the problem of performing static analysis by abstract interpretation using template linear constraint domains. Such invariants can be obtained by Kleene iterations that are, in order to guarantee termination, accelerated by widening operators. In many cases, however, applying this form of extrapolation leads to invariants that are weaker than the strongest inductive invariant that can be expressed within the abstract domain in use. Another well-known source of imprecision of traditional abstract interpretation techniques stems from their use of join operators at merge nodes in the control flow graph. The mentioned weaknesses may prevent these methods from proving safety properties. The technique we develop in this article addresses both of these issues: contrary to Kleene iterations accelerated by widening operators, it is guaranteed to yield the strongest inductive invariant that can be expressed within the template linear constraint domain in use. It also eschews join operators by distinguishing all paths of loop-free code segments. Formally speaking, our technique computes the least fixpoint within a given template linear constraint domain of a transition relation that is succinctly expressed as an existentially quantified linear real arithmetic formula. In contrast to previously published techniques that rely on quantifier elimination, our algorithm is proved to have optimal complexity: we prove that the decision problem associated with our fixpoint problem is in the second level of the polynomial-time hierarchy.


    Volume: Volume 8, Issue 3
    Published on: September 30, 2012
    Imported on: October 17, 2011
    Keywords: Computer Science - Programming Languages,D.2.4, F.3.1 (D.2.1, D.2.4, D.3.1, E.1), F.3.2 (D.3.1)

    10 Documents citing this article

    Consultation statistics

    This page has been seen 1035 times.
    This article's PDF has been downloaded 496 times.