What is algorithmic verification about?

It is virtually impossible to guarantee correctness of a system, and in turn the absence of bugs by standard software engineering practice such as code review, systematic testing and good software design alone. The complexity of systems is typically too high to be manageable by informal reasoning or reasoning that is not tool supported. The formal methods community has developed various rigorous, mathematically sound techniques and tools that allow the automatic analysis of systems and software. The application of these fully automatic techniques is typically called algorithmic verification. The course will describe several automatic verification techniques, the algorithms they are based on, and the tools that support them. We will discuss examples to which the techniques have been applied, and provide experience with the use of several state-of-the-art analysis tools.

Objectives of the course

The goal is to educate students on the concepts of algorithmic verification and give them hands-on experience in modern verification tools.

Technical aspects covered

The topics covered by the lectures will educate students on the foundations of automata theory and temporal logics, LTL and CTL model checking techniques and model checking tools, the application of static analysis techniques to program verification, and modern advanced verification techniques for timed and probabilistic systems.

During the course, students are exposed to a scientific theory of algorithmic verification techniques, the underlying concepts for state-of-the-art tools, and sound frameworks for program analysis.

Course philosophy and teaching strategies

The learning focus in this course is primarily on lectures and assignments, plus a mid term project which you can use to demonstrate your skills acquired until then. While marks are assigned to the assignments, their primary purpose is to give you concrete tasks with deadlines to help you structure your learning.

MSc. student 2016: "An excellent introduction to algorithmic verification. This course began with almost no prerequisite knowledge (only competency with logic and the ability to quickly pick up the concept of an automata was necessary), but built up a very sound understanding of how model checking works from a low level abstract mathematical model, to a formalized high level specification. As well, both details and an intuitive understanding of all concepts was provided to address all levels of understanding."
Msc. student 2016: "Very interesting and challenging."

BSc. student 2013: "I have learnt a lot during this course and will definitely recommend it to CS students who want to acquire solid basis in modelling and verification."
Ph.D. student 2013: "The course covers advanced material in the area of automated verification. It provides a clear and comprehensive overview of modern verification techniques."


Copyright 2015—2017