Research Fellows Directory
Dr Vaclav Brozek
University of Edinburgh
Formal verification is a rapidly evolving part of computer science, enjoying strong focus recently but dating back to the beginnings of computer science itself. Is it the seminal work of Turing on halting problem in the first half of 20th century, or some late study on parity games, the central motivation stays the same -- Can we formulate and prove important properties about programs, ideally using an automated system? Faults in computer programs are annoying, very often costly, and sometimes even fatal to people's lives. The classical approach of testing is to try to run the program on a variety of inputs, hoping for discovering a design error. However, this can never be 100% fault proof since there are infinitely many possible inputs. The task of formal verification is to design classes of properties and formalisations of systems such that given a system and a property, one can algorithmically determine whether the system satisfies the property. Both on the side of properties and on the side of system formalisations, there is always a trade-off between the expressibility and decidability -- the more interesting properties we allow to formulate, the more difficult (or even impossible) it will be to check them.
A special kind of formal verification is verification of recursive stochastic games. This formalism is very rich, it allows to describe a system with uncertainty (e.g. measurements), controlled behaviour (e.g. driver), and adversarial behaviour (e.g. non-predictable user), along with unbounded recursion, leading to infinite state space. We study optimization problems of these systems, i.e. we ask what is the maximal probability of some desired, or the minimal probability of some undesired event. This is already on the edge of decidability, even for very simple properties, and fine tuning of the model leads surprisingly to both undecidable classes and tractable classes of such problems.