Omega++: Certified Reasoning with Infinity

By Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor and Wei-Ngan Chin

Omega++'s Overview

SPLAInf

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".

Downloads

Latest Omega++'s virtual machine (all-in-one ~5.6GB) - with SLPAInf Source and prerequisite software pre-installed

Omega++ (Technical Report)

Coq Proofs and Implementation (including .vo files)

Coq Documentation

Example programs

Example programs (on the left panel) can be run ONLINE. More example programs and benchmarks can be found in our Download page