Directed Ramsey Quantifiers with Applications in Formal Verification

• Applicant: Professor Dr. Anthony Lin
• Subject Area: Theoretical Computer Science
• Term: since 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 522843867

The last fifteen years or so have witnessed significant advances in the field of automated reasoning. A problem is modeled as a first-order formula (or fragment thereof) in some logical theory, whose solutions will correspond to satisfying assignments of the formula. Algorithms for finding satisfying solutions to a given formula over logical theories (a.k.a. SMT-solvers, where SMT stands for Satisfiability Modulo Theories) have made such an enormous stride that they have been adopted in industry. Despite the above advances, one important problem remains: how does a problem reduce to satisfiability checking that is amenable to SAT/SMT-solvers? This is in itself a highly challenging and multifaceted question. Our proposal is to investigate the extensions of SMT theories with the so-called directed Ramsey quantifiers. Loosely speaking, a directed Ramsey quantifier allows one to express the existence of a directed infinite clique in the graph defined by a formula. In turn, such quantifiers were shown very recently by the PI and collaborators to have direct applications in liveness verification over infinite-state systems (an important property that has proven to be more difficult to verify in comparison to safety verification) and monadic decomposition (a powerful method in SMT that allows one to deal with richer theories and speed up expensive methods like quantifier elimination). Unfortunately, very few results are available on reasoning about first-order theories (or fragments thereof) containing directed Ramsey quantifiers in the formulas. Our intention is to significantly advance the state-of-the-art of reasoning about first-order theories that allow the use of directed Ramsey quantifers, including foundations (decidability and complexity), tools (integration with SMT-solvers), and transferring these algorithmic insights into actual applications in formal verification including liveness verification and monadic decomposition.

• DFG Programme: Research Grants