Lab Course "Modeling and Automated Verification"

Dr. Sascha Klüppelholz, Prof. Christel Baier
SWS: (0/2/0) in English

Description

This lab course is intended for students in the Master's program “Computational Logic” and “Computational Modeling and Simulation”. It affords the opportunity to participate in theoretical as well as applied state-of-the-art research projects. Most problems addressed in this course are closely related to or a part of current research projects of our workgroup. See for example:

• QuantLA
• RoSI
• 5G-Lab Germany

• Foundations of Perspicuous Software Systems (CPEC)

• CeTi

Within these projects, tasks in various areas arise, which include:

• Symbolic methods in model checking
• Explicit model-checking techniques
• Reduction techniques
• Omega-automata (probabilistic)
• Numerical solution methods
• Logics
• Specification formalisms
• Abstraction techniques
• Case studies

Registration

Enrolling via  OPAL is required until 31.10.2020.

Prerequisites

• Solid foundations in algorithms and data structures, complexity theory, automata theory and formal languages
• Basic mathematical foundations
• Programming skills in C/C++ or Java

Rules

The following rules need to be followed in order to assure a successful participation:

Written Part

• There will be an initial event at the beginning of November 2020, where some different topics will be presented.
• Every participant will be assigned to a topic. The aim of this course is to work autonomously on a topic and to give a presentation on the findings. A date for this presentation will be fixed at the initial event for every participant.
• A tutor is assigned to every participant during the initial meeting.
• The developed code has to be commented properly and has to be described in a PDF document.
• The concluding presentation should not exceed 30 minutes.

Awarding of Credit Points

The Credit Points will be awarded if all of the following conditions are fulfilled:

• Every deadline was kept.
• The source code is commented and documented properly.
• The presentation of the own results was acceptable.
• The presentations of the other participants were attended.

Proceedings

All participants will be notified about the initital meeting. This meeting will take the form of a video conference.

Further dates and proceedings will be arranged depending on the current developments of the corona crisis. The same holds for meetings with the tutor.

Creditability

Master Computational Logic

• MCL-PS: Skills

Master Computational Modeling and Simulation

• CMS-MOC: Models of Computation
• CMS-LM-ADV: Advanced Logical Modeling

Contact