Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, Georg Zetzsche

TL;DR

The paper addresses liveness verification for infinite-state systems by extending SMT with Ramsey quantifiers and proposing REAL to eliminate them in existential $\text{LIA}$/$\text{LRA}$/$\text{LIRA}$, yielding formulas that standard SMT solvers can handle. It introduces a solver-agnostic elimination procedure, integrates it with an Alchemist transpiler for Armoise/FASTer outputs, and demonstrates the end-to-end pipeline on liveness benchmarks, achieving significant speedups and more compact encodings. It also provides an SMT-LIB extension for the Ramsey construct, a PySMT integration, and public toolchains that enable practical liveness verification for parameterized distributed protocols. Overall, the work advances scalable liveness checking by enabling efficient Ramsey elimination and seamless interoperability with existing verification stacks.

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.

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

TL;DR

The paper addresses liveness verification for infinite-state systems by extending SMT with Ramsey quantifiers and proposing REAL to eliminate them in existential //, yielding formulas that standard SMT solvers can handle. It introduces a solver-agnostic elimination procedure, integrates it with an Alchemist transpiler for Armoise/FASTer outputs, and demonstrates the end-to-end pipeline on liveness benchmarks, achieving significant speedups and more compact encodings. It also provides an SMT-LIB extension for the Ramsey construct, a PySMT integration, and public toolchains that enable practical liveness verification for parameterized distributed protocols. Overall, the work advances scalable liveness checking by enabling efficient Ramsey elimination and seamless interoperability with existing verification stacks.

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.

Paper Structure

This paper contains 20 sections, 5 equations, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Implemenation
  4. Alchemist
  5. REAL
  6. Benchmarks and Experiments
  7. Pipeline
  8. Sliding Window Protocol:
  9. Lamport’s Bakery Algorithm.
  10. McCarthy 91 Function.
  11. Elimination
  12. Comparison
  13. Conclusion and Future Work
  14. Elimination Formulas
  15. Benchmarks.
  16. ...and 5 more sections

Figures (4)

  • Figure 1: Toolchain
  • Figure 2: Liveness verification results with execution times (left) and formula sizes measured in tree nodes (right)
  • Figure 3: Integer and real elimination times and sizes over selected benchmarks (see \ref{['app:elim_data', 'app:formulas_elim']})
  • Figure 4: Comparison of elimination and solving times (see \ref{['app:comp_data']})