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.

翻译：拉姆齐量词最近被提出作为一种统一框架，用于处理程序验证中涉及无限团形式证明的各类性质，这些性质无法在一阶逻辑中表达。其中包括活性验证和一元可分解性等。我们提出了工具REAL，该工具实现了在整数线性算术理论（LIA）、实数线性算术理论（LRA）以及混合情形（LIRA）中高效消除存在性拉姆齐量词的方法。该工具支持便捷的输入格式，这是对前述支持拉姆齐量词的SMT-LIB理论体系的扩展。我们还展示了相较于原始原型的显著加速效果。作为应用实例，我们提供了从FASTer（一种验证无限状态系统可达性的工具）输出格式到我们扩展的SMT-LIB格式的自动转换方案，并展示了本工具如何将FASTer扩展至活性检验领域。