I870 – Formal Verification

Module
Formal Verification
Formale Verifikation
Module number
I870 [I-870]
Version: 1
Faculty
Informatics/Mathematics
Level
Master
Duration
1 Semester
Semester
Summer semester
Module supervisor

Prof. Dr. rer. nat. Boris Hollas
boris.hollas(at)htw-dresden.de
Lecturer(s)

Prof. Dr. rer. nat. Boris Hollas
boris.hollas(at)htw-dresden.de
Course language(s)
ECTS credits

5.00 credits

Workload

150 hours

Courses

4.00 SCH (2.00 SCH Lecture | 1.00 SCH Seminar | 1.00 SCH Internship)
Self-study time

0.00 hours

Pre-examination(s)
None
Examination(s)

Oral examination
Examination time: 30 min | Weighting: 100%
in "Formale Verifikation"
Form of teaching

2/1/1  V/Ü/P
Media type
No information
Instruction content/structure
  • Temporale Logik: Syntax und Semantik von LTL, Transitionssysteme.
  • Model Checking mit Spin: Sprachelemente von Promela, nebenläufige Systeme, Kommunikationsprotokolle.
  • Software-Model-Checking durch SAT-Solving.
  • Abstrakte Interpretation: Halbordnungen, Verbände, abstrakte und konkrete Semantik, abstrakte Verbände, Kontrollflussgraphen. Anwendungen mit Microsoft Code Contracts.
Qualification objectives

Die formale Verifikation umfasst Verfahren, mit denen Fehler
in Hard- und Software frühzeitig erkannt und die Abwesenheit
von Fehlern garantiert werden kann. Seit einigen Jahren werden
diese Verfahren zur Verifikation von Kommunikationsprotokollen,
integrierten Schaltkreisen und sicherheitskritischer Software
erfolgreich eingesetzt.
Social and personal skills
No information
Special admission requirements
No information
Recommended prerequisites
No information
Continuation options
No information
Literature
  • Huth, Ryan: Logic in Computer Science, 2004.
  • Ben-Ari: Principles of the Spin Model Checker, 2007.
Current teaching resources

-
Notes
No information
Link to course/learning resources in OPAL
Close detail view
© Modulux (Version 4.3)