Abstract:

The theory of quantifier-free Presburger arithmetic (integer linear arithmetic) has many applications in software analysis and hardware verification. In this talk, I will describe a new decision procedure for quantifier-free Presburger arithmetic that is designed to exploit the special structure of formulas commonly occurring in software verification; viz, that most linear constraints are separation (difference-bound) constraints, and the non-separation constraints are sparse.

The decision procedure is based on the following property of quantifier-free Presburger arithmetic: If there is a satisfying solution to a formula F, then there is one whose size, measured in bits, is polynomially bounded in the size of F. We derive a new solution bound in terms of parameters characterizing the sparseness of linear constraints and the number of non-separation constraints, in addition to traditional measures of formula size. Our decision procedure encodes integer variables in the formula as bit-vectors taking values within the bound, thus generating an equi-satisfiable Boolean encoding that is checked using a Boolean satisfiability solver. Experimental results indicate that this method can greatly outperform other decision procedures.

This is joint work with Randy Bryant, and will appear at LICS'04.