## Decision Procedures for Term Algebras with Integer
Constraints

Ting Zhang,
Henny Sipma,
Zohar Manna.
Term algebras can model recursive data structures which are widely
used in programming languages. To verify programs we must be able to
reason about these structures. However, as programming languages
often involve multiple data domains, in program verification decision
procedures for a single theory are usually not applicable. An
important class of \emph{mixed} constraints consists of combinations
of data structures with integer constraints on the size of data
structures. Such constraints can express memory safety properties
such as absence of memory overflow and out-of-bound array access,
which are crucial for program correctness. In this paper we extend
the theory of term algebras with the length function which maps a term
to its size, resulting in a combined theory of term algebras and
Presburger arithmetic. This arithmetic extension provides a natural
but tight coupling between the two theories, and hence the general
purpose combination methods like Nelson-Oppen combination are not
applicable. We present decision procedures for quantifier-free
theories in structures with an infinite constant domain and with a
finite constant domain. We also present a quantifier elimination
procedure for the extended first-order theory that can remove a block
of existential quantifiers in one step.

In *Information and Computation*, volume 204,
pp 1526-1574, October 2006.

Postscript,
PDF
© 2006, Elsevier Inc.

© Henny Sipma /
sipma@cs.stanford.edu