Flow Analysis for Verifying Specifications of Concurrent and Distributed Software

This paper presents FLAVERS, a finite state verification approach that analyzes whether concurrent or sequential programs satisfy user-defined correctness properties. In contrast to other finite-state verification techniques, FLAVERS is based on algorithms with low-order polynomial bounds on the running time. FLAVERS achieves this efficiency 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 sufficient 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. 1 Introduction The application of distributed and concurrent pr..