We demonstrate how infinities improve the expressivity, power, readability, conciseness, and compositionality of a program logic. We prove that adding infinities to Presburger arithmetic enables these improvements without sacrificing decidability. We develop Omega++, a Coq-certified decision procedure for Presburger arithmetic with infinity and benchmark its performance. Both the program and proof of Omega++ are paramaterized over user-selected semantics for the indeterminate terms (such as 0 * \inf).
It is our intention to release a cleaned-up version under a BSD-style license shortly. However, until that time: These proofs and implementation are (c) 2014 All Rights Reserved. Permission granted only to examine these coq proofs and implementation for the purpose of evaluating the paper "Certified Reasoning with Infinity".
Latest Omega++'s virtual machine (all-in-one ~5.6GB) - with SLPAInf Source and prerequisite software pre-installed
Example programs (on the left panel) can be run ONLINE. More example programs and benchmarks can be found in our Download page