Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)

TL;DR

This paper introduces the tool REAL, which efficiently eliminates Ramsey quantifiers in linear arithmetic theories, enabling advanced program verification tasks like liveness checking with significant speed improvements.

Contribution

The paper presents REAL, a tool for fast Ramsey quantifier elimination in linear arithmetic theories, extending SMT-LIB and enabling applications in liveness verification.

Findings

Substantial speedup over previous prototype

Supports extension of SMT-LIB with Ramsey quantifiers

Enables automatic liveness checking in program verification

Abstract

Ramsey quantifiers have recently been proposed as a unified framework for handling properties of interests in program verification involving proofs in the form of infinite cliques, which are not expressible in first-order logic. Among others, these include liveness verification and monadic decomposability. We present the tool REAL, which implements an efficient elimination of Ramsey quantifiers in existential linear arithmetic theories over integers (LIA), reals (LRA), and the mixed case (LIRA). The tool supports a convenient input format, which is an extension of SMT-LIB over the aforementioned theories with Ramsey quantifiers. We also demonstrate a substantial speedup from the original prototype. As an application, we provide an automatic translation from FASTer (a tool for verifying reachability over infinite-state systems) output format to our extension of SMT-LIB and show how our tool extends FASTer to liveness checking.