- Author:
- Matthew Barbour Dwyer,
- Director:
- Lori A. Clarke
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 and the precision of analysis results by incrementally introducing additional information into the analysis. One strength of this approach is the flexibility allowed in choosing and combining a variety of sources of information about the program and property being analyzed, so as to increase precision without making the cost of analysis impractical.
We have extended the theoretical foundations of data flow analysis to support the description and solution of data flow analysis problems for concurrent programs. We have engineered a domain-specific software architecture that greatly reduces the cost of developing data flow analyzers. These advances are widely applicable. We have leveraged off of them to produce an implementation of FLAVERS with which we have been able to successfully validate the feasibility of the analysis approach.
Cited By
- Brylow D and Palsberg J (2004). Deadline Analysis of Interrupt-Driven Software, IEEE Transactions on Software Engineering, 30:10, (634-655), Online publication date: 1-Oct-2004.
Dwyer M, Clarke L, Cobleigh J and Naumovich G (2004). Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), 13:4, (359-430), Online publication date: 1-Oct-2004.- Grimaud G, Lanet J and Vandewalle J (2019). FACADE, ACM SIGSOFT Software Engineering Notes, 24:6, (476-493), Online publication date: 1-Nov-1999.
- Grimaud G, Lanet J and Vandewalle J FACADE Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, (476-493)
- Naumovich G, Clarke L and Osterweil L Efficient composite data flow analysis applied to concurrent programs Proceedings of the 1998 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, (51-58)
- Naumovich G, Clarke L and Osterweil L (2019). Efficient composite data flow analysis applied to concurrent programs, ACM SIGPLAN Notices, 33:7, (51-58), Online publication date: 1-Jul-1998.
- Naumovich G and Avrunin G A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, (24-34)
- Naumovich G and Avrunin G (1998). A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel, ACM SIGSOFT Software Engineering Notes, 23:6, (24-34), Online publication date: 1-Nov-1998.
- Naumovich G, Clarke L and Osterweil L Verification of communication protocols using data flow analysis Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, (93-105)
- Naumovich G, Clarke L and Osterweil L (2019). Verification of communication protocols using data flow analysis, ACM SIGSOFT Software Engineering Notes, 21:6, (93-105), Online publication date: 1-Nov-1996.
- Dwyer M and Clarke L A flexible architecture for building data flow analyzers Proceedings of the 18th international conference on Software engineering, (554-564)
- Corbett J (1996). Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, 22:3, (161-180), Online publication date: 1-Mar-1996.
Recommendations
Verifying concurrent programs: tutorial talk
FMCAD '11: Proceedings of the International Conference on Formal Methods in Computer-Aided DesignThe proliferation of multi-core hardware has led to widespread use of concurrent programs. However, these programs are notoriously difficult to get right and to debug for developers. Even for automated verification, it is a big challenge to reason about ...
Verifying safety properties of concurrent heap-manipulating programs
We provide a parametric framework for verifying safety properties of concurrent heap-manipulating programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to verification algorithms that are ...
Data flow analysis for verifying properties of concurrent programs
In this paper we present an approach, based on data flow analysis, that can provide cost-effective analysis of concurrent programs with respect to explicitly stated correctness properties. Using this approach, a developer specifies a property of a ...