## Decision Procedures for Queues with Integer Constraints

Ting Zhang,
Henny Sipma,
Zohar Manna.
Queues are a widely used data structure in programming languages.
They also provide an important synchronization mechanism in modeling
distributed protocols. In this paper we extend the theory of queues
with the length function that maps a queue to its size, resulting in a
combined theory of queues and Presburger arithmetic. This arithmetic
extension provides a natural but tight coupling between the two
theories, and hence the general Nelson-Oppen combination method for
decision procedures is not applicable. We present a decision
procedure for the quantifier-free theory and a quantifier elimination
procedure for the first-order theory that can remove a block of
existential quantifiers in one step.

In *Proc. Foundations of Software Technology and Theoretical Computer
Science (FSTTCS)*, December 2005, Lecture Notes in Computer Science,
Volume 3821, Springer-Verlag.

Postscript,
PDF.
© 2005, Springer Verlag.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: Nov 19 14:40:50 PDT 2004