Kursinformation

When 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.