In the following table, contact information relevant to the page. The first column is for visual reference only. Data is in the right column.
|Division:||Department of Computer Science|
|Organisation:||University of Oxford|
|Tags:||Fellowship: Early Career, Fellowship: Previous Fellow, University of Oxford|
|Related theme:||Digital economy Engineering ICT Mathematical sciences|
I obtained a doctoral degree at the TU München in 2009. From 2009 to 2013 I had postdoctoral positions at the University of Oxford. I hold a Royal Society University Research Fellowship. I became a Research Lecturer in 2013 and an Associate Professor in 2014 at the Oxford University Department of Computer Science.
Computers are now ubiquitous: they are embedded in mobile phones, airplanes, medical devices, and so on. Consequently our dependence on them has increased dramatically, and the failure of so-called safety-critical systems may lead to catastrophic consequences. 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.
The field of computer-aided verification is based on this idea. Research in the field has led to four Turing awards to date. The economic importance of formal verification can be illustrated by prominent software errors, such as the one that led to the 2003 power blackout in the Northeast of the United States, which could have been avoided by computer-aided verification.
The most basic correctness property is termination: given a program, does it ever terminate (stop its computation)? Famously, Alan Turing proved that there exists no algorithm that takes a program as input and determines whether it terminates. However, Turing's result leaves open the possibility of proving or disproving termination for large classes of programs. Driven by numerous applications, this is a thriving research area.
Special-purpose tools can now answer questions such as: "Does the operating system eventually handle all requests and remain responsive in the meantime?" New challenges are posed by programs that contain probabilities. For this project we are developing technology that automatically proves termination properties of probabilistic programs.