Research Fellows Directory
Dr Stefan Kiefer
University of Oxford
Computers are now ubiquitous: they are embedded in mobile phones, airplanes, medical devices, among many others. Consequently our dependence on them has increased dramatically, and the failure of so-called safety-critical systems may lead to catastrophic consequences and enormous economic damage.
Computer systems have become far too complex to analyse by hand. However their correctness and performance can be systematically analysed with the help of specialised programs, including so-called model checkers and theorem provers. The field of computer-aided verification is based on this idea. Making this technique scalable and applying it as widely as possible has been identified as a Grand Challenge by the famous computer scientist Sir Tony Hoare, and research in the field has led among others to four Turing awards (the "Nobel prize of computing") to date.
Modern embedded computer systems interact directly with the physical world. As a consequence, the focus of engineers and researchers has shifted towards quantitative properties of computer systems. For instance, a car may be required to "apply brake pads no later than 40 ms after the brake pedal is depressed". The precision of sensor inputs may be specified in terms of probabilities. To comprehensively assess a computer system, one needs to integrate qualitative and quantitative analyses to guarantee both correctness and performance.
Despite great advances and improvements in quantitative analysis and verification technology during the last years, the state of the art is largely confined to finite-state systems. This stands in sharp contrast to the fact that infinite state spaces arise naturally in many contexts, e.g., when procedures call each other.
In this fellowship I am developing technology that will answer quantitative questions concerning the correctness and performance of systems with infinitely many states.