2025-11-27

Formal verification tooling increasingly relies on logic solvers as backend automated reasoning engines. A commonality among these solvers is the high complexity of their codebases, which makes bug occurrence disturbingly frequent. Tool competitions have showcased many examples of state-of-the-art solvers disagreeing on the satisfiability of logic formulas, be it solvers for Boolean satisfiability (SAT), satisfiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers' results is thus of paramount importance, in order to increase the confidence not only in the solvers themselves, but also in the tooling which they underpin. In this talk, recent advances on the validation of CHC solvers' results will be covered. Two complementary approaches, for the validation of satisfiable and unsatisfiable results, will be presented. The practical impact of result validation will also be discussed. The talk concludes with an outlook on future research.

Fault trees are a widely used and effective risk model for complex systems, answering the question what can go wrong? through minimal cut set analysis. In this talk, we study fault trees from the perspective of Halpern & Pearl's theory of actual causality. This allows us to use fault trees to answer the question why has it gone wrong? We give a complete classification of each of the different notions of actual causality in terms of the fault tree's graph structure and logical structure, and show how minimal cut sets give rise to actual causes. This talk represents joint work with Georgiana Caltais and Mariëlle Stoelinga.

Propositional Dynamic Logic (PDL) is a modal logic for reasoning about the iterative execution of programs. Via the standard translation, PDL can be embedded into Transitive Closure Logic (TCL), an extension of first-order logic with a recursive operator expressing the transitive closure of binary relations. Cyclic proof systems based on Gentzen-style sequents have been developed for both PDL and TCL in the literature, but cyclic proofs for PDL do not directly translate into cyclic proofs for TCL. Therefore, the standard translation does not lift to the level of Gentzen-style cyclic proofs. Motivated by this observation, we introduce a hypersequent-style cyclic proof system for TCL, which enriches Gentzen-style sequents with additional structural connectives. We prove that this system is sound and that it simulates cyclic proofs for PDL, thereby establishing cut-free completeness for a fragment of TCL.

This talk is based on joint work with Anupam Das, published in the Journal of Automated Reasoning

A preprint is available here