Abstract
Invisible Control Flow (ICF) results from dynamic binding and asynchronous processing. For modern software replete with ICF, the ability to analyze and resolve ICF is crucial for verifying software. A fully automated analysis to resolve ICF suffers from imprecision and high computational complexity. As a practical alternative, we present a novel solution of interactive human-machine collaboration to resolve ICF. Our approach is comprised of interactive program analysis and comprehension to systematically capture and link the clues crucial for resolving ICF. We present the tool support we have developed using the query language and visualization capabilities of the Atlas Platform. We illustrate the approach using examples where resolving ICF is crucial to verify software and show a complex bug in the Linux kernel discovered by resolving ICF.