Logic and Verification Seminar (Winter 2020)

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 AI systems via games.

From its (arguably) first conception, artificial intelligence has been closely related to games. In the seminal paper Computing Machinery and Intelligence, Alan Turing proposed a technique to answer the question 'Can machines think?', and called such a technique 'imitation game' (later known as the Turing test.) Since then, games have been an integral part of AI research. Today, with the rapid progress and proliferation of AI systems, game theoretic methods provide mathematical tools for proving correctness of dynamical systems, automatically designing provably correct systems, synthesising controller, etc.

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: 26.11.20 03.12.20
  • Report submission deadline: 11.03.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 Najib (najib@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: Thursday 10:00 to 11:00
  • Kickoff meeting: Tuesday 03.11.20 14:30 - 15:30 (48-208) via OLAT/BBB: follow this link
  • Periodicity: weekly (default, unless announced otherwise)
  • Registration: send a mail to najib@cs.uni-kl.de with your name and matriculation number

Available topics

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

  • 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
  • String Constraint Solver
  • Concrete Semantics for Programming Languages

Slides from the kick-off meeting can be downloaded here

List of suggested papers can be found here

Some previous reports and slides can be found here

Instructors

  • Prof. Anthony Lin
  • Dr. Shuanglong Kan
  • Dr. Muhammad Najib

Planned sessions




Übergeordnete Seite: Teaching
[mehr ...]
Feedback zu dieser Seite
Email an den Verantwortlichen dieser Seite (stan@informatik.uni-kl.de) [mehr ...]