Date(s) - 30 Apr 2014
1:10 PM - 2:00 PM
2222 Coover Hall
Title: Event-Flow Graphs for Efficient Verification of Correctness Properties
Speaker: Ahmed Tamrawi, ECpE Graduate Student
Adviser: Suraj Kothari, Richardson Professor
Abstract: Large and complex software systems calls for automated techniques to achieve high accuracy and efficiency in verifying correctness properties. Efficient verification requires performing efficient and accurate path-sensitive analyses that pose the challenges of: (a) analyzing an exponentially-increasing number of paths in a control flow graph (CFG), and (b) checking feasibility of paths in a CFG. We address these challenges by introducing an equivalence relation on the CFG paths to partition them into equivalence classes. It is then sufficient to perform analysis on these equivalence classes rather than on the individual paths in a CFG. This technique has two major advantages: (a) although the number of paths in a CFG can be exponentially large, the essential information to be analyzed is captured by a small number of equivalence classes, and (b) checking path feasibility becomes simpler. The key challenge is how to efficiently compute equivalence classes of paths in a CFG without examining each path in the CFG? We present a linear-time algorithm to form equivalence classes without the need for examination of each path in a CFG. The key to this algorithm is construction of an event-flow graph (EFG), a compact derivative of the CFG, in which each path represents an equivalence class of paths in the corresponding CFG. EFGs are defined with respect to the set of events that are in turn defined by the analyzed property. The equivalence classes are thus guaranteed to preserve all the event traces in the original CFG. We present an empirical evaluation of the Linux kernel (v3.12). The EFGs in our evaluation are defined with respect to events of the spin safe-synchronization property. Empirical evaluation results show that there are many fewer EFG-based equivalence classes compared to the corresponding number of paths in a CFG. This reduction is close to 99% for CFGs with a large number of paths.