Talks and Poster Presentations (with Proceedings-Entry):
Keynote Lecture: RV 2015, the 6th International Conference on Runtime Verification,
- 2015-09-25; in: "Runtime Verification",
E. Bartocci, R. Majumdar (ed.);
Lecture Notes in Computer Science/Springer,
Heisenbugs are complex software bugs that alter their behaviour when attempts to isolate them are made. The term heisenbug is a pun on the name of physicist Werner Heisenberg and refers to bugs whose analysis is complicated by the probe effect, an unintended alteration of system behaviour caused by an observer.
Heisenbugs are most prevalent in concurrent systems, where the interplay of multiple threads running on multi-core processors leads to intricate effects not anticipated by the developer. Faced with a heisenbug, it is the tedious task of the programmer to reproduce the erroneous behaviour and analyse its cause before the bug can be fixed.
It is exactly in these situations that automated analyses are the most desirable. Model checkers and systematic testing tools, for instance, can automatically reproduce erroneous executions manifesting the bug. The subsequent inspection of the error trace, however, is still a time-consuming process that requires substantial insight.
My group developed two approaches to analyse erroneous executions and explain concurrency bugs, attacking the problem from different angles. In both cases, the goal is to allow the programmer to focus on the essence of the bug rather than the specifics of the failed execution. On the one hand, we use data mining to extract explanations from execution logs by juxtaposing successful runs of the program with failed executions. The resulting explanations highlight potentially problematic data dependencies that frequently occur in failing executions. The second approach relies on static analysis and automated reasoning to obtain a slice of an erroneous execution trace that reflects the core of the problem.
After introducing both approaches, I will discuss their advantages as well as shortcomings, and explain differences regarding soundness and comprehensibility using case studies and empirical results.
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.