EFFICIENT COMPOSITE DATA-FLOW ANALYSIS APPLIED TO CONCURRENT PROGRAMS

FLAVERS, a tool for verifying properties of concurrent systems, uses c omposite data flow analysis to incrementally improve the precision of the results of its verifications. Although FLAVERS is one of the few s tatic analysis techniques for concurrent systems that has the potentia l to handle large scale systems, it sometimes can still be very expens ive to use. Ln this paper we experimentally compare the cost of two ve rsions of this approach for solving composite data flow analysis probl ems. The first version, product-based, uses the more straightforward a pproach, and the second, tuple-based, is built around the idea of redu cing analysis space requirements at the expense of analysis time. We d emonstrate experimentally, by analyzing properties of actual concurren t programs, that the tuple-based version is comparable in time to the product-based version but for large composite data flow problems it re quires several orders of magnitude less space.