Browse Reports

FLAVERS, a tool for verifying properties of concurrent systems, uses composite data flow analysis to incrementally improve the precision of the results of its verifications. Although FLAVERS is one of the few static analysis techniques for concurrent systems that does not have exponential worst case bounds, it sometimes can still be very expensive to use. In this paper we experimentally compare the cost of two approaches for solving composite data flow analysis problems. The first approach, product-based, is the more straightforward approach, and the second, tuple-based, is built around the idea of reducing analysis space requirements at the expense of analysis time. We demonstrate experimentally, by analyzing properties of actual concurrent programs, that the tuple-based approach is comparable in time to the product-based approach but for large composite data flow problems it requires several orders of magnitude less space.