There has been significant progress in automated verification techniques for finite-state systems. One such technique, model-checking, explores the state space of a finite-state system and checks that a desired property is satisfied. While verification of finite-state systems suffers from the well-known state-explosion problem, for infinite-state systems, there is a more serious problem - the decidability problem. For example, it is well-known that it is not possible to automatically verify whether an arithmetic program with two integer variables will halt. We are interested in developing automata-based techniques for proving the decidability (and complexity) of verification queries for infinite-state systems by restricting the properties or the systems that can be verified. In this talk, we describe the use of the decidable properties of automata with "reversal-bounded" counters in verification. We also relate some decidability questions for these machines to the solvability of certain classes of quadratic Diophantine equations.