Data flow analysis for verifying correctness properties of concurrent programs
Matthew B. Dwyer, Lori A. Clarke · 1995
Developers of modern software systems are increasingly employing concurrency to meet demanding system requirements. To deal with the inherent complexity that results from concurrency, developers require cost-effective automated analysis techniques to gain confidence in the quality of their concurrent software. We present an approach, called FLAVERS, that is able to provide cost-effective analysis of concurrent programs with respect to a rich class of explicitly stated correctness properties. FLAVERS is based on a family of polynomial-time, conservative data flow analysis algorithms. Unlike existing analysis approaches for concurrent software, FLAVERS allows developers to control the tradeoff between analysis cost an...