I am devoted to making the world a safer place by inventing techniques that enable us to establish the correctness of software in a fully automated manner. This interest is driven by…

• the ubiquity of software. Electronic devices continue to permeate our environment and become an indispensable (yet more and more unnoticed) part of our everyday life. They control the brakes in our cars, guard our houses, or trigger our heart beat as cardiac pacemakers.
• the challenges imposed by the scale of modern software systems. The ever growing complexity of the individual components and the increasing number of processors (currently about 100 in a modern car) in autonomous as well as in distributed systems keeps raising the bar for automated verification techniques.
• the potential damage caused by faulty software. This spans from potential financial losses (e.g., a failed software upgrade triggered a 9.6% plunge in an exchange traded fund in October 2010) to threatening human lives (race condition bugs have caused a radiation therapy machine to malfunction and resulted in a power blackout in New York City as observed in 2003). Moreover, once the damage is done, we need to find the causes. Software failures can be so unexpected and intricate that it even becomes a challenge to find out what actually went wrong.
• the technical challenges faced when it comes to creating safe and correct software systems. To guarantee the success of a software project, verification needs to start even before the first line of code is written. Moreover, seemingly conflicting requirements (e.g., global accessibility and availability of medical or financial data while ensuring the privacy of individuals and the integrity of each entry) raise an even more fundamental question: Is it even possible to build the system?