Paper Info
Title
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
Abstract
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 low 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 Pi(p)(2)-complete. Our procedure mimics a Pi(p)(2) search.
Year
DOI
Venue
2012
10.2168/LMCS-8(3:29)2012
LOGICAL METHODS IN COMPUTER SCIENCE
Keywords
Field
DocType
static program analysis,abstract interpretation,fixpoint equation systems,strategy improvement algorithms,SMT solving
Quantifier elimination,Discrete mathematics,Decision problem,Combinatorics,Control flow graph,Abstract interpretation,Computer science,Static analysis,Operator (computer programming),Invariant (mathematics),Fixed point
Journal
Volume
Issue
ISSN
8
3
1860-5974
Citations 
PageRank 
References 
7
0.56
21
Authors
2
Name
Order
Citations
PageRank
Thomas Martin Gawlitza1886.37
David Monniaux275444.94