The ability to algorithmically decide whether a given formula has a model is valuable to many areas of compiler construction and formal verification. It allows one to automatically prove that a given code optimization is sound to detect unintentional overflows and highlight other potential defects in a given program. Decision procedures are an active research area, and their implementations are being employed in the industry, e.g., to reason about the correctness of the configuration of critical infrastructure. This talk focuses on a decision procedure for the first-order theory of integers with addition (so-called Presburger arithmetic) based on the formal finite automata model.
(to be continued in PDF)