Research Group

Heisenbugs: From Detection to Explanation

Project type: Research Group
Programme: Information and Communication Technology
Call: Vienna Research Groups for Young Investigators Call 2011
Start: 01.10.2012
Duration: 8,00 years
Grant awarded: 1.500.000 €
Keywords: model checking, automated software verification, predicate abstraction, Heisenbugs, interpolation, decision procedures

Georg Weissenbacher

Vienna University of Technology

A Heisenbug is a computer bug that disappears or alters its behaviour when the developer attempts to analyse or isolate it. This phenomenon is a ramification of the increasing complexity of modern computer systems: sophisticated software algorithms
and their interplay with contemporary multi-core processors lead to intricate effects not anticipated by the programmer.

Heisenbugs are difficult to detect, replicate, and understand, leading to unpredictable development schedules and software containing undiscovered bugs. The goal of the research project is to increase programmer productivity as well as the quality of
software by providing tools and techniques that help the programmer to discover, reproduce, and locate the causes of Heisenbugs.

The challenges posed by Heisenbugs are manifold. The successful reconstruction of the erroneous behaviour is a prerequisite to its explanation. However, limited control over the
order of events in multi-core or distributed systems complicates the detection as well as the reproduction of concurrency bugs. Observability limitations at the hardware level may prevent the developer from recording an execution history sufficiently detailed to
analyse the bug, while the side effects of probing and logging mechanisms can effectively hide the bug. Finally, an execution that exposes a Heisenbug may be extremely long.
The excessive length of a scenario triggering a bug is an obstacle to narrowing down the underlying causes.

The project aims at overcoming these problems by deploying and advancing existing techniques such as static analysis and model checking (avoiding side effects and the execution of the program altogether), runtime verification (monitoring the execution
by means of non-invasive instrumentation), and symbolic analysis and automated reasoning (determining causes by reasoning about logical consistency).

The Heisenbugs project lies at the intersection of automated program analysis, logic and decision procedures, and artificial intelligence, and requires theoretical as well as practical advances in these fields. Vienna University of Technology is home to world renowned
experts in the above mentioned areas, making the institution the ideal location to conduct this research.

« back