Applications
Because Presburger arithmetic is decidable, automatic theorem provers for Presburger arithmetic exist. (For example, the Coq proof assistant system features a tactic for Presburger arithmetic.) The double exponential complexity of the theory makes it infeasible to use the theorem provers on complicated formulas, but this behavior occurs only in the presence of nested quantifiers: Oppen and Nelson (1980) describe an automatic theorem prover which uses the simplex algorithm on an extended Presburger arithmetic without nested quantifiers. The simplex algorithm has exponential worst-case running time, but displays considerably better efficiency for typical real-life instances. Exponential running time is only observed for specially constructed cases. This makes a simplex-based approach practical in a working system.
Presburger arithmetic can be extended to include multiplication by constants, since multiplication is repeated addition. Most array subscript calculations then fall within the region of decidable problems. This approach is the basis of at least five proof-of-correctness systems for computer programs, beginning with the Stanford Pascal Verifier in the late 1970s and continuing though to Microsoft's Spec# system of 2005.
Read more about this topic: Presburger Arithmetic