Supporting Proofs for Control-Flow Recovery from Partial Failure ReportsSupporting Proofs for Control-Flow Recovery from Partial Failure ReportsThis research was conducted by Peter Ohmann, Alexander Brooks, Loris D’Antoni, and Ben Liblit.
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.
The full paper is available as a single PDF document. A suggested BibTeX citation record is also available.