Seminar Learning in Verification

Seminar in Theoretical CS, Summer 2026

News

  • 10.12.2025: we are online

Dates & Deadlines

TBAKick-off meeting (room 4201b, 2nd floor, building E1, Faculty of CS)
TBATopic preferences due
TBADetailed outline due
TBASeminar report due
TBAPresentation slides due
TBAPresentations (room 4201b, 2nd floor, building E1, CS Department)

Note that the full versions of your report and your slides should be your final submission and the camera-ready versions should differ only with regard to minor remarks, comments, and corrections by your supervisor. Please feel free, however, to talk to your supervisor about submitting preliminary versions before the due dates.

Introduction

  • Slides of introduction (to follow)
  • Topic choice form (to follow)

Overview

The success of machine learning has been motivating researchers in formal methods to adapt learning methods to the verification setting, where correctness guarantees on the result are essential. The aim of this seminar is to provide an overview of approaches to exploit learning methods in verification or to verify systems with learning-based components. This includes, for instance, 

  • the use of learning techniques (e.g., reinforcement learning) for speeding up verification,
  • the use of machine learning data structures and algorithms (e.g. decision trees) for enhancing results of verification (e.g., by generating simple invariants of programs or by generating efficient controllers for reactive systems), 
  • verification of machine-learning artefacts (e.g. verification of neural networks), or
  • the meta-usage of machine learning (e.g. to predict the best tools to be applied to a verification problem).

The setting of the seminar is inspired by an annual workshop of the same name. It covers several areas of computer science which combine learning and verification topics, and which are closely connected to the research fields of the respective supervisors. Each area features a number of topics which are discussed in a scientific journal or conference article. These research articles are the basis on which students have to prepare their report and presentation. The following list gives an overview of the areas that will be covered.

 

Topic Areas (preliminary & incomplete)

A. Verification of Neural Networks [Xaver Fink]

  1. An Abstract Domain for Certifying Neural Networks
  2. Solving Probabilistic Verification Problems of Neural Networks

B. Generation of Invariants [Darion Haase]

  1. Neural Model Checking

C. Controller Synthesis for Partially Observable Stochastic Systems [Alexander Bork, Lisa Pühl]

  1. Strategy Synthesis for Partially Observable Markov Decision Processes

D. Compositional Learning [Hannah Mertens]

  1. Compositional Learning

E. Learning for Software Verification [Thomas Noll]

  1. Detecting and Locating Null Pointer Vulnerabilities
  2. Bisimulation Learning
    • Alessandro Abate, Mirco Giacobbe, Yannik Schnitzer: Bisimulation Learning, CAV 2024
    • Student: –
    • Supervisor: –

Prerequisites

Basic knowledge in the following areas is expected:

  • Formal languages and automata theory
  • Mathematical logic

Previous knowledge in neural networks, stochastic systems and quantum programming (depending on the choice of the topic) is helpful but not mandatory.

Registration

Registration to the seminar is handled via the SuPra system.

Additional Resources

Contact

Thomas Noll