622.051 (17W) Specification and Verification
Overview
- Lecturer
- Course title german Spezifikation und Verifikation
- Type Practical class (continuous assessment course )
- Hours per Week 2.0
- ECTS credits 4.0
- Registrations 33 (35 max.)
- Organisational unit
- Language of instruction English
- possible language(s) of the assessment English
- Course begins on 03.10.2017
- eLearning Go to Moodle course
Time and place
Course Information
Intended learning outcomes
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.
Teaching methodology including the use of eLearning tools
The teaching method will be practically exercises in the classroom.
Course content
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.
Prior knowledge expected
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.
Literature
Similar to the lectures taught in 622.050.
Examination information
Examination methodology
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.
Examination topic(s)
Almost every theme that is taught in the lecture part of this course (622.050) will have an associated lab exercise.
Assessment criteria / Standards of assessment for examinations
The exam mode includes study of the lecture material, learning tools and developing exercises in those tools.
Grading scheme
Grade / Grade grading schemePosition in the curriculum
- Teacher training programme Computer Sciences and Computer Sciences Management (Secondary School Teacher Accreditation)
(SKZ: 884, Version: 04W.7)
-
Stage two
-
Subject: Angewandte Informatik (LI 2.3)
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
-
Subject: Angewandte Informatik (LI 2.3)
(Compulsory subject)
-
Stage two
- Bachelor's degree programme Applied Informatics
(SKZ: 511, Version: 17W.1)
-
Subject: Software Development
(Compulsory elective)
-
6.4 Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
6.4 Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
-
Subject: Software Development
(Compulsory elective)
- Bachelor's degree programme Applied Informatics
(SKZ: 511, Version: 12W.1)
-
Subject: Software Development
(Compulsory elective)
-
Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
-
Subject: Software Development
(Compulsory elective)
- Bachelorstudium Informatik
(SKZ: 521, Version: 09W.3)
-
Subject: Spezifikation und Verifikation
(Compulsory elective)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
-
Subject: Spezifikation und Verifikation
(Compulsory elective)
- Bachelor's degree programme Informatics
(SKZ: 521, Version: 03W.1)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
- Master's degree programme Applied Informatics
(SKZ: 911, Version: 13W.1)
-
Subject: Vertiefung Informatik
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h UE / 4.0 ECTS)
-
Subject: Vertiefung Informatik
(Compulsory subject)
- Masterstudium Informatik
(SKZ: 921, Version: 09W.1)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
- Master's degree programme Informatics
(SKZ: 921, Version: 03W.1)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
-
Subject: Spezifikation und Verifikation
(Compulsory subject)
- Diploma programme Informatics
(SKZ: 880, Version: 02W)
-
Stage two
-
Subject: Angewandte Informatik inkl. Vertiefungsfach
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
-
Subject: Angewandte Informatik inkl. Vertiefungsfach
(Compulsory subject)
-
Stage two
- Diploma programme Informatics
(SKZ: 880, Version: 02W)
-
Stage three
-
Subject: Angewandte Informatik und Vertiefungsfach
(Compulsory subject)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
- 622.051 Specification and Verification (2.0h UE / 4.0 ECTS)
-
Spezifikation und Verifikation (
2.0h PR / 4.0 ECTS)
-
Subject: Angewandte Informatik und Vertiefungsfach
(Compulsory subject)
-
Stage three
Equivalent courses for counting the examination attempts
-
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 2019/20
- 622.051 UE Spezifikation und Verifikation (2.0h / 4.0ECTS)
-
Wintersemester 2018/19
- 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