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.

Bsc. student 2018: "The assignment-focused learning process he adopted really worked well for helping me to learn and keeping me disciplined on reviewing and reading materials. It was a good aid."

MSc. student 2018: "I liked the smaller lecture, the enthusiasm of the lecturer for the subject matter. While I thought this was the highest volume of assignments for any course I did in the first semester by quite a stretch, it was the course I also learnt the most interesting and novel content from doing. All the assignments are carefully marked and feed backs are given."

MSc. student 2017: "It's changllenging and substantial. Assignments are always returned in time with feedbacks provided. Interactive teaching, lecturer gives a lot of problem example to understand the material"

BSc. student 2017: "The content was pretty cool. Glad to know how much of this stuff exists. Fix Points are cool."

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.

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—2018