Formal Verification of Systems

The problem of correctness, i.e., the problem to verify that a given computer system (hardware and/or software) really has some properties required by a its specification, is one of the most fundamental practical and theoretical problems in computer science.
The goal of the course is to show to students some approaches used for verification of systems.

One of methods, successful in practice, is model checking where a tested property of system is expressed using a formula of some of so called temporal logics, and verification is done using (semi)automated methods on a model of a system.

Other example of methods, used in practice, is so called equivalence checking where we have a model representing a specification of behaviour of the system, i.e., what is expected as a desired behaviour, and a model representing implementation, i.e., how the desired behaviour is implemented in practice. The goal is to determine whether the behaviours of both models is equivalent
in some precisely defined sense, which would mean that the given implementation
really behaves according to the specification.

Other approach is based on creating proof of correctness of programs in some system for interactive and automated theorem proving. There exist several different software tools that allow to create proofs interactively while they check the correctness of these proofs automatically, and to some extend they also allow to automate some routine steps of the proofs. This area is also closely connected with problems concerning semantics of programming languages and type theory because to be able to create proofs of correctness of programs, at first we need a formally represented semantics of programs. So some of the lectures will deal with this topic. There will be also studied
logics used for proving properties of programs - Hoare logic and separation logic (which is a modern and more general extension of Hoare logic that allows to prove correctness of programs that work with pointers and dynamically allocated structures).

The purpose of the course is an explanation of basic principles of these approaches to verification, and also a demonstration of such
verification on models of concrete practical problems using freely available tools.

Results of learning:
- To get acquainted with some methods used for verification of systems.
In particular, to know approaches based on model checking, approaches based on equivalence checking, and approaches using tools for interactive a automated theorem proving.
- To know different mathematical formalisms used for verification. In particular, how semantics of programs and programming languages can be described and represented formally. To know some examples of logics used for specification of properties of systems such as different types of temporal logics and logics used for program verification such as Hoare logic and separation logic. To obtain a basic knowledge of type theory.