Software Verification

The course teaches concepts in the area of automated formal verification of software. The focus of the course is on methods that map the verification problem to a logical satisfiability problem or into an automata-based representation.

As a basis for the automation of the considered verification methods, the mechanization of formal logic is discussed and corresponding algorithmic results are studied. In the area of verification of programs, deductive and inductive methods are compared. Starting from classical Hoare logic and simple search, e.g., methods generating inductive invariants during verification are considered. In the area of verification of software components, methods that generate formal behavior models from implementations are discussed, as well as methods that check logical properties on behavior models (e.g., automata).

In addition to the study of algorithmic results, the use of tools that implement the presented concepts is trained.

Competencies 

Students will acquire basic knowledge of logics and algorithms for finding models for logical formulas relevant in the field of software verification. They will learn to compare and apply verification methods, analyze usage scenarios and learn to critically select a suitable verification method and algorithms. In addition, students will be trained in evaluating and using (research) tools in the area of software verification. 

Students will gain an overview of selected parts of current research and learn fundamentally how to access current research contributions in the area of formal methods on their own. 

Module type and applicability of the module 

• Advanced module in the master programs Computer Science and Applied Computer Science
• Research Area: Software, Security and Verification 

Material

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