Current Topics of Modular Verification

Form: Seminar - 3 CP (2 SWS)
Organizer: Prof. Dr. Heiko Mantel
Contact: Thomas Höhl
Time and place: Block seminar on 30.01.20 and 31.01.20
Language: English
Registration: via TUCaN, course id 20-00-1077-se
Max. participants: 12
Preparation Meeting: Thursday, 17.10.2019, 16:00 in room S2|02 A213

Material

Will be made available in the course internal area.

Content

CTMV-SeminarWhen designing software systems, correctness is a key feature. Bugs do not only lead to costs, but can, in the worst case, even endanger human lives (e.g. software in planes, space ships, nuclear reactors, ...). Verification of software can be used to show the absence of bugs.

A key question hereby is how to make formal verification and testing scale for complex systems. The complexity of analyses can arise from multiple factors, e.g., the program size or the number of concurrent threads. Modular verification tackles this complexity with decomposition. The system components are verified separately and the verification results are composed to guarantees for the whole system. This composition of verification results must be supported by compositionality results to ensure that the modular analysis is trustworthy.

In this seminar, current research articles that focus on different techniques used for modular verification are presented and discussed in detail.

Learning Objectives

After successful participation in this course, students will be able to discuss selected developments in modular verification. Furthermore, students will have improved their skills in reading and understanding scientific articles, in presenting scientific results, and in scientific discussions.

Prerequisites

Knowledge of Computer Science and Mathematics equivalent to the first four semesters in the Computer Science Bachelor program, in particular the ability to use formal languages and calculi.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang