Laborkurs "Modeling and Automated Verification"

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 18.04.2021.

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-LM-MOC: Models of Computation
• CMS-LM-ADV: Advanced Logical Modeling

Contact