Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols

We study a class of extended automata defined by guarded commands over Presburger arithmetic with uninterpreted functions. On the theoretical side, we show that the bounded reachability problem is decidable in this model. On the practical side, the class is useful for modeling programs with unbounded data structures, and the reachability procedure can be used for symbolic simulation, testing, and verification.