Improving static analysis accuracy on concurrent Ada programs: Complexity results and empirical findings

This paper presents several techniques for improving the accuracy of static analysis of concurrent Ada programs. We determine the cost of building the program representations used to perform the analysis and examine the complexity of performing analysis on those representations. Inaccuracies in the static analysis are reflected in spurious results, which can be generated if the analysis considers paths through the program that are infeasible, or if the effects of aliasing lead to consideration of task communications that can not actually occur. We present three techniques to counter the effects of infeasible path consideration and aliasing and determine the cost of using these techniques. We present empirical results that demonstrate the improvements in accuracy and, in some cases, the reduction in the search space that result from application of our techniques.