Flow Analysis for Verifying Specications of Concurrent and Distributed Software

This paper presents FLAVERS, a nite state verication approach that analyzes whether concurrent or sequential programs satisfy user-dened correctness properties. In contrast to other nite-state verica-tion techniques, FLAVERS is based on algorithms with low-order polynomial bounds on the running time. FLAVERS achieves this eciency at the cost of precision. Users, however, can improve the precision of the results by selectively and judiciously incorporating additional semantic information into the analysis problem. The FLAVERS analysis approach has been implemented for programs written in Ada. We report on an empirical study of the performance of applying the FLAVERS/Ada tool set to a collection of multi-tasking Ada programs. This study indicates that sucient precision for proving program properties can be achieved and that the cost for such analysis grows as a low-order polynomial in the size of the program.