International Center for Computational Logic - Benutzerbeiträge [de]

Teamprojekt "Model Checking" (WS2025)

2025-09-23T14:04:28Z

Andrea Kühn:

{{Vorlesung
|Title=Teamprojekt „Model Checking“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=EN
|Term=WS
|Year=2025
|Module=CMS-LM-TEA
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

This course offers advanced topics in the field of formal modeling and analysis. It is meant for students enrolled in the Master's program “Computational Modeling and Simulation”. The tasks are usually taken from our current projects and cover programming as well as theoretical problems. Within this research-relevant project, students are working in teams of about 2 to 4 people to solve a complex interdisciplinary task that includes different areas of logical modeling and model checking.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567445 via Opal] is required until October 20.

=== Prerequisites ===

* Profound knowledge in model checking, acquired in the lecture “Model Checking” or similar courses at other universities
* Solid foundations in algorithms and data structures, in automata theory and formal languages as well as in complexity theory
* Basic mathematical foundations
* Programming skills in Java or C/C++ are beneficial, unless you are interested in a purely theoretical topic

=== Dates ===

Participants will be notified via e-mail about the initial meeting, where each group is assigned a topic. Presentations will be held between January and March. The specific dates will be announced later.

The written summary is due by March 21, 2026.

=== Exam and Creditability ===

'''Master Computational Modeling and Simulation'''

* {{ModuleLink|CMS-LM-TEA}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Profilprojekt Grundlagenforschung (WS2025)

2025-09-23T13:33:19Z

Andrea Kühn:

{{Vorlesung
|Title=Profilprojekt
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=WS
|Year=2025
|Module=INF-PM-FPG, INF-PM-FPA
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|UmfangAlternativ=8P/PB
|Description='''This website is still under construction. Please come back later.'''

The introductory project (Profilprojekt) is intended for students enrolled in the Master or Diplom programs Informatik (computer science). Participants study selected topics from the fields of model checking, automata theory and logics. The purpose is to acquire skills for their research-oriented specialisation and independent research work.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567441 via Opal] is required until October 20.

=== Exam and Creditability ===

We offer three ''Profilprojekte'', which differ slightly in their creditability. The three courses have a unified registration via Opal. If you have questions about the differences between the courses, please contact [[Sascha Klüppelholz]].

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-PM-FPG}} as ''Profilprojekt „Forschungsprojekt Formale Methoden“'': exam according to module description
* {{ModuleLink|INF-PM-FPA}} as ''Profilprojekt „Anwendungsforschung in der Informatik“'': exam according to module description
* {{ModuleLink|INF-PM-FPG}} as ''Profilprojekt „Grundlagenforschung in der Informatik“'': exam according to module description

'''Diplom Informatik (PO 2010)'''
* {{ModuleLink|INF-PM-FPG}} as ''Profilprojekt „Forschungsprojekt Formale Methoden“'': exam according to module description
* {{ModuleLink|INF-PM-FPA}} as ''Profilprojekt „Anwendungsforschung in der Informatik“'': exam according to module description
* {{ModuleLink|INF-PM-FPG}} as ''Profilprojekt „Grundlagenforschung in der Informatik“'': exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Seminar "Selected Topics in Logic and Verification" (WS2025)

2025-09-23T13:27:12Z

Andrea Kühn:

{{Vorlesung
|Title=Seminar “Selected Topics in Logic and Verification”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=EN
|Term=WS
|Year=2025
|Module=CMS-LM-ADV, CMS-LM-MOC, CMS-SEM-A, INF-AQUA, INF-B-510, INF-B-520, INF-D-940, MCL-PS
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

This seminar is mainly intended for students enrolled in the Master or Diplom programs Informatik (computer science).

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567444 via Opal] is required until October 20.

=== Prerequisites ===

The seminar addresses students that have profound knowledge in theoretical computer science and logics.

=== Dates ===

All participants will be notified about the initital meeting by e-mail. Each participant is then assigned a topic and a supervisor.

Presentations will be held between January and March. The specific dates will be announced later. The seminar paper (Seminararbeit) is due by March 7.

=== Exam and Creditability ===

'''Bachelor Informatik (PO 2009)'''
* {{ModuleLink|INF-B-510}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)
* {{ModuleLink|INF-B-520}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-AQUA}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Diplom Informatik (PO 2010)'''
* {{ModuleLink|INF-D-940}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Medieninformatik'''
* {{ModuleLink|INF-AQUA}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Computational Logic'''
* {{ModuleLink|MCL-PS}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-SEM}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)
* {{ModuleLink|CMS-LM-MOC}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)
* {{ModuleLink|CMS-LM-ADV}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Laborkurs "Modeling and Automated Verification" (WS2025)

2025-09-23T13:22:59Z

Andrea Kühn:

{{Vorlesung
|Title=Laborkurs „Modeling and Automated Verification“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=EN
|Term=WS
|Year=2025
|Module=CMS-LM-ADV, CMS-LM-MOC, MCL-PS
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

This lab course is intended for students in the Master's programs “Computational Logic” and “Computational Modeling and Simulation”. It offers 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 are part of current research projects of our workgroup. See for example:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* symbolic methods in model checking,
* explicit model checking,
* reduction techniques,
* automata over finite and infinite words,
* numerical methods for quantitative analysis,
* logics,
* specification formalisms,
* abstraction techniques,
* case studies.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567439 via Opal] is required until October 20.

=== Prerequisites ===

* Solid foundations in algorithms and data structures, complexity theory, automata theory and formal languages
* Solid programming skills
* Basic mathematical foundations

=== Exam and Creditability ===

'''Master Computational Logic'''
* {{ModuleLink|MCL-PS}}: ''Projektarbeit inkl. Präsentation'' (research project with a 10-page documentation and a 30-minute presentation)

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: ''Projektarbeit inkl. Präsentation'' (research project with a 10-page documentation and a 30-minute presentation)
* {{ModuleLink|CMS-LM-ADV}}: ''Projektarbeit inkl. Präsentation'' (research project with a 10-page documentation and a 30-minute presentation)

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Komplexpraktikum "Modellierung und quantitative Systemanalyse I" (WS2025)

2025-09-23T13:16:08Z

Andrea Kühn:

{{Vorlesung
|Title=Komplexpraktikum „Modellierung und quantitative Systemanalyse I“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=WS
|Year=2025
|Module=INF-MA-PR
|SWSLecture=0
|SWSExercise=0
|SWSPractical=4
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

The course is intended for students enrolled in the Master or Diplom programs Informatik (computer science) as well as for those enrolled in the Diplom program Informationssystemtechnik (information systems engineering). The Komplexpraktikum “Modeling and Quantitative System Analysis I” allows students to analyse and work on practical projects relevant in current research. Some topics are taken from current projects of the group. The following links give more information on these projects:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* symbolic methods in model checking,
* explicit model checking,
* reduction techniques,
* automata over finite and infinite words,
* numerical methods for quantitative analysis,
* logics,
* specification formalisms,
* abstraction techniques,
* case studies.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567437 via Opal] is required until October 20.

=== Prerequisites ===

In addition to an interest in theoretical computer science, the project requires solid knowledge of model checking and programming. Experience in C/C++ or Java is helpful, but not required.

=== Dates ===

All enrolled participants will be notified about the initial meeting by e-mail. The specific dates will be announced later.

=== Exam and Creditability ===

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-MA-PR}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Lecture "Model Checking" (WS2025)

2025-09-23T13:14:31Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier; Sascha Klüppelholz
|Language=EN
|Term=WS
|Year=2025
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-25-MA-FTK-MC, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-TCSL
|SWSLecture=4
|SWSExercise=4
|SWSPractical=0
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

Model Checking is a fully automatic verification method for reactive systems. This course provides an introduction to the main principles of model checking:
* modeling reactive systems by means of transition systems,
* linear-time properties and Büchi automata,
* linear temporal logic and automata-based model checking,
* computation tree logic,
* abstraction ((bi)simulation),
* probabilistic model checking.

=== Literature ===

The course follows the book “Principles of Model Checking” (C. Baier, J.P. Katoen; Principles of Model Checking; MIT Press) closely. This book is available at the SLUB (Lehrbuchsammlung).

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567432/CourseNode/1630463385910115008?9 via Opal] is required until November 3.

=== Prerequisites ===

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===

Thursdays and Fridays, 9:20–10:50 and 11:10–12:40, APB E005 (starting October 16)

There is no fixed assignment of the lectures and exercises to time slots. It will be announced each week when lectures and exercises will take place in the following week.

The course consists of a (4/2/0) lecture with exercises for the theoretical foundations and an introduction to model checkers with practical exercises (0/2/0).

=== Creditability ===
'''Bachelor Informatik (PO 2009)'''
* {{ModuleLink|INF-B-510}}: oral exam (30 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (30 minutes)

'''Bachelor Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computer Science (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Diplom Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-TCSL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: oral exam (30 minutes)
* {{ModuleLink|CMS-LM-ADV}}: oral exam (30 minutes)

=== Oral Exams ===

Appointments for the oral examination are to be made via our secretary's office. Please contact [[Andrea Kühn]] via e-mail.

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Komplexpraktikum "Modellierung und quantitative Systemanalyse II" (WS2025)

2025-09-23T13:13:57Z

Andrea Kühn:

{{Vorlesung
|Title=Komplexpraktikum „Modellierung und quantitative Systemanalyse II“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=WS
|Year=2025
|Module=INF-MA-PR
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Exam type=nach Modulbeschreibung
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

The course is intended for students enrolled in the Master or Diplom programs Informatik (computer science) as well as for those enrolled in the Diplom program Informationssystemtechnik (information systems engineering). The Komplexpraktikum “Modeling and Quantitative System Analysis II” allows students to analyse and work on practical projects relevant in current research. Some topics are taken from current projects of the group. The following links give more information on these projects:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* symbolic methods in model checking,
* explicit model checking,
* reduction techniques,
* automata over finite and infinite words,
* numerical methods for quantitative analysis,
* logics,
* specification formalisms,
* abstraction techniques,
* case studies.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567438/ via Opal] is required until October 20.

=== Prerequisites ===

In addition to an interest in theoretical computer science, the project requires solid knowledge of model checking and programming. Experience in C/C++ or Java is helpful, but not required.

=== Dates ===

All enrolled participants will be notified about the initial meeting by e-mail. The specific dates will be announced later.

=== Exam and Creditability ===

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-MA-PR}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Forschungsprojekt: Algebraische und logische Grundlagen der Informatik (WS2025)

2025-09-23T13:08:24Z

Andrea Kühn:

{{Vorlesung
|Title=Forschungsprojekt
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=WS
|Year=2025
|Module=INF-25-MA-FP
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|UmfangAlternativ=Projekte (100 Stunden)
|Description='''This website is still under construction. Please come back later.'''

The Forschungsprojekt is intended for students enrolled in the Master Computer Science and Diplom Informatik programs. Participants study selected topics from the fields of model checking, automata theory and logics. The purpose is to acquire skills for their research-oriented specialisation and independent research work.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567435 via Opal] is required until October 20.

=== Exam and Creditability ===

'''Master Computer Science (PO 2025)'''
* {{ModuleLink|INF-25-MA-FP}}: exam according to module description

'''Diplom Informatik (PO 2025)'''
* {{ModuleLink|INF-25-MA-FP}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Forschungsprojekt: Algebraische und logische Grundlagen der Informatik (WS2025)

2025-09-23T13:06:34Z

Andrea Kühn:

{{Vorlesung
|Title=Forschungsprojekt
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=WS
|Year=2025
|Module=INF-25-MA-FP
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|UmfangAlternativ=Projekte (100 Stunden)
|Description='''This website is still under construction. Please come back later.'''

The Forschungsprojekt is intended for students enrolled in the Master Computer Science and Diplom Informatik. Participants study selected topics from the fields of model checking, automata theory and logics. The purpose is to acquire skills for their research-oriented specialisation and independent research work.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567435 via Opal] is required until October 20.

=== Exam and Creditability ===

'''Master Computer Science (PO 2025)'''
* {{ModuleLink|INF-25-MA-FP}}: exam according to module description

'''Diplom Informatik (PO 2025)'''
* {{ModuleLink|INF-25-MA-FP}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Lecture "Modal Logic" (WS2025)

2025-09-23T13:03:08Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Modal Logic”
|Research group=Algebraische und logische Grundlagen der Informatik
|Language=EN
|Lecturers=Jakob Piribauer
|Term=WS
|Year=2025
|Module=CMS-LM-BAS, INF-25-Ma-FTK-ASAI, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-TCSL
|SWSLecture=2
|SWSExercise=2
|SWSPractical=0
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

Modalities are expressions that quantify the truth of a statement, e.g. ‘possibly’ and ‘necessarily’. Modal logics are simple, yet expressive formalisms that incorporate such modalities. The incorporated modalities offer a wide variety of possible readings such as temporal readings (‘at some point in the future …’), epistemic readings (‘the agent knows that …’) or readings talking about the dynamics of programs (‘there is an execution of program P after which …’). Therefore, modal logics are applicable to various application domains and play an important role in computer science, philosophy, mathematics and linguistics, among others.

This course provides an introduction to the main concepts of modal logic with a focus on its role in computer science. It covers:
* syntax and semantics of modal logics,
* Kripke structures and Kripke frames,
* bisimulations,
* translations to first-order logic,
* frame definability,
* soundness and completeness results,
* complexity and decidability results,
* propositional dynamic logic.

===Literature===

The course follows the book “Modal logic (Fourth printing with corrections)” (P. Blackburn, M. de Rijke, Y. Venema; Modal logic (Fourth printing with corrections); Cambridge University Press; 2010). This book is available online via the [https://doi.org/10.1017/CBO9781107050884 SLUB].

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567433 via Opal] is required until November 3.

=== Prerequisites ===

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===

* Lecture: Wednesdays, 14:50–16:20, APB E005
* Exercise: Thursdays, 14:50–16:20, APB E006

The first lecture is held on October 15. Occasionally, there might be exercises during the Wednesdays or lectures on Thursdays, which will be announced in advance.

=== Creditability ===
'''Bachelor Informatik (PO 2009)'''
* {{ModuleLink|INF-B-510}}: oral exam (25 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (25 minutes)

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computer Science (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-ASAI}}: exam according to module description

'''Diplom Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-ASAI}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-TCSL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-BAS}}: oral exam (25 minutes)

=== Oral Exams ===

Appointments for the oral examination are to be made via our secretary’s office. Please contact [[Andrea Kühn]] via e-mail.

=== Contact ===

In case of organisational questions, please contact [[Jakob Piribauer]].
}}

Lecture "Model Checking" (WS2025)

2025-09-23T13:01:57Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier; Sascha Klüppelholz
|Language=EN
|Term=WS
|Year=2025
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-25-MA-FTK-MC, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-TCSL
|SWSLecture=4
|SWSExercise=4
|SWSPractical=0
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

Model Checking is a fully automatic verification method for reactive systems. This course provides an introduction to the main principles of model checking:
* modeling reactive systems by means of transition systems
* linear-time properties and Büchi automata
* linear temporal logic and automata-based model checking
* computation tree logic
* abstraction ((bi)simulation)
* probabilistic model checking

=== Literature ===

The course follows the book “Principles of Model Checking” (C. Baier, J.P. Katoen; Principles of Model Checking; MIT Press) closely. This book is available at the SLUB (Lehrbuchsammlung).

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567432/CourseNode/1630463385910115008?9 via Opal] is required until November 3.

=== Prerequisites ===

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===

Thursdays and Fridays, 9:20–10:50 and 11:10–12:40, APB E005 (starting October 16)

There is no fixed assignment of the lectures and exercises to time slots. It will be announced each week when lectures and exercises will take place in the following week.

The course consists of a (4/2/0) lecture with exercises for the theoretical foundations and an introduction to model checkers with practical exercises (0/2/0).

=== Creditability ===
'''Bachelor Informatik (PO 2009)'''
* {{ModuleLink|INF-B-510}}: oral exam (30 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (30 minutes)

'''Bachelor Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computer Science (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Diplom Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-TCSL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: oral exam (30 minutes)
* {{ModuleLink|CMS-LM-ADV}}: oral exam (30 minutes)

=== Oral Exams ===

Appointments for the oral examination are to be made via our secretary's office. Please contact [[Andrea Kühn]] via e-mail.

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Lecture "Model Checking" (WS2025)

2025-09-23T13:00:13Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier; Sascha Klüppelholz
|Language=EN
|Term=WS
|Year=2025
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-25-MA-FTK-MC, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-TCSL
|SWSLecture=4
|SWSExercise=4
|SWSPractical=0
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

Model Checking is a fully automatic verification method for reactive systems. This course provides an introduction to the main principles of model checking:
* modeling reactive systems by means of transition systems
* linear-time properties and Büchi automata
* linear temporal logic and automata-based model checking
* computation tree logic
* abstraction ((bi)simulation)
* probabilistic model checking

=== Literature ===

The course follows the book “Principles of Model Checking” (C. Baier, J.P. Katoen; Principles of Model Checking; MIT Press) closely. This book is available at the SLUB (Lehrbuchsammlung).

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567432/CourseNode/1630463385910115008?9 via Opal] is required until November 3.

=== Prerequisites ===

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===

Thursdays and Fridays, 9:20–10:50 and 11:10–12:40, APB E005 (starting October 16)

There is no fixed assignment of the lectures and exercises to time slots. It will be announced each week when lectures and exercises will take place in the following week.

The course consists of a (4/2/0) lecture with exercises for the theoretical foundations and an introduction to model checkers with practical exercises (0/2/0).

=== Creditability ===
'''Bachelor Informatik (PO 2009)'''
* {{ModuleLink|INF-B-510}}: oral exam (30 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (30 minutes)

'''Bachelor Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computer Science (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Diplom Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-TCSL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: oral exam (30 minutes)
* {{ModuleLink|CMS-LM-ADV}}: oral exam (30 minutes)

=== Oral Exams ===

Appointments for the oral examination are made via our secretary's office. Please contact [[Andrea Kühn]] via e-mail.

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Lecture "Model Checking" (WS2025)

2025-09-23T12:59:55Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier; Sascha Klüppelholz
|Language=EN
|Term=WS
|Year=2025
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-25-MA-FTK-MC, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-TCSL
|SWSLecture=4
|SWSExercise=4
|SWSPractical=0
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

Model Checking is a fully automatic verification method for reactive systems. This course provides an introduction to the main principles of model checking:
* modeling reactive systems by means of transition systems
* linear-time properties and Büchi automata
* linear temporal logic and automata-based model checking
* computation tree logic
* abstraction ((bi)simulation)
* probabilistic model checking

=== Literature ===

The course follows the book “Principles of Model Checking” (C. Baier, J.P. Katoen; Principles of Model Checking; MIT Press) closely. This book is available at the SLUB (Lehrbuchsammlung).

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567432/CourseNode/1630463385910115008?9 via Opal] is required until November 3.

=== Prerequisites ===

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===

Thursdays and Fridays, 9:20–10:50 and 11:10–12:40, APB E005 (starting October 16)

There is no fixed assignment of the lectures and exercises to time slots. It will be announced each week when lectures and exercises will take place in the following week.

The course consists of a (4/2/0) lecture with exercises for the theoretical foundations and an introduction to model checkers with practical exercises (0/2/0).

=== Creditability ===
'''Bachelor Informatik (PO 2009)'''
* {{ModuleLink|INF-B-510}}: oral exam (30 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (30 minutes)

'''Bachelor Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computer Science (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Diplom Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-MC}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-TCSL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: oral exam (30 minutes)
* {{ModuleLink|CMS-LM-ADV}}: oral exam (30 minutes)

=== Oral Exams ===

Appointments for the oral examination are made via our secretary's office. Please contact [[Andrea Kühn]] via email.

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Lecture "Modal Logic" (WS2025)

2025-09-23T12:59:31Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Modal Logic”
|Research group=Algebraische und logische Grundlagen der Informatik
|Language=EN
|Lecturers=Jakob Piribauer
|Term=WS
|Year=2025
|Module=CMS-LM-BAS, INF-25-Ma-FTK-ASAI, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-TCSL
|SWSLecture=2
|SWSExercise=2
|SWSPractical=0
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

Modalities are expressions that quantify the truth of a statement, e.g. ‘possibly’ and ‘necessarily’. Modal logics are simple, yet expressive formalisms that incorporate such modalities. The incorporated modalities offer a wide variety of possible readings such as temporal readings (‘at some point in the future …’), epistemic readings (‘the agent knows that …’) or readings talking about the dynamics of programs (‘there is an execution of program P after which …’). Therefore, modal logics are applicable to various application domains and play an important role in computer science, philosophy, mathematics and linguistics, among others.

This course provides an introduction to the main concepts of modal logic with a focus on its role in computer science. It covers:
* syntax and semantics of modal logics,
* Kripke structures and Kripke frames,
* bisimulations,
* translations to first-order logic,
* frame definability,
* soundness and completeness results,
* complexity and decidability results,
* propositional dynamic logic.

===Literature===

The course follows the book “Modal logic (Fourth printing with corrections)” (P. Blackburn, M. de Rijke, Y. Venema; Modal logic (Fourth printing with corrections); Cambridge University Press; 2010). This book is available online via the [https://doi.org/10.1017/CBO9781107050884 SLUB].

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51182567433 via Opal] is required until November 3.

=== Prerequisites ===

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===

* Lecture: Wednesdays, 14:50–16:20, APB E005
* Exercise: Thursdays, 14:50–16:20, APB E006

The first lecture is held on October 15. Occasionally, there might be exercises during the Wednesdays or lectures on Thursdays, which will be announced in advance.

=== Creditability ===
'''Bachelor Informatik (PO 2009)'''
* {{ModuleLink|INF-B-510}}: oral exam (25 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (25 minutes)

'''Master Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computer Science (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-ASAI}}: exam according to module description

'''Diplom Informatik (PO 2010)'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik (PO 2025)'''
* {{ModuleLink|INF-25-Ma-FTK-ASAI}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-TCSL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-BAS}}: oral exam (25 minutes)

=== Oral Exams ===

Appointments for the oral examination are made via our secretary’s office. Please contact [[Andrea Kühn]] via e-mail.

=== Contact ===

In case of organisational questions, please contact [[Jakob Piribauer]].
}}

CMS Research Project Model Checking (WS2025)

2025-09-23T12:43:01Z

Andrea Kühn:

{{Vorlesung
|Title=CMS Research Project “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=EN
|Term=WS
|Year=2025
|Module=CMS-PRO
|SWSLecture=0
|SWSExercise=0
|SWSPractical=12
|Description='''This page is still under construction. The information is preliminary and subject to change. Please check back later!'''

This course offers advanced topics in the field of verification and model checking. It is meant for students enrolled in the Master's program “Computational Modeling and Simulation”. The tasks are usually taken from our current projects and cover programming as well as theoretical problems.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027280/ via Opal] is required until October 20.

=== Prerequisites ===

* Profound knowledge in model checking, acquired in the lecture “Model Checking” or similar courses at other universities
* Solid foundations in algorithms and data structures, in automata theory and formal languages as well as in complexity theory
* Basic mathematical foundations
* Programming skills in Java or C/C++ are beneficial, unless you are interested in a purely theoretical topic

=== Dates ===

All enrolled participants will be notified about the initital meeting by e-mail.

=== Exam and Creditability ===
'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-PRO}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Proseminar „Binäre Entscheidungsgraphen“ (SS2025)

2025-03-17T14:41:32Z

Andrea Kühn:

{{Vorlesung
|Title=Proseminar „Binäre Entscheidungsgraphen“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=DE
|Term=SS
|Year=2025
|Lecture series=Proseminar „Binäre Entscheidungsgraphen“
|Module=INF-B-610, INF-D-520
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=Das Proseminar richtet sich an Studierende der Studiengänge Bachelor und Diplom Informatik. Das Thema des Proseminars sind Binäre Entscheidungsgraphen (engl. binary decision diagrams, kurz BDDs). Diese wurden erstmals von Lee und Akers zur Darstellung von Schaltfunktionen vorgestellt. Heutzutage werden verschiedene Varianten von ordered BDDs (OBDDs) in zahlreichen Verifikationswerkzeugen und Model Checkern wie z. B. nuSMV oder Prism als Datenstruktur zur effizienten Speicherung und Analyse von Systemmodellen eingesetzt.

Die individuell zu bearbeitenden Seminarthemen befassen sich mit den theoretischen Grundlagen binärer Entscheidungsgraphen. Insbesondere sollen die wichtigsten Operatoren und Algorithmen auf BDDs vorgestellt und hinsichtlich ihrer theoretischen Komplexität untersucht werden.

Das Proseminar wird auf Deutsch abgehalten.

=== Registrierung ===

Die Teilnahme setzt eine Registierung [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027283 via Opal] bis zum 14. April voraus.

=== Voraussetzungen ===

Neben dem Interesse an Theoretischer Informatik setzt das Proseminar solide Kenntnisse in den Gebieten Algorithmen und Datenstrukturen sowie Mathematik im Umfang der ersten zwei Studiensemester voraus.

=== Ablauf ===

Alle fristgerecht eingeschriebenen Teilnehmer:innen werden per E-Mail über die Einführungsveranstaltung informiert. In dieser wird allen Teilnehmer:innen je ein Thema und ein Betreuer zugeteilt. Das weitere Vorgehen wird individuell mit dem Betreuer besprochen.

Die Vorträge werden als Blockveranstaltung im Zeitraum Juni–August 2025 stattfinden. Termine werden später bekanntgegeben.

Die schriftliche Ausarbeitung ist bis zum 30. August 2025 einzureichen.

=== Prüfungsleistung und anrechenbare Module ===

'''Bachelor Informatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Diplom Informatik'''
* {{ModuleLink|INF-D-520}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Bachelor Medieninformatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

=== Kontakt ===

Bei organisatorischen Fragen wenden Sie sich bitte an [[Sascha Klüppelholz]].
}}

Team Project “Model Checking” (SS2025)

2025-03-17T14:25:17Z

Andrea Kühn:

{{Vorlesung
|Title=Team Project “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Team Project “Model Checking”
|Module=CMS-LM-TEA
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Description=This course offers advanced topics in the field of formal modeling and analysis. It is meant for students enrolled in the Master's program “Computational Modeling and Simulation”. The tasks are usually taken from our current projects and cover programming and theoretical problems as well. Within this research-relevant project, students are working in teams of about 2 to 4 people to solve a complex interdisciplinary task that includes different areas of logical modeling and model checking.

This course is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027281 via Opal] is required until April 14.

=== Prerequisites ===

* Profound knowledge in model checking, acquired in the lecture “Model Checking” or similar courses at other universities
* Solid foundations in algorithms and data structures, in automata theory and formal languages as well as in complexity theory
* Basic mathematical foundations
* Programming skills in Java or C/C++ are beneficial, unless you are interested in a purely theoretical topic

=== Dates ===

Participants will be notified via e-mail about the initial meeting, where each group is assigned a topic. Presentations will be held between June and August. The specific dates will be announced later.

The written summary is due by August 30, 2025.

=== Exam and Creditability ===

* {{ModuleLink|CMS-LM-TEA}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Team Project “Model Checking” (SS2025)

2025-03-17T14:24:44Z

Andrea Kühn:

{{Vorlesung
|Title=Team Project “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Team Project “Model Checking”
|Module=CMS-LM-TEA
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Description=This course offers advanced topics in the field of formal modeling and analysis. It is meant for students enrolled in the Master's program “Computational Modeling and Simulation”. The tasks are usually taken from our current projects and cover programming and theoretical problems as well. Within this research-relevant project, students are working in teams of about 2 to 4 people to solve a complex interdisciplinary task that includes different areas of logical modeling and model checking.

This course is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027281 via Opal] is required until April 14.

=== Prerequisites ===

* Profound knowledge in model checking, acquired in the lecture “Model Checking” or similar courses at other universities
* Solid foundations in algorithms and data structures, in automata theory and formal languages as well as in complexity theory
* Basic mathematical foundations
* Programming skills in Java or C/C++ are beneficial, unless you are interested in a purely theoretical topic

=== Dates ===

Participants will be notified via e-mail about the initial meeting, where each group is assigned a topic. Presentations will be held between June and August. The specific dates will be announced later.

The written summary is due by August 30, 2025.

=== Exam and Creditability ===

* {{ModuleLink|CMS-LM-TEA}}: exam is according to the module description.

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Seminar “Selected Topics in Logic and Verification” (SS2025)

2025-03-17T14:24:05Z

Andrea Kühn:

{{Vorlesung
|Title=Seminar “Selected Topics in Logic and Verification”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Seminar “Selected Topics in Logic and Verification”
|Module=CMS-LM-ADV, CMS-LM-MOC, CMS-SEM, INF-AQUA, INF-D-940, MCL-PS, INF-B-510, INF-B-520
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=This seminar is mainly intended for students enrolled in the Master or Diplom programs Informatik (computer science).

This seminar is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027275?58 via Opal] is required until April 14.

=== Prerequisites ===

The seminar addresses students that have profound knowledge in theoretical computer science and logics.

=== Dates ===

All participants will be notified about the initital meeting by e-mail. Each participant is then assigned a topic and a supervisor.

Presentations will be held between June and August. The specific dates will be announced later. The seminar paper (Seminararbeit) is due by August 16.

=== Exam and Creditability ===

'''Bachelor Informatik'''
* {{ModuleLink|INF-B-510}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)
* {{ModuleLink|INF-B-520}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Informatik'''
* {{ModuleLink|INF-AQUA}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Diplom Informatik'''
* {{ModuleLink|INF-D-940}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Medieninformatik'''
* {{ModuleLink|INF-AQUA}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Computational Logic'''
* {{ModuleLink|MCL-PS}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-SEM}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)
* {{ModuleLink|CMS-LM-MOC}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)
* {{ModuleLink|CMS-LM-ADV}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Research Seminar “Formal Methods” (SS2025)

2025-03-17T14:23:20Z

Andrea Kühn:

{{Vorlesung
|Title=Research Seminar “Formal Methods”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Research Seminar “Formal Methods”
|Module=INF-PM-FOR
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=This seminar is mainly intended for students enrolled in the Master or Diplom programs Informatik (computer science). Participants engage with selected topics from the field of Model Checking.

This course is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027282/ via Opal] is required until April 14.

=== Prerequisites ===

The seminar addresses students that have profound knowledge in theoretical computer science and logics. Background knowledge in the areas of formal methods (and model checking in particular) or concurrency theory is recommended.

=== Dates ===

All participants will be notified about the initital meeting by e-mail.

=== Exam and Creditability ===

* {{ModuleLink|INF-PM-FOR}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Proseminar “Theoretische Informatik” (SS2025)

2025-03-17T14:23:05Z

Andrea Kühn:

{{Vorlesung
|Title=Proseminar „Theoretische Informatik“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=DE
|Term=SS
|Year=2025
|Lecture series=Proseminar „Theoretische Informatik“
|Module=INF-B-610, INF-D-520
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=Das Proseminar richtet sich an Studierende der Studiengänge Bachelor und Diplom Informatik. Das Thema des Proseminars ist die Analyse von Algorithmen. Es werden u. a. Algorithmen aus den Büchern [https://mitpress.mit.edu/9780262046305/introduction-to-algorithms/ „Introduction to Algorithms“] von Cormen, Leiserson, Rivest und Stein, [https://www-cs-faculty.stanford.edu/~knuth/gkp.html „Concrete Mathematics“] von Graham, Knuth und Patashnik sowie [https://diestel-graph-theory.com/german/index.html „Graphentheorie“] von Diestel betrachtet.

Das Proseminar wird auf Deutsch abgehalten.

=== Registrierung ===

Die Teilnahme setzt eine Registierung [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027274/ via Opal] bis zum 14. April voraus.

=== Voraussetzungen ===

Neben dem Interesse an Theoretischer Informatik setzt das Proseminar solide Kenntnisse in den Gebieten Algorithmen und Datenstrukturen sowie Mathematik im Umfang der ersten zwei Studiensemester voraus.

=== Ablauf ===

Alle fristgerecht eingeschriebenen Teilnehmer:innen werden per E-Mail über die Einführungsveranstaltung informiert. In dieser wird allen Teilnehmer:innen je ein Thema und ein Betreuer zugeteilt. Das weitere Vorgehen wird individuell mit dem Betreuer besprochen.

Die Vorträge werden als Blockveranstaltung im Zeitraum Juni–August 2025 stattfinden. Termine werden später bekanntgegeben.

Die schriftliche Ausarbeitung ist bis zum 30. August 2025 einzureichen.

=== Prüfungsleistung und anrechenbare Module ===

'''Bachelor Informatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Diplom Informatik'''
* {{ModuleLink|INF-D-520}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Bachelor Medieninformatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

=== Kontakt ===

Bei organisatorischen Fragen wenden Sie sich bitte an [[Sascha Klüppelholz]].
}}

Profilprojekt “Research Project Formal Methods” (SS2025)

2025-03-17T14:22:33Z

Andrea Kühn:

{{Vorlesung
|Title=Profilprojekt „Forschungsprojekt Formale Methoden“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=SS
|Year=2025
|Lecture series=Profilprojekt „Forschungsprojekt Formale Methoden“
|Module=INF-PM-FPG
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Description=The introductory project (Profilprojekt) is intended for students enrolled in the Master or Diplom programs Informatik (computer science). Participants study selected topics from the fields of model checking, automata theory and logics. The purpose is to acquire skills for their research-oriented specialization and independent research work.

This course is offered in German and English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027279 via Opal] is required until April 14.

=== Exam and Creditability ===

'''Master Informatik'''
* {{ModuleLink|INF-PM-FPG}}: exam according to module description

'''Diplom Informatik'''
* {{ModuleLink|INF-PM-FPG}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Lab Course “Modeling and Automated Verification” (SS2025)

2025-03-17T14:22:18Z

Andrea Kühn:

{{Vorlesung
|Title=Lab Course “Modeling and Automated Verification”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Lab Course “Modeling and Automated Verification”
|Module=CMS-LM-ADV, CMS-LM-MOC, MCL-PS
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=This lab course is intended for students in the Master's programs “Computational Logic” and “Computational Modeling and Simulation”. It offers 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 are part of current research projects of our workgroup. See for example:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* Symbolic methods in model checking
* Explicit model checking
* Reduction techniques
* Automata over finite and infinite words
* Numerical methods for quantitative analysis
* Logics
* Specification formalisms
* Abstraction techniques
* Case studies

This course is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027273/ via Opal] is required until April 14.

=== Prerequisites ===

* Solid foundations in algorithms and data structures, complexity theory, automata theory and formal languages
* Solid programming skills
* Basic mathematical foundations

=== Exam and Creditability ===

'''Master Computational Logic'''
* {{ModuleLink|MCL-PS}}: ''Projektarbeit inkl. Kolloquium'' (research project with a 10-page documentation and a 30-minute presentation)

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: ''Projektarbeit inkl. Kolloquium'' (research project with a 10-page documentation and a 30-minute presentation)
* {{ModuleLink|CMS-LM-ADV}}: ''Projektarbeit inkl. Kolloquium'' (research project with a 10-page documentation and a 30-minute presentation)

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Komplexpraktikum „Modellierung und quantitative Systemanalyse II“ (SS2025)

2025-03-17T14:21:56Z

Andrea Kühn:

{{Vorlesung
|Title=Komplexpraktikum „Modellierung und quantitative Systemanalyse Ⅱ“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=SS
|Year=2025
|Module=INF-MA-PR
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Description=The course is intended for students enrolled in the Master or Diplom programs Informatik (computer science) as well as for those enrolled in the Diplom program Informationssystemtechnik (information systems engineering). The Komplexpraktikum “Modeling and Quantitative System Analysis I” allows students to analyse and work on practical projects relevant in current research. Some topics are taken from current projects of the group. The following links give more information on these projects:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* Symbolic methods in model checking
* Explicit model checking
* Reduction techniques
* Automata over finite and infinite words
* Numerical methods for quantitative analysis
* Logics
* Specification formalisms
* Abstraction techniques
* Case studies

This course is offered in German and English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027278 via Opal] is required until April 14.

=== Prerequisites ===

In addition to an interest in theoretical computer science, the project requires solid knowledge of model checking and programming. Experience in C/C++ or Java is helpful, but not required.

=== Dates ===

All enrolled participants will be notified about the initial meeting by e-mail. The specific dates will be announced later.

=== Exam and Creditability ===

'''Master Informatik'''
* {{ModuleLink|INF-MA-PR}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Komplexpraktikum „Modellierung und quantitative Systemanalyse I“ (SS2025)

2025-03-17T14:21:32Z

Andrea Kühn:

{{Vorlesung
|Title=Komplexpraktikum „Modellierung und quantitative Systemanalyse Ⅰ“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=SS
|Year=2025
|Module=INF-MA-PR
|SWSLecture=0
|SWSExercise=0
|SWSPractical=4
|Description=The course is intended for students enrolled in the Master or Diplom programs Informatik (computer science) as well as for those enrolled in the Diplom program Informationssystemtechnik (information systems engineering). The Komplexpraktikum “Modeling and Quantitative System Analysis I” allows students to analyse and work on practical projects relevant in current research. Some topics are taken from current projects of the group. The following links give more information on these projects:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* Symbolic methods in model checking
* Explicit model checking
* Reduction techniques
* Automata over finite and infinite words
* Numerical methods for quantitative analysis
* Logics
* Specification formalisms
* Abstraction techniques
* Case studies

This course is offered in German and English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027276/ via Opal] is required until April 14.

=== Prerequisites ===

In addition to an interest in theoretical computer science, the project requires solid knowledge of model checking and programming. Experience in C/C++ or Java is helpful, but not required.

=== Dates ===

All enrolled participants will be notified about the initial meeting by e-mail. The specific dates will be announced later.

=== Exam and Creditability ===

'''Master Informatik'''
* {{ModuleLink|INF-MA-PR}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

CMS Research Project “Model Checking” (SS2025)

2025-03-17T14:20:38Z

Andrea Kühn:

{{Vorlesung
|Title=CMS Research Project “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=EN
|Term=SS
|Year=2025
|Lecture series=CMS Research Project “Model Checking”
|Module=CMS-PRO
|SWSLecture=0
|SWSExercise=0
|SWSPractical=12
|Description=This course offers advanced topics in the field of verification and model checking. It is meant for students enrolled in the Master's program “Computational Modeling and Simulation”. The tasks are usually taken from our current projects and cover programming and theoretical problems as well.

This course is in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027280 via Opal] is required until April 14.

=== Prerequisites ===

* Profound knowledge in model checking, acquired in the lecture “Model Checking” or similar courses at other universities
* Solid foundations in algorithms and data structures, in automata theory and formal languages as well as in complexity theory
* Basic mathematical foundations
* Programming skills in Java or C/C++ are beneficial, unless you are interested in a purely theoretical topic

=== Dates ===

All enrolled participants will be notified about the initital meeting by e-mail.

=== Exam and Creditability ===
'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-PRO}}: exam according to module description

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Advanced Logics (SS2025)

2025-03-17T14:19:58Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Advanced Logics”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier; Jakob Piribauer
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Advanced Logics
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-AL
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Description=The purpose of this course is to study several extensions of classical propositional, first-order and second-order logic. We will concentrate on aspects of mathematical logic that are relevant for computer science, such as expressiveness, game-theoretic characterizations, deductive calculi, decision and transformation algorithms and computational complexity.

This lecture is in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027272?29 via Opal] is required until April 30.

=== Prerequisites ===

For the course, basic knowledge in algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===
* Lecture: Thursdays and Fridays, 9:20–10:50, APB E005 (starting April 10)
* Tutorial: Thursdays, 11:10–12:40, APB E005 (starting April 17)

=== Creditability ===
'''Bachelor Informatik'''
* {{ModuleLink|INF-B-510}}: oral exam (30 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (30 minutes)

'''Master Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-AL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: oral exam (30 minutes)
* {{ModuleLink|CMS-LM-ADV}}: oral exam (30 minutes)

=== Contact ===

In case of organisational questions, please contact [[Sascha Klüppelholz]].
}}

Proseminar „Binäre Entscheidungsgraphen“ (SS2025)

2025-03-17T14:16:36Z

Andrea Kühn:

{{Vorlesung
|Title=Proseminar „Binäre Entscheidungsgraphen“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=DE
|Term=SS
|Year=2025
|Lecture series=Proseminar „Binäre Entscheidungsgraphen“
|Module=INF-B-610, INF-D-520
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=Das Proseminar richtet sich an Studierende der Studiengänge Bachelor und Diplom Informatik. Das Thema des Proseminars sind Binäre Entscheidungsgraphen (engl. binary decision diagrams, kurz BDDs). Diese wurden erstmals von Lee und Akers zur Darstellung von Schaltfunktionen vorgestellt. Heutzutage werden verschiedene Varianten von ordered BDDs (OBDDs) in zahlreichen Verifikationswerkzeugen und Model Checkern wie z. B. nuSMV oder Prism als Datenstruktur zur effizienten Speicherung und Analyse von Systemmodellen eingesetzt.

Die individuell zu bearbeitenden Seminarthemen befassen sich mit den theoretischen Grundlagen binärer Entscheidungsgraphen. Insbesondere sollen die wichtigsten Operatoren und Algorithmen auf BDDs vorgestellt und hinsichtlich ihrer theoretischen Komplexität untersucht werden.

Das Proseminar wird auf Deutsch abgehalten.

=== Registrierung ===

Die Teilnahme setzt eine Registierung [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027283 via Opal] bis zum 21. April voraus.

=== Voraussetzungen ===

Neben dem Interesse an Theoretischer Informatik setzt das Proseminar solide Kenntnisse in den Gebieten Algorithmen und Datenstrukturen sowie Mathematik im Umfang der ersten zwei Studiensemester voraus.

=== Ablauf ===

Alle fristgerecht eingeschriebenen Teilnehmer:innen werden per E-Mail über die Einführungsveranstaltung informiert. In dieser wird allen Teilnehmer:innen je ein Thema und ein Betreuer zugeteilt. Das weitere Vorgehen wird individuell mit dem Betreuer besprochen.

Die Vorträge werden als Blockveranstaltung im Zeitraum Juni–August 2025 stattfinden. Termine werden später bekanntgegeben.

Die schriftliche Ausarbeitung ist bis zum 30. August 2025 einzureichen.

=== Prüfungsleistung und anrechenbare Module ===

'''Bachelor Informatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Diplom Informatik'''
* {{ModuleLink|INF-D-520}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Bachelor Medieninformatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

=== Kontakt ===

Bei organisatorischen Fragen wenden Sie sich bitte an [[Sascha Klüppelholz]].
}}

Advanced Logics (SS2025)

2025-03-17T14:14:57Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Advanced Logics”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier; Jakob Piribauer
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Advanced Logics
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-AL
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Description=The purpose of this course is to study several extensions of classical propositional, first-order and second-order logic. We will concentrate on aspects of mathematical logic that are relevant for computer science, such as expressiveness, game-theoretic characterizations, deductive calculi, decision and transformation algorithms and computational complexity.

This lecture is in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027272?29 via Opal] is required until April 30.

=== Prerequisites ===

For the course, basic knowledge in algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===
* Lecture: Thursdays and Fridays, 9:20–10:50, APB E005 (starting April 10)
* Tutorial: Thursdays, 11:10–12:40, APB E005 (starting April 17)

=== Creditability ===
'''Bachelor Informatik'''
* {{ModuleLink|INF-B-510}}: oral exam (30 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (30 minutes)

'''Master Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-AL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: oral exam (30 minutes)
* {{ModuleLink|CMS-LM-ADV}}: oral exam (30 minutes)

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Proseminar „Binäre Entscheidungsgraphen“ (SS2025)

2025-03-17T14:11:52Z

Andrea Kühn:

{{Vorlesung
|Title=Proseminar „Binäre Entscheidungsgraphen“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=DE
|Term=SS
|Year=2025
|Lecture series=Proseminar „Binäre Entscheidungsgraphen“
|Module=INF-B-610, INF-D-520
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=Das Proseminar richtet sich an Studierende der Studiengänge Bachelor und Diplom Informatik. Das Thema des Proseminars sind Binäre Entscheidungsgraphen (engl. binary decision diagrams, kurz BDDs). Diese wurden erstmals von Lee und Akers zur Darstellung von Schaltfunktionen vorgestellt. Heutzutage werden verschiedene Varianten von ordered BDDs (OBDDs) in zahlreichen Verifikationswerkzeugen und Model Checkern wie z. B. nuSMV oder Prism als Datenstruktur zur effizienten Speicherung und Analyse von Systemmodellen eingesetzt.

Die individuell zu bearbeitenden Seminarthemen befassen sich mit den theoretischen Grundlagen binärer Entscheidungsgraphen. Insbesondere sollen die wichtigsten Operatoren und Algorithmen auf BDDs vorgestellt und hinsichtlich ihrer theoretischen Komplexität untersucht werden.

Das Proseminar wird auf Deutsch abgehalten.

=== Registrierung ===

Die Teilnahme setzt eine Registierung [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027283 via Opal] bis zum 21. April voraus.

=== Voraussetzungen ===

Neben dem Interesse an Theoretischer Informatik setzt das Proseminar solide Kenntnisse in den Gebieten Algorithmen und Datenstrukturen sowie Mathematik im Umfang der ersten zwei Studiensemester voraus.

=== Ablauf ===

Alle fristgerecht eingeschriebenen Teilnehmer:innen werden per E-Mail über die Einführungsveranstaltung informiert. In dieser wird allen Teilnehmer:innen je ein Thema und ein Betreuer zugeteilt. Das weitere Vorgehen wird individuell mit dem Betreuer besprochen.

Die Vorträge werden als Blockveranstaltung im Zeitraum Juni–August 2025 stattfinden. Termine werden später bekanntgegeben.

Die schriftliche Ausarbeitung ist bis zum 30. August 2024 einzureichen.

=== Prüfungsleistung und anrechenbare Module ===

'''Bachelor Informatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Diplom Informatik'''
* {{ModuleLink|INF-D-520}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Bachelor Medieninformatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

=== Kontakt ===

Bei organisatorischen Fragen wenden Sie sich bitte an [[Sascha Klüppelholz]].
}}

Proseminar “Theoretische Informatik” (SS2025)

2025-03-17T14:11:35Z

Andrea Kühn:

{{Vorlesung
|Title=Proseminar „Theoretische Informatik“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=DE
|Term=SS
|Year=2025
|Lecture series=Proseminar „Theoretische Informatik“
|Module=INF-B-610, INF-D-520
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=Das Proseminar richtet sich an Studierende der Studiengänge Bachelor und Diplom Informatik. Das Thema des Proseminars ist die Analyse von Algorithmen. Es werden u. a. Algorithmen aus den Büchern [https://mitpress.mit.edu/9780262046305/introduction-to-algorithms/ „Introduction to Algorithms“] von Cormen, Leiserson, Rivest und Stein, [https://www-cs-faculty.stanford.edu/~knuth/gkp.html „Concrete Mathematics“] von Graham, Knuth und Patashnik sowie [https://diestel-graph-theory.com/german/index.html „Graphentheorie“] von Diestel betrachtet.

Das Proseminar wird auf Deutsch abgehalten.

=== Registrierung ===

Die Teilnahme setzt eine Registierung [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027274/ via Opal] bis zum 14. April voraus.

=== Voraussetzungen ===

Neben dem Interesse an Theoretischer Informatik setzt das Proseminar solide Kenntnisse in den Gebieten Algorithmen und Datenstrukturen sowie Mathematik im Umfang der ersten zwei Studiensemester voraus.

=== Ablauf ===

Alle fristgerecht eingeschriebenen Teilnehmer:innen werden per E-Mail über die Einführungsveranstaltung informiert. In dieser wird allen Teilnehmer:innen je ein Thema und ein Betreuer zugeteilt. Das weitere Vorgehen wird individuell mit dem Betreuer besprochen.

Die Vorträge werden als Blockveranstaltung im Zeitraum Juni–August 2025 stattfinden. Termine werden später bekanntgegeben.

Die schriftliche Ausarbeitung ist bis zum 30. August 2024 einzureichen.

=== Prüfungsleistung und anrechenbare Module ===

'''Bachelor Informatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Diplom Informatik'''
* {{ModuleLink|INF-D-520}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

'''Bachelor Medieninformatik'''
* {{ModuleLink|INF-B-610}}: Seminararbeit (ca. 10 Seiten) inklusive Präsentation (30 Minuten)

=== Kontakt ===

Bei organisatorischen Fragen wenden Sie sich bitte an [[Sascha Klüppelholz]].
}}

Team Project “Model Checking” (SS2025)

2025-03-17T14:10:41Z

Andrea Kühn:

{{Vorlesung
|Title=Team Project “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Team Project “Model Checking”
|Module=CMS-LM-TEA
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Description=This course offers advanced topics in the field of formal modeling and analysis. It is meant for students enrolled in the Master's program “Computational Modeling and Simulation”. The tasks are usually taken from our current projects and cover programming and theoretical problems as well. Within this research-relevant project, students are working in teams of about 2 to 4 people to solve a complex interdisciplinary task that includes different areas of logical modeling and model checking.

This course is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027281 via Opal] is required until April 14.

=== Prerequisites ===

* Profound knowledge in model checking, acquired in the lecture “Model Checking” or similar courses at other universities
* Solid foundations in algorithms and data structures, in automata theory and formal languages as well as in complexity theory
* Basic mathematical foundations
* Programming skills in Java or C/C++ are beneficial, unless you are interested in a purely theoretical topic

=== Dates ===

Participants will be notified via e-mail about the initial meeting, where each group is assigned a topic. Presentations will be held between June and August. The specific dates will be announced later.

The written summary is due by August 30, 2025.

=== Exam and Creditability ===

* {{ModuleLink|CMS-LM-TEA}}: exam is according to the module description.

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Team Project “Model Checking” (SS2025)

2025-03-17T14:06:00Z

Andrea Kühn:

{{Vorlesung
|Title=Team Project “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Team Project “Model Checking”
|Module=CMS-LM-TEA
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Description=This course offers advanced topics in the field of formal modeling and analysis. It is meant for students enrolled in the Master's program “Computational Modeling and Simulation”. The tasks are usually taken from our current projects and cover programming and theoretical problems as well. Within this research-relevant project, students are working in teams of about 2 to 4 people to solve a complex interdisciplinary task that includes different areas of logical modeling and model checking.

This course is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027281 via Opal] is required until April 14.

=== Prerequisites ===

* Profound knowledge in model checking, acquired in the lecture “Model Checking” or similar courses at other universities
* Solid foundations in algorithms and data structures, in automata theory and formal languages as well as in complexity theory
* Basic mathematical foundations
* Programming skills in Java or C/C++ are beneficial, unless you are interested in a purely theoretical topic

=== Dates ===

Participants will be notified via e-mail about the initial meeting, where each group is assigned a topic. Presentations will be held between June and August. The specific dates will be announced later.

The written summary is due by August 30, 2025.

=== Exam and Creditability ===

The exam is according to the module description.

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Seminar “Selected Topics in Logic and Verification” (SS2025)

2025-03-17T13:52:34Z

Andrea Kühn:

{{Vorlesung
|Title=Seminar “Selected Topics in Logic and Verification”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Seminar “Selected Topics in Logic and Verification”
|Module=CMS-LM-ADV, CMS-LM-MOC, CMS-SEM, INF-AQUA, INF-D-940, MCL-PS, INF-B-510, INF-B-520
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=This seminar is mainly intended for students enrolled in the Master or Diplom programs Informatik (computer science).

This seminar is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027275?58 via Opal] is required until April 14.

=== Prerequisites ===

The seminar addresses students that have profound knowledge in theoretical computer science and logics.

=== Dates ===

All participants will be notified about the initital meeting by e-mail. Each participant is then assigned a topic and a supervisor.

Presentations will be held between June and August. The specific dates will be announced later. The seminar paper (Seminararbeit) is due by August 16.

=== Exam and Creditability ===

'''Bachelor Informatik'''
* {{ModuleLink|INF-B-510}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)
* {{ModuleLink|INF-B-520}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Informatik'''
* {{ModuleLink|INF-AQUA}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Medieninformatik'''
* {{ModuleLink|INF-AQUA}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Diplom Informatik'''
* {{ModuleLink|INF-D-940}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Computational Logic'''
* {{ModuleLink|MCL-PS}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-SEM}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)
* {{ModuleLink|CMS-LM-MOC}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)
* {{ModuleLink|CMS-LM-ADV}}: ''Seminararbeit inkl. Präsentation'' (a 10-page seminar paper and a 30-minute presentation)

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Lab Course “Modeling and Automated Verification” (SS2025)

2025-03-17T13:48:36Z

Andrea Kühn:

{{Vorlesung
|Title=Lab Course “Modeling and Automated Verification”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Lab Course “Modeling and Automated Verification”
|Module=CMS-LM-ADV, CMS-LM-MOC, MCL-PS
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=This lab course is intended for students in the Master's programs “Computational Logic” and “Computational Modeling and Simulation”. It offers 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 are part of current research projects of our workgroup. See for example:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* Symbolic methods in model checking
* Explicit model checking
* Reduction techniques
* Automata over finite and infinite words
* Numerical methods for quantitative analysis
* Logics
* Specification formalisms
* Abstraction techniques
* Case studies

This course is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027273/ via Opal] is required until April 14.

=== Prerequisites ===

* Solid foundations in algorithms and data structures, complexity theory, automata theory and formal languages
* Solid programming skills
* Basic mathematical foundations

=== Exam and Creditability ===

'''Master Computational Logic'''
* {{ModuleLink|MCL-PS}}: ''Projektarbeit inkl. Kolloquium'' (research project with a 10-page documentation and a 30-minute presentation)

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: ''Projektarbeit inkl. Kolloquium'' (research project with a 10-page documentation and a 30-minute presentation)
* {{ModuleLink|CMS-LM-ADV}}: ''Projektarbeit inkl. Kolloquium'' (research project with a 10-page documentation and a 30-minute presentation)

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Research Seminar “Formal Methods” (SS2025)

2025-03-17T13:35:13Z

Andrea Kühn:

{{Vorlesung
|Title=Research Seminar “Formal Methods”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Research Seminar “Formal Methods”
|Module=INF-PM-FOR
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=This seminar is mainly intended for students enrolled in the Master or Diplom programs Informatik (computer science). Participants engage with selected topics from the field of Model Checking.

This course is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027282/ via Opal] is required until April 14.

=== Prerequisites ===

The seminar addresses students that have profound knowledge in theoretical computer science and logics. Background knowledge in the areas of formal methods (and model checking in particular) or concurrency theory is recommended.

=== Dates ===

All participants will be notified about the initital meeting by e-mail.

=== Exam and Creditability ===

* {{ModuleLink|INF-PM-FOR}}: exam according to module description

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Profilprojekt “Research Project Formal Methods” (SS2025)

2025-03-17T13:27:14Z

Andrea Kühn:

{{Vorlesung
|Title=Profilprojekt „Forschungsprojekt Formale Methoden“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=SS
|Year=2025
|Lecture series=Profilprojekt „Forschungsprojekt Formale Methoden“
|Module=INF-PM-FPG
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Description=The introductory project (Profilprojekt) is intended for students enrolled in the Master or Diplom programs Informatik (computer science). Participants study selected topics from the fields of model checking, automata theory and logics. The purpose is to acquire skills for their research-oriented specialization and independent research work.

This course is offered in German and English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027279 via Opal] is required until April 14.

=== Exam and Creditability ===

'''Master Informatik'''
* {{ModuleLink|INF-PM-FPG}}: exam according to module description

'''Diplom Informatik'''
* {{ModuleLink|INF-PM-FPG}}: exam according to module description

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Lab Course “Modeling and Automated Verification” (SS2025)

2025-03-17T12:47:42Z

Andrea Kühn:

{{Vorlesung
|Title=Lab Course “Modeling and Automated Verification”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Lab Course “Modeling and Automated Verification”
|Module=CMS-LM-ADV, CMS-LM-MOC, MCL-PS
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Description=This lab course is intended for students in the Master's programs “Computational Logic” and “Computational Modeling and Simulation”. It offers 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 are part of current research projects of our workgroup. See for example:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* Symbolic methods in model checking
* Explicit model checking
* Reduction techniques
* Automata over finite and infinite words
* Numerical methods for quantitative analysis
* Logics
* Specification formalisms
* Abstraction techniques
* Case studies

This course is held in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027273/ via Opal] is required until April 14.

=== Prerequisites ===

* Solid foundations in algorithms and data structures, complexity theory, automata theory and formal languages
* Solid programming skills
* Basic mathematical foundations

=== Exam and Creditability ===

'''Master Computational Logic'''
* {{ModuleLink|MCL-PS}}: ''Projektarbeit inkl. Kolloquium'' (research project with 10 page documentation including a 30 minute presentation)

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: ''Projektarbeit inkl. Kolloquium'' (research project with 10 page documentation including a 30 minute presentation)
* {{ModuleLink|CMS-LM-ADV}}: ''Projektarbeit inkl. Kolloquium'' (research project with 10 page documentation including a 30 minute presentation)

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Komplexpraktikum „Modellierung und quantitative Systemanalyse II“ (SS2025)

2025-03-17T12:43:57Z

Andrea Kühn:

{{Vorlesung
|Title=Komplexpraktikum „Modellierung und quantitative Systemanalyse Ⅱ“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=SS
|Year=2025
|Module=INF-MA-PR
|SWSLecture=0
|SWSExercise=0
|SWSPractical=8
|Description=The course is intended for students enrolled in the Master or Diplom programs Informatik (computer science) as well as for those enrolled in the Diplom program Informationssystemtechnik (information systems engineering). The Komplexpraktikum “Modeling and Quantitative System Analysis I” allows students to analyse and work on practical projects relevant in current research. Some topics are taken from current projects of the group. The following links give more information on these projects:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* Symbolic methods in model checking
* Explicit model checking
* Reduction techniques
* Automata over finite and infinite words
* Numerical methods for quantitative analysis
* Logics
* Specification formalisms
* Abstraction techniques
* Case studies

This course is offered in German and English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027278 via Opal] is required until April 14.

=== Prerequisites ===

In addition to an interest in theoretical computer science, the project requires solid knowledge of model checking and programming. Experience in C/C++ or Java is helpful, but not required.

=== Dates ===

All enrolled participants will be notified about the initial meeting by e-mail. The specific dates will be announced later.

=== Exam and Creditability ===

'''Master Informatik'''
* {{ModuleLink|INF-MA-PR}}: exam according to module description

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Komplexpraktikum „Modellierung und quantitative Systemanalyse I“ (SS2025)

2025-03-17T12:42:43Z

Andrea Kühn:

{{Vorlesung
|Title=Komplexpraktikum „Modellierung und quantitative Systemanalyse Ⅰ“
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier
|Language=DE,EN
|Term=SS
|Year=2025
|Module=INF-MA-PR
|SWSLecture=0
|SWSExercise=0
|SWSPractical=4
|Description=The course is intended for students enrolled in the Master or Diplom programs Informatik (computer science) as well as for those enrolled in the Diplom program Informationssystemtechnik (information systems engineering). The Komplexpraktikum “Modeling and Quantitative System Analysis I” allows students to analyse and work on practical projects relevant in current research. Some topics are taken from current projects of the group. The following links give more information on these projects:

* [https://www.perspicuous-computing.science/ CPEC]
* [https://ceti.one/ CeTI]
* [https://secai.org/de SECAI]
* [https://digitalhealth.tu-dresden.de/projects/semeco/ SEMECO]
* [http://5glab.de/ 5G-Lab Germany]

Potential topics include:
* Symbolic methods in model checking
* Explicit model checking
* Reduction techniques
* Automata over finite and infinite words
* Numerical methods for quantitative analysis
* Logics
* Specification formalisms
* Abstraction techniques
* Case studies

This course is offered in German and English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027276/ via Opal] is required until April 14.

=== Prerequisites ===

In addition to an interest in theoretical computer science, the project requires solid knowledge of model checking and programming. Experience in C/C++ or Java is helpful, but not required.

=== Dates ===

All enrolled participants will be notified about the initial meeting by e-mail. The specific dates will be announced later.

=== Exam and Creditability ===

'''Master Informatik'''
* {{ModuleLink|INF-MA-PR}}: exam according to module description

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

CMS Research Project “Model Checking” (SS2025)

2025-03-17T12:18:29Z

Andrea Kühn:

{{Vorlesung
|Title=CMS Research Project “Model Checking”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Sascha Klüppelholz
|Language=EN
|Term=SS
|Year=2025
|Lecture series=CMS Research Project “Model Checking”
|Module=CMS-PRO
|SWSLecture=0
|SWSExercise=0
|SWSPractical=12
|Description=This course offers advanced topics in the field of verification and model checking. It is meant for students enrolled in the Master's program “Computational Modeling and Simulation”. The tasks are usually taken from our current projects and cover programming and theoretical problems as well.

This course is in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027280 via Opal] is required until April 14.

=== Prerequisites ===

* Profound knowledge in model checking, acquired in the lecture “Model Checking” or similar courses at other universities
* Solid foundations in algorithms and data structures, in automata theory and formal languages as well as in complexity theory
* Basic mathematical foundations
* Programming skills in Java or C/C++ are beneficial, unless you are interested in a purely theoretical topic

=== Dates ===

All enrolled participants will be notified about the initital meeting by e-mail.

=== Exam and Creditability ===
'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-PRO}}: exam according to module description

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Advanced Logics (SS2025)

2025-03-17T12:13:41Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Advanced Logics”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier; Jakob Piribauer
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Advanced Logics
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-AL
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Description=The purpose of this course is to study several extensions of classical propositional, first-order and second-order logic. We will concentrate on aspects of mathematical logic that are relevant for computer science, such as expressiveness, game-theoretic characterizations, deductive calculi, decision and transformation algorithms and computational complexity.

This lecture is in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027272?29 via Opal] is required until April 30.

=== Prerequisites ===

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===
* Lecture: Thursdays and Fridays, 9:20–10:50, APB E005 (starting April 10)
* Tutorial: Thursdays, 11:10–12:40, APB E005 (starting April 17)

=== Creditability ===
'''Bachelor Informatik'''
* {{ModuleLink|INF-B-510}}: oral exam (30 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (30 minutes)

'''Master Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-AL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: oral exam (30 minutes)
* {{ModuleLink|CMS-LM-ADV}}: oral exam (30 minutes)

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Andrea Kühn

2025-03-17T12:00:39Z

Andrea Kühn:

{{Mitarbeiter
|Vorname=Andrea
|Nachname=Kühn
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
|Stellung=Sekretärin
|Ehemaliger=0
|Telefon=+49 351 463 38549
|Email=secretary_alg@mailbox.tu-dresden.de
|Raum=APB 3005
|Bild=Andrea.jpeg
|Publikationen anzeigen=0
|Abschlussarbeiten anzeigen=0
}}

Algebraische und logische Grundlagen der Informatik

2025-03-17T11:59:43Z

Andrea Kühn:

{{Forschungsgruppe
|Name EN=Algebraic and Logical Foundations of Computer Science
|Kurzname=ALG
|Beschreibung DE=Die Forschungsgruppe ''Algebraische und logische Grundlagen der Informatik'' beschäftigt sich mit der Modellierung, Spezifikation und Verifikation reaktiver Systeme. Zu den Forschungsschwerpunkten gehören die formale Analyse und Synthese stochastischer Systeme sowie Konzepte der Erklärbarkeit im Kontext formaler Methoden. Weitere Forschungsthemen sind Automatentheorie, temporale und modale Logiken, Spieltheorie und dynamische Systeme.
|Beschreibung EN=The chair of ''Algebraic and Logical Foundations of Computer Science'' researches the modeling, specification and verification of reactive systems. The focus is on the formal analysis and synthesis of stochastic systems and on explainability in the context of formal methods. Further areas of research include automata theory, temporal and modal logics, game theory and dynamic systems.
|Forschungsgruppenleiter=Christel Baier
|Sekretariat Mail=secretary_alg@mailbox.tu-dresden.de
|Bild=Gruppenfoto.jpeg
|Ehemalige Forschungsgruppe=0
|Name DE=Algebraische und logische Grundlagen der Informatik
|Anzahl Lehrveranstaltungen in Tab=11
|Lehrveranstaltungen als Boxen anzeigen=true
}}

Advanced Logics (SS2025)

2025-03-14T12:42:07Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Advanced Logics”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier; Jakob Piribauer
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Advanced Logics
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-AL
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Description=The purpose of this course is to study several extensions of classical propositional, first-order and second-order logic. We will concentrate on aspects of mathematical logic that are relevant for computer science, such as expressiveness, game-theoretic characterizations, deductive calculi, decision and transformation algorithms and computational complexity.

This lecture is in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027272?29 via Opal] is required until 30 April.

=== Prerequisites ===

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===
* Lecture: Thursdays and Fridays, 9:20–10:50, APB E005 (starting 10 April)
* Tutorial: Thursdays, 11:10–12:40, APB E005 (starting 17 April)

=== Creditability ===
'''Bachelor Informatik'''
* {{ModuleLink|INF-B-510}}: oral exam (30 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (30 minutes)

'''Master Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-AL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: oral exam (30 minutes)
* {{ModuleLink|CMS-LM-ADV}}: oral exam (30 minutes)

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}

Advanced Logics (SS2025)

2025-03-14T12:41:42Z

Andrea Kühn:

{{Vorlesung
|Title=Lecture “Advanced Logics”
|Research group=Algebraische und logische Grundlagen der Informatik
|Lecturers=Christel Baier, Jakob Piribauer
|Language=EN
|Term=SS
|Year=2025
|Lecture series=Advanced Logics
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-B-510, INF-B-520, INF-BAS6, INF-VERT6, MCL-AL
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Description=The purpose of this course is to study several extensions of classical propositional, first-order and second-order logic. We will concentrate on aspects of mathematical logic that are relevant for computer science, such as expressiveness, game-theoretic characterizations, deductive calculi, decision and transformation algorithms and computational complexity.

This lecture is in English.

=== Registration ===

Registration [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/48422027272?29 via Opal] is required until 30 April.

=== Prerequisites ===

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

=== Dates ===
* Lecture: Thursdays and Fridays, 9:20–10:50, APB E005 (starting 10 April)
* Tutorial: Thursdays, 11:10–12:40, APB E005 (starting 17 April)

=== Creditability ===
'''Bachelor Informatik'''
* {{ModuleLink|INF-B-510}}: oral exam (30 minutes)
* {{ModuleLink|INF-B-520}}: oral exam (30 minutes)

'''Master Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Diplom Informatik'''
* {{ModuleLink|INF-BAS6}}: exam according to module description
* {{ModuleLink|INF-VERT6}}: exam according to module description

'''Master Computational Logic'''
* {{ModuleLink|MCL-AL}}: exam according to module description

'''Master Computational Modeling and Simulation'''
* {{ModuleLink|CMS-LM-MOC}}: oral exam (30 minutes)
* {{ModuleLink|CMS-LM-ADV}}: oral exam (30 minutes)

=== Contact ===

Please contact [[Sascha Klüppelholz]] for organisational questions.
}}