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.