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 and decision procedures to prove (or disprove) the correctness of software. Here are two concrete examples of my current research interests:

• 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 generate interpolants. I am interested in the theoretical aspects of interpolation as well as the construction of interpolating decision procedures.