Gleb Naumovich
ABSTRACT
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 data flow problems it requires several orders of magnitude less space.
- 1.R. Bodik, R. Gupta, and M. L. Soffa. Refining data flow information using infeasible paths. In Proceedings of the 6th European Sgfiware Engineering Conflrence and the 5th ACM SIGSOFTSymposium on Foundations of software Engineering, pages 361.--377, September 1991. Google Scholar
Digital Library
- 2.M Dwyer. Data Flow Analysis fbr Verifjiing Correctness Properties of Concurrent Programs. PhD thesis, University of Massachussetts, Amherst, 1995. Google ScholarDigital Library
- 3.M. Dwyer and L. Clarke. Data flow analysis for verifying properties of concurrent programs. In Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 62-75, December 1994. Google ScholarDigital Library
- 4.P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proceeding.s of the Third Workhop on Computer Aided Ver@ation, pages 417428, July 1991. Google Scholar
- 5.L. H. Halley and B. K. Rosen. Qualified data flow problems. IEEE Transactions on Software Engineering, SE-7( I ):60-78, January I98 1. Google ScholarDigital Library
- 6.G. J. Holzmann, P. Godefroid, and D. Pirottin. Coverage preserving reduction strategies for reachability analysis. In Proceedins of 12th International Conjkrence on Protocol Specification. Testing, and Ver- $cation. INWG/IFIP, Orlando, FI., June 1992. Google ScholarDigital Library
- 7.J. E. Hopcroft and J. D. Ullman. Formal Languages and their Relation to Automata. Addison-Wesley, 1969. Google ScholarDigital Library
- 8.T. J. Marlowe and B. G. Ryder. Properties of data flow frameworks. Acta Informutica, (28):121-163, 1990. Google ScholarDigital Library
- 9.S. P. Masticola, T. J. Marlowe, and B. G. Ryder. Lattice frameworks for multisource and bidirectional data flow problems. ACM Transactions on Programming Languages and Sy.stems, 17(5):777- 803, September 1995. Google ScholarDigital Library
- 10.G. Naumovich, L. A. Clarke, and L. J. Osterweii. Verification of communication protocols using data flow analysis. In Proc. ofrhe Fourth ACMSlGSOFTSymposium on the Foundations of SofhYare Engineering, pages 9%05, Oct. 1996. Google ScholarDigital Library
- 11.G. Naumovich, L. A. Clarke, and L. J. Osterweil. Comparing implementation strategies for composite data flow analysis problems. Technical Report UM-C&1997-043, University of Massachusetts, Amherst, August 1997. Google ScholarDigital Library
- 12.K. M. Olender and L. J. Osterweil. Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation. IEEE Transactions on Software Engineering, 16(3):268-280, March 1990. Google ScholarDigital Library
- 13.A. Valmari. A stubborn attack on state explosion. In E. M. Clarke and R. Kurshan, editors, Computer-Aided Verification, pages 25-41. American Mathematical Society, Providence RI, 1991. Number 3 in DIMACS Series in Discrete Mathematics and Theoretical Computer Science. Google ScholarDigital Library
Index Terms
- Efficient composite data flow analysis applied to concurrent programs
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 ...
Comments