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 tools.
The aim of the game
The goal is to educate students on the concepts of algorithmic verification and give them hands-on experience in verification tools.
Technical
To 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
- advanced verification techniques for timed and probabilistic systems.
Educational
Expose students 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.
Course website
- General information and formal notices with respect to enrolment and exams.
- Lectures with dates and handouts.
- Assignments and related information.
- Resources such a tools and literature.