To content
Fakultät für Informatik
Bachelor's module

Proseminar: Software Verification


Module INF-BSc-110
Type Proseminar
Credits 2 Credits (Seminar)
1 Credit (Presentation)

Today, software determines many areas of our daily lives. Some examples that most of us come into contact with on a daily basis are smartphone apps (e.g. for communicating with friends), software in ATMs, POS systems, smartcards and assistance systems in vehicles. For the above examples and many other applications, it is important that software functions correctly. For safety-critical systems, it is often not sufficient to test software: Testing can only reveal errors, but not prove the absence of errors. Instead, formal methods for specification and verification are used.

Software verification proves the correctness of an algorithm with respect to a formal requirement specification. In the proseminar, different approaches to the formal specification of software systems (e.g., automata, transition systems, and process algebras) and requirements for software systems (e.g., temporal logics) as well as methods for formal verification (e.g., model checking, theorem provers) are considered.

Literature / Links

The material (slides, literature, exercises) is provided in the TU Dortmund Moodle. Registration in LSF is mandatory and automatically perfoms enrolment in the Moodle.

Note on the language
The literature for the proseminar will be in English only. Presentations and papers may be in English or German.