What gives? A hybrid algorithm for error trace explanation

Abstract

When a program fails, the cause of the failure is often buried in a long, hard-to-understand error trace. We present a new technique for automatic error localization, which formally unifies prior approaches based on computing interpolants and minimal unsatisfiable cores of failing executions. Our technique works by automatically reducing an error trace to its essential components-a minimal set of statements that are responsible for the error, together with key predicates that explain how these statements lead to the failure.We prove that our approach is sound, and we show that it is useful for debugging real programs.