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

Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi +2

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,…