Logic and Verification Seminar (Summer 2021)

The Logic and Verification seminar is a reading group gathering the members of the Automatic Reasoning AG and students interested in formal methods. During this semester, we will focus on regular model checking techniques.

This approach focuses on manipulating models represented as regular languages or equivalently, finite automata, and their extensions (transducer, tree-automaton, etc). These representations paves the way to novel techniques based on synthesis and learning techniques.

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: ??.05.20
• Report submission deadline: 03.09.21

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 Daniel (stan@cs.uni-kl.de) an email.

When and where

Tentative Schedule and location:

• Room: Online (via OLAT/BBB: follow this link). A confirmation email will be sent out beforehand.
• Date and time: Friday 11:15 to 12:15
• Kickoff meeting: Friday 30.04.21 11:15 - 12:15 via OLAT/BBB: follow this link
• Periodicity: every two weeks (default, unless announced otherwise)
• Registration: send a mail to stan@cs.uni-kl.de with your name and matriculation number

Available topics

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

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

The list of articles for the current section is now available here. Slides of the kickoff meetings.

Some previous topics can be found here here. and some reports and slides here.

Instructors

• Prof. Anthony Lin
• Dr. Daniel Stan
• Oliver Markgraf

Planned sessions

• 30.04.21: Kickoff meeting
• 14.05.21: Topic Selection/Arbitration
• 28.05.21: Short/survey meeting
• 18.06.21: Short/survey meeting
• 16.07.21: Short/survey meeting
• 23.07.21: Student Presentation: Regular Tree Model Checking by HM
• 30.07.21: Student Presentation: Regular Model Checking using Widening Techniques by HE
• 20.08.21: Student Presentation: Parameterized verification through view abstraction by RFN