Semws21

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