Automatic Reasoning Group: Certified Verification with Applications

What it is

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.

Involved groups

When and where

Check the announcements below.

Interested?

To receive updates, please subscribe to the seminar’s mailing list as follows:
Write an email to sympa@informatik.uni-kl.de with subject “subscribe arg-cervera Yourfirstname Yourlastname” and empty message body.
If you have any questions, feel free to contact Pascal Bergsträßer (bergstraesser[at]cs.uni-kl.de).

Next talk

08.08.2024 at 11:00 in room 32-439
- Speaker: Moritz Graf
- Title: Symbolic Computation of Sequential Equilibria
- Abstract:
  The sequential equilibrium is a standard solution concept for extensive-form games with imperfect information. We show how the defining properties of sequential equilibria can be written as a system of polynomial equations and inequalities. By solving this system symbolically, we have built an implementation that can find all sequential equilibria of small games.
- Bio:
  Moritz Graf is a computer science graduate from the University of Freiburg with a background in Mathematics. He is interested in game theory and multi-agent systems with a focus on mathematical proofs and software implementation. He developed the first algorithmic solver for sequential equilibria during his master’s thesis. He is currently living in Bad Dürkheim and looking for an academic research position with the possibility of a PhD.
08.08.2024 at 14:00 in room 32-439
- Speaker: Marco Sälzer
- Title: The Complexity of Formal Reasoning of Neural Network-Based Models
- Abstract:
  The widespread success of neural network-based models has led to their application in various fields, including safety-critical areas. This necessitates the development of sound and complete verification or interpretability methods, collectively referred to as formal reasoning. However, the black-box nature of neural networks obscures in which cases formal reasoning is practically feasible. In this talk, we explore the complexity of decision problems related to formal reasoning of neural network-based models. We begin with classical Feedforward Neural Networks (FNNs), for which the complexity landscape is relatively well-understood. In contrast, for more advanced models like Graph Neural Networks (GNNs) and Transformers, the results are limited. We present first findings showing that there are undecidable cases, highlighting that formal reasoning can only be conducted in carefully restricted settings. We discuss such settings and corresponding complexity bounds, indicating that sound and complete reasoning may be generally intractable. Additionally, we address how some recent characterizations of the expressivity of GNNs and Transformers imply complexity results of formal reasoning, while others do not. We conclude by outlining open questions that must be answered to fully understand the role of formal reasoning in the context of highly expressive neural network-based models.
- Bio:
  Marco Sälzer is a PhD student under the supervision of Prof. Martin Lange, and a member of the Formal Methods / Theoretical Computer Science group at the University of Kassel, Germany. He completed his M.Sc. at the same university, focusing on the (infinite) converging behavior of fixpoint logics. Currently, his research interests lie at the intersection of formal methods and machine learning, with a specific focus on the computational complexity of formal reasoning tasks in various neural network-based models.

Past talks

24.06.2024: Talk by Julian Pasert
- Title: Neural Termination Analysis
19.04.2024: Session consisting of 3 talks:
- Talk 1: Andreea Costea
  - Title: Patch Space Exploration using Static Analysis Feedback
- Talk 2: Matthew Hague
  - Title: Parikh’s Theorem Made Symbolic
- Talk 3: Martin Lester
  - Title: Easily encode problems in SAT With This One Simple Trick: Declarative programming in C using CBMC
03.02.22: Talk by Roland Meyer
- Title: BMC with Memory Models as Input
27.01.22: Talk by Laura Kovács
- Title: Getting Saturated with Induction
09.12.21: Talk by Florin Manea
- Title: Matching Patterns with Variables: A General Framework for Text Processing
02.12.21: Talk by Artur Jeż
- Title: Recompression-based algorithm for word equations
25.11.21: Talk by Julian Gutierrez
- Title: Games, Logic, and Formal Verification
28.10.21: Talk by Alexandra Silva
- Title: Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks
27.05.21: Talk by Yunwen Lei
- Title: Statistical Learning by Stochastic Gradient Descent
20.05.21: Talk by Loris D’Antoni
- Title: Programmable Program Synthesis
22.04.21: Talk by Pablo Barceló
- Title: Explainability Queries for ML Models and its Connections with Data Management Problems
25.03.21: Talk by Oliver Markgraf
- Title: Learning in reactive Synthesis
18.03.21: Talk by Chih-Hong Cheng
- Title: Verification and Validation of DNN-based Autonomy Perception
11.03.21: Talk by Ekaterina Komendantskaya
- Title: Continuous Verification of Machine Learning: a Declarative Programming Approach
25.02.21: Talk by Yutaka Nagashima
- Title: Artificial Intelligence for Inductive Theorem Proving
11.02.21: Talk by Dave Parker
- Title: Verification with Stochastic Games: Advances and Challenges