ABSTRACT. On the applications of Constrained Horn Clauses for the verification of software and beyond. (TBD)

ABSTRACT. Z3-Noodler is an automata-based solver for string constraints, based on the Z3 SMT solver. It replaces the string theory implementation of Z3 with a portfolio of decision procedures. In this talk, I will give an overview of the used decision procedures, and present the current state of Z3-Noodler, especially the newly added support for transducer constraints such as str.replace_all and str.replace_re_all.

ABSTRACT. A short talk on the usefulness of user-defined, application-specific decisions in SMT solving and a proposal for a standardization of their specification in SMT-LIB.

ABSTRACT. The optimal solution to a planning task is a sequence of actions with minimal cost that leads from the initial state to a goal state. Optimal planning is PSPACE-complete, and different approaches are used in practice to find an optimal solution. We introduce lower-bound certificates for classical planning tasks, which can be used to prove the optimality of a solution in a way that can be verified by an independent third party. We describe a general framework for generating lower-bound certificates based on pseudo-Boolean constraints, which is agnostic to the planning algorithm used. We also demonstrate how to modify the A∗ algorithm to produce proofs of optimality.

ABSTRACT. Interference-based certification methods for SAT solving, including the de facto standard DRAT, show intriguing and counter-intuitive non-monotonic properties (Wetzler et al. 2014; Järvisalo et al. 2012). In particular, their proof rules depend not only on the claims that were previously derived, but also on *not having derived* some claims, complicating proof composition and trimming (Rebola-Pardo, Suda 2018; Rebola-Pardo 2023).

Recent results, presented at SYNASC this year, show these properties are not inherent to the underlying reasoning, but rather artifacts of the way interference-based proofs are understood and presented (Rebola-Pardo, 2025). Through novel methods that interpret these proofs as programs, monotonicity and compositionality can be recovered.

While this view paves the way for more usable proof formats for SAT and other combinatorial problems, it also suggests a framework to develop hardware and software certification methods, where proofs of programs may carry programs themselves. In this talk, I will explore what kinds of programs and properties this framework can handle.

ABSTRACT. Automata learning has long since excelled in learning behaviour models from black-box systems. For this, a lot of different methods exists, among them, SAT solving can usually be used to exactly infer deterministic automata from a set of execution traces. However, in practice, systems and data sets may not be perfectly deterministic and may often contain faults due to message loss or other environmental factors. We present a method, using partial Max-SAT, to learn deterministic models from noisy execution traces and present current research to apply this to active automata learning as well.