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

  • Online via Zoom
  • Date and time: Thursdays 13:00
  • Check the schedule below for exact dates.
  • A longer-term plan can be found in this Google Calendar.


  • To get the Zoom link of the next talks, please subscribe to the seminar's mailing list as follows:
  • Write a mail 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

  • 27.05.21: Talk by Yunwen Lei
    • Title: Statistical Learning by Stochastic Gradient Descent
    • Abstract:
      Stochastic gradient descent (SGD) has become the workhorse behind many machine learning problems. Optimization and sampling errors are two contradictory factors responsible for the statistical behavior of SGD. In this talk, we report our generalization analysis of SGD by considering simultaneously the optimization and sampling errors. We remove some restrictive assumptions in the literature and significantly improve the existing generalization bounds. Our results help to understand how to stop SGD early to get a best statistical behavior.
    • Bio:
      Dr. Yunwen Lei got his PhD degree from Wuhan University in 2014. He is now a Lecturer at School of Computer Science, University of Birmingham. Previously, he was a Humboldt Research Fellow at University of Kaiserslautern, a Research Assistant Professor at Southern University of Science and Technology, and a Postdoctoral Research Fellow at City University of Hong Kong. Dr. Lei's research interests include learning theory and optimization. He has published papers in ICML, NeurIPS, ICLR and some prestigious journals including IEEE Transactions on Information Theory and Journal of Machine Learning Research.

Past talks

  • 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