Ramsey Quantifiers in First-Order Logic - Complexity and Applications to Verification

Explore the application of Ramsey quantifiers in first-order logic to safety verification and liveness/termination problems in a 30-minute talk by Pascal Bergsträßer from the University of Kaiserslautern-Landau. Delve into the extension of Constrained Horn Clauses (CHC) with Ramsey quantifiers as a more general approach to capturing liveness and termination properties in infinite-state systems. Examine how Ramsey quantifiers assert the existence of infinite cliques in formula-induced graphs and learn about their effective elimination in common SMT theories such as linear integer and real arithmetic. Gain insights into the potential of this approach for advancing verification techniques in various infinite-state systems.