Supporting Proofs for Control-Flow Recovery from Partial Failure Reports

Abstract

Debugging post-deployment failures is difficult, in part because failure reports from these applications usually provide only partial information about what occurred during the failing execution. We introduce approaches that answer control-flow queries about a failing program's execution based on failure constraints given as formal languages. A key component of our approach is the introduction of a new class of subregular languages, the unreliable trace languages (UTL), which allow us to answer many common queries in polynomial time. This report supplements the description of these new approaches with formal proofs. Specifically: we prove completeness for our context-insensitive query problem, tightly bind polynomial-time decidability of query recovery to the UTL class, and prove partial correctness for our approach to answering user queries with UTL constraints.