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.

Venue: 24th International Conference on Program Comprehension (ICPC 2016), Austin, Texas, May 14-22, 2016

Authors: Suresh Kothari, Ahmed Tamrawi, Jon Mathews

Paper (PDF): ICF-ICPC2016.pdf

Bibtex:
@INPROCEEDINGS{7503727,
author={S. Kothari and A. Tamrawi and J. Mathews},
booktitle={2016 IEEE 24th International Conference on Program Comprehension (ICPC)},
title={Human-machine resolution of Invisible Control Flow?},
year={2016},
pages={1-4},
keywords={Linux;computational complexity;data visualisation;formal verification;human computer interaction;query languages;Atlas platform;ICF;Linux kernel;asynchronous processing;computational complexity;dynamic binding;human-machine resolution;invisible control flow;query language;software verification;visualization capabilities;Collaboration;Database languages;Indexes;Kernel;Man-machine systems;Reactive power},
doi={10.1109/ICPC.2016.7503727},
month={May},}