Software Verification

Overview

The increasing complexity of modern computer systems makes the development of correct software very challenging. A successful approach to master this challenge is formal verification which proves that the implementation of a system fulfills its specification or which shows that the implementation is buggy.

In this course, we will cover state-of-the-art topics on software verification as used in huge software companies. Examples of topics are bounded model checking, symbolic execution.

Organization

• This course will be blocked (see KUSSS).
• There will be a lecture part providing the necessary background on theory and tools.
• In a hands-on exercise part recent verification tools will be applied.

Course Material

Slides of the lecture will be provided.

• Model Checking
• Separation Logic
• KLEE examples and quick setup description (tar.gz and zip)
• Infer examples and quick setup description (tar.gz and zip)

Contact

For questions, contact Martina Seidl, Katalin Fazekas, or Armin Biere.