The focus of the seminar series is to build a bridge between research groups in Kaiserslautern with interests in formal verification, machine learning, distributed systems, and embedded systems, oriented towards the topic of certified verification. The past decades have seen the rise of powerful methods in formal verification and machine learning, including SAT and SMT-solvers, deep neural networks, program synthesis, and property-directed reachability (IC3), to mention a few. Such techniques, as well as the optimizations that are applied to increase scalability and applicability, often become so complex that bugs in those implementations start to creep in. We are interested in techniques that can ensure correctness in those implementations, including certified solvers, certified verifiers, and type systems, among others. The aim of the seminar series is to exchange ideas that could lead to the development of such techniques.
In the word equations problem, we are given two sequences consisting of letters and variables, and we are asked to decide whether there exists a substitution for the variables that turns the equation into a true equality of strings. This setting is often extended with regular constraints, which restrict the possible substitution for a given variable to some regular language. We extend this setting with a directed version of Ramsey quantifiers, which express the existence of an infinite directed clique. Given a formula over word equations (with regular constraints) α(X→, Y→), where X→ and Y→ are two equal-length sequences of variables, we ask whether there exists an infinite sequence S→₁, S→₂, …, S→ₙ, … such that α(S→ᵢ, S→ⱼ) holds for each i < j. Here, the formula α may use conjunction, disjunction, and negation, and is quantifier-free. Ramsey quantifiers are generally introduced into theories to reason about the well-foundedness of relations and, in practical terms, about program termination. We show that this problem is in PSPACE, i.e., in the same complexity class as the currently best algorithms for the satisfiability of word equations.
This is a work-in-progress talk.
Time: 16.12.2025 , 10:45 - 11:15
Speaker: Kilian Lichtner
Title: REAL: Ramsey Elimination for Arithmetic Logics
Abstract:
Ramsey Quantifiers extend first-order logic and have emerged as a powerful tool for expressing properties in program verification, including liveness and monadic decomposability, which involve reasoning about infinite cliques. Previous work by Bergsträßer et al. proposed an elimination procedure for Ramsey Quantifiers in linear arithmetic, but its prototype implementation was limited in scope and efficiency. We introduce REAL—Ramsey Elimination for Arithmetic Logics—a fully integrated tool for efficient elimination of Ramsey Quantifiers, over existential linear arithmetic theories on integers, reals, and mixed domains. REAL extends SMT-LIB with Ramsey Quantifiers and is built on the PySMT framework, enabling elimination as a direct SMT-LIB(+Ramsey) to SMT-LIB translation. This modular design ensures compatibility with existing SMT solvers while achieving substantial performance improvements over the original prototype. As a case study, we transpile reachability relations generated by FASTer, a tool for analyzing infinite counter systems, into SMT-LIB using our new tool Alchemist. This allows us to then pose liveness questions using the Ramsey Quantifier, which is subsequently eliminated. Integrating FASTer with REAL’s elimination pipeline provides an efficient workflow for verifying liveness properties in various counter systems.
Time: 16.12.2025 , 11:15 - 11:45
Speaker: Annika Delb
Title: Reachability in Power-Word Compressed Pushdown Systems
Abstract:
Compressed automata provide compact representations of exponentially long computations, yet many of their algorithmic properties remain open. This talk focuses on reachability in power-word compressed pushdown systems, where transitions may be labeled with expressions of the form u^k, with u a word over the stack alphabet and k given in binary. This setting generalizes reachability in succinct one counter systems, known to be NP-complete. I present techniques for analyzing power-compressed computations and determine the exact complexity of their reachability problem. I also discuss surrounding decision problems in compressed automata and outline open questions in this area.
Time: 16.12.2025 , 11:45 - 12:15
Speaker: Heyang Li
Title: Answering Constraint Path Queries over Graphs
Abstract:
Constraints are powerful declarative constructs that allow users to conveniently restrict variable values that potentially range over an infinite domain. In this paper, we propose a constraint path query language over property graphs, which extends Regular Path Queries (RPQs) with SMT constraints on data attributes in the form of equality constraints and Linear Real Arithmetic (LRA) constraints. We provide efficient algorithms for evaluating such path queries over property graphs, which exploits optimization of macro-states (among others, using theory-specific techniques). In particular, we demonstrate how such an algorithm may effectively utilize highly optimized SMT solvers for resolving such constraints over paths. We implement our algorithm in MillenniumDB, an open-source graph engine supporting property graph queries and GQL. Our extensive empirical evaluation in a real-world setting demonstrates the viability of our approach.
Past talks:
08.08.2024: Talk by Marco Sälzer
- Title: The Complexity of Formal Reasoning of Neural Network-Based Models
08.08.2024: Talk by Moritz Graf
- Title: Symbolic Computation of Sequential Equilibria