direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content

Summer Term 2020

In this module, tools that are often used in industry are used for an automatic analysis of parts of real software. The lecture gives an introduction into formal, tool-supported verification of C programs. The whole programming language C, in the amount that is used to program operating system components, is considered. The analysis includes simple function specifications, invariants, memory safety, functional correctness and the correctness of concurrent programs. Examples in the lecture and exercises are performed with the verification tool VCC, which was developed at Microsoft Research.
Furthermore, the lecture presents the technical and academic progress that - starting from the Hoare calculus - brought verification of C programs into practice.
The course is held in English.
Course Data
Course type and credit points
3 credit points, ECTS (2 SWS integrated course)
Master of Science Computer Science
Compulsory elective course
Master of Science Computer Engineering
Compulsory elective course

see ISIS
see ISIS
Online Application
via ISIS
Module description

Supporting Material

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe

Auxiliary Functions