URL study guide
https://tue.osiris-student.nl/onderwijscatalogus/extern/cursus?cursuscode=2IMP10&collegejaar=2026&taal=enDescription
1. System modelling and verification of temporal logic formulas using model checking.2. Software verification by means of abstraction-refinement, bounded model checking and automatic test suite generation.
3. (Automated) code annotation checking techniques, algorithms and tooling that use (Hoare-style) function contracts.
Objectives
The purpose of the course is to provide an overview of the available formal methods techniques to verify the correctness of programs. The focus is on the user-level, meaning that more attention is given to how the various techniques can be applied than on the algorithms used by those techniques, although we will also look at the basic principles of the algorithms. The learning outcomes are that after finishing the course, students should be able to- know the pros and cons of the various types of formal verification techniques, and recognise when to use which technique.
- apply in practice: 1) a symbolic model checker, 2) a software model checker, 3) an automatic test suite generator, 4) a code verifier.
- apply the theory of:
3.1. LTL and CTL model checking.
3.2. predicate abstraction and abstraction-refinement.
3.3. bounded model checking.
3.4. assertional verification. - explain the meaning of a logical formula.
- formalise system properties using temporal logics, propositional logic, first-order logic, Hoare logic.
- construct a formal model of a software system.