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 has the potential to handle large scale systems, it sometimes can still be very expensive to use. In this paper we experimentally compare the cost of two versions of this approach for solving composite data flow analysis problems. The first version, product- based, uses 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 version is comparable in time to the product- based version but for large composite date flow problems it requires several orders of magnitude less space.
Recommendations
Efficient composite data flow analysis applied to concurrent programs
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 ...
Efficient composite data flow analysis applied to concurrent programs
PASTE '98: Proceedings of the 1998 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineeringFLAVERS, 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 ...
Efficient Verification of Sequential and Concurrent C Programs
There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...