Logic and Verification Seminar (Winter 2021)

The Logic and Verification seminar is a reading group gathering the members of the Automatic Reasoning AG and students interested in formal methods. In this semester, we are looking at the diverse applications of formal methods in the design and verification of software systems.

The seminar is open both for Bachelor and Master students.

As a student

Your main role is to attend the weekly sessions, and contribute to the discussions. Each session consists in either:

a presentation of an article or an ongoing research by a member of the group followed by some questions and discussions, or
a discussion about students’ reading progress.

As a student, you will read a scientific paper in logic and verification, summarize it in a report, and present it. There will be several possible topics (see below). To help you with these tasks, a researcher of our group will be assigned to you to supervise you and provide advice both for your presentation and your report.

Some important dates:

Paper selection deadline: 03.12.21
Report submission deadline: 11.03.22

note: some details are yet to be finalised, but expected to be done in the next several days. If you have any questions, feel free to drop Shuanglong (shuanglong@cs.uni-kl.de) an email.

When and where

Schedule and location:

Room: Offline (13-370) or Online (via OLAT/BBB: follow this link). A confirmation email will be sent out beforehand.
Date and time: Friday 14:00 to 15:30
Kickoff meeting: Friday 29.10.21 14:00 - 15:00 via OLAT/BBB: follow this link
Periodicity: weekly (default, unless announced otherwise)
Registration: send a mail to shuanglong@cs.uni-kl.de with your name and matriculation number

Available topics

The topics covered include, but are not limited to, the following:

String Constraint Solver
Concrete Semantics for Programming Languages
Modal and Temporal Logics
Model Checking
Computational Aspects of Game Theory
Games and Automata for Verification
Specification and Verification of Finite and Infinite-State Systems
Synthesis

List of suggested papers can be found here

Instructors

Prof. Anthony Lin
Dr. Shuanglong Kan

Planned sessions

05.11.2021, 14:15 ~ 15:15: by Najib, title: Rational Verification for Probabilistic Systems
12.11.2021, 14:00 ~ 15:00: by Shuanglong, title: An Introduction to string solvers Slide Download
19.11.2021, 13:00 ~ 14:00: paper selection
25.11.2021, 13:00 ~ 14:00: by Julian Gutierrez, title: Games, Logic, and Formal Verification
29.11.2021, 14:00 ~ 15:00: by Pascal Bergsträßer, title: Automatic Structures
03.12.2021, 14:00 ~ 15:00. Paper reading discussion
09.12.2021, 14:00 ~ 15:00. Paper reading discussion
17.12.2021, 14:00 ~ 15:00. by Daniel STAN, title Regular Model Checking of Epistemic Logic
14.01.2022, 14:00 ~ 15:00. Paper reading discussion
04.02.2022, 14:00 ~ 15:00. Student presentation by Kai Schneider, Decision procedures for path feasibility of string-manipulating programs with complex operations
11.02.2022, 14:00 ~ 15:00. by Micha Schrader, Certified Implementation of Symbolic Automata
04.03.2022, 14:00 ~ 15:00. Student presentation By Philipp Bird, An Overview of K Framework