Georg WeissenbacherDPhil (Oxon)
I am interested in the fully automated
verification of software and the detection of bugs.
I'm working on automated program analysis tools that use techniques
such as model checking
to prove (or disprove) the correctness
of software. Here are two concrete examples of my current
Heisenbugs are software bugs that disappear
when an attempt to analyse and locate them is made.
This phenomenon is due to the probe effect introduced
by debugging. Heisenbugs are
particularly prevalent in modern multi-core systems,
where the parallel execution of applications leads
to intricate interference effects. On the ARM processor
architecture, deployed in most modern smartphones,
software fragments executed on different processors
might not even agree on the order in which events happen.
Bugs caused by such discrepancies are particularly hard
to reproduce and locate. My goal is to provide tools
that enable the programmer to automatically
pin-point the causes of heisenbugs. The challenge is
to invent techniques that minimally perturb the execution
of the program.
Contemporary software rarely contains annotations that
demonstrate that the code is bug-free
— the correctness of a program
depends on implicit assumptions made by the programmer.
Interpolation is a technique to extract
these implicit assumptions from the source code and
use them as building blocks for correctness proofs.
For this purpose, we translate programs into logical
formulas, which are then automatically analysed
by decision procedures (algorithms that perform
mathematical reasoning) that
I am interested in the theoretical aspects of
interpolation as well as the construction of interpolating