622.051 (19W) Spezifikation und Verifikation
Überblick
- Lehrende/r
- LV-Titel englisch Specification and Verification
- LV-Art Übung (prüfungsimmanente LV )
- Semesterstunde/n 2.0
- ECTS-Anrechnungspunkte 4.0
- Anmeldungen 18 (35 max.)
- Organisationseinheit
- Unterrichtssprache Englisch
- mögliche Sprache/n der Leistungserbringung Englisch
- LV-Beginn 05.10.2019
- eLearning zum Moodle-Kurs
Zeit und Ort
LV-Beschreibung
Intendierte Lernergebnisse
Please note that this course is a blocked course. Each block will be of approx. 4 hours and will take place once in every month (i.e. October, November, December and January). The anticipated meeting dates are October 5, 2019, November 9, 2019, December 14, 2019 and January 13, 2020. This course will start at noon (12:30pm-4:00pm).
The learning outcome of this course includes mastering the practical aspects of
- the foundations of logic based proving techniques,
- the various formal methods for program verification,
- the logic based specification and verification of sequential and concurrent programs,
- the specification and verification of Java programs and
- state-of-the-art (programming) tools (OpenJML and Spin model checker) that support program verification and model checking.
Lehrmethodik inkl. Einsatz von eLearning-Tools
The teaching method will be practical and online exercises in the classroom.
Inhalt/e
The background theoretical contents of this course are taught in 622.050.
The course will include the practicing of basics and advanced of the following topics
- logic and proving
- various formal methods
- logic based specification
- program verification
- specification and verification of sequential programs, for instance, verifying Java programs specified in Java Modeling Language and
- specification and verification of concurrent programs, for instance, using Spin model checker
Importantly, the course will help students to master practical tools for the verification of industrial applications developed in popular programming languages.
Erwartete Vorkenntnisse
Some intuitive knowledge of logic and proving is helpful. However, reasonable programming skills are desired.
Importantly, the lecture course 622.050 is required to understand the background theory that is required to solve practical exercises of this course.
Literatur
Similar to the lectures taught in 622.050.
Prüfungsinformationen
Prüfungsmethode/n
The exam method of this course will be based on ONLY practical exercises. Six (6) exercises will be handed out in total and the best 5 will count for final grading.
Prüfungsinhalt/e
Almost every theme that is taught in the lecture part of this course (622.050) will have an associated lab exercise.
Beurteilungskriterien/-maßstäbe
The exam mode will be ONLY course work submissions which will be based on study of the lecture material, learning tools and developing exercises in those tools.
Beurteilungsschema
Note BenotungsschemaPosition im Curriculum
- Diplom-Lehramtsstudium Unterrichtsfach Informatik und Informatikmanagement
(SKZ: 884, Version: 04W.7)
-
2.Abschnitt
-
Fach: Angewandte Informatik (LI 2.3)
(Pflichtfach)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
- 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
-
Fach: Angewandte Informatik (LI 2.3)
(Pflichtfach)
-
2.Abschnitt
- Bachelorstudium Angewandte Informatik
(SKZ: 511, Version: 19W.2)
-
Fach: Softwareentwicklung
(Wahlfach)
-
8.8 Softwareentwicklung (
0.0h XX / 12.0 ECTS)
- 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS) Absolvierung im 4., 5., 6. Semester empfohlen
-
8.8 Softwareentwicklung (
0.0h XX / 12.0 ECTS)
-
Fach: Softwareentwicklung
(Wahlfach)
- Bachelorstudium Angewandte Informatik
(SKZ: 511, Version: 17W.1)
-
Fach: Softwareentwicklung
(Wahlfach)
-
6.4 Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
- 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
-
6.4 Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
-
Fach: Softwareentwicklung
(Wahlfach)
- Bachelorstudium Angewandte Informatik
(SKZ: 511, Version: 12W.1)
-
Fach: Softwareentwicklung
(Wahlfach)
-
Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
- 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
-
Fach: Softwareentwicklung
(Wahlfach)
- Masterstudium Angewandte Informatik
(SKZ: 911, Version: 13W.1)
-
Fach: Vertiefung Informatik
(Pflichtfach)
-
Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
- 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
-
Fach: Vertiefung Informatik
(Pflichtfach)
- Masterstudium Mathematics
(SKZ: 401, Version: 18W.1)
-
Fach: Informatics
(Wahlfach)
-
8.6 Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
- 622.051 Spezifikation und Verifikation (2.0h UE / 4.0 ECTS)
-
8.6 Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
-
Fach: Informatics
(Wahlfach)
Gleichwertige Lehrveranstaltungen im Sinne der Prüfungsantrittszählung
-
Wintersemester 2023/24
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2022/23
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2021/22
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2020/21
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2018/19
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2017/18
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2016/17
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2015/16
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2014/15
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2013/14
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2012/13
- 622.051 PR Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2010/11
- 622.051 PR Spezifikation und Verifikation (2.0h / 4.0ECTS)
- Wintersemester 2009/10