Cited references and notes

1. E. W. Dijkstra, Notes on Structured Programming, Academic Press, London (1972), pp. 1–82.
2. R. Floyd, “Assigning Meaning to Programs,” Proceedings, Symposium on Applied Mathematics, Volume 19, American Mathematical Society, Providence, RI (1967), pp. 19–32.
3. S. Owre, J. Rushby, N. Shankar, and D. Stringer-Calvert, “PVS: An Experience Report,” Applied Formal Methods—FM-Trends 98, Volume 1641 of Lecture Notes in Computer Science, D. Hutter, W. Stephan, P. Traverso, and M. Ullman, Editors, Springer-Verlag, Boppard, Germany (October 1998), pp. 338–345.
4. E. M. Clarke and J. M. Wing, “Formal Methods: State of the Art and Future Directions,” ACM Computing Surveys 28, No. 4, 626–643 (December 1996).
5. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic Model Checking: 1020 States and Beyond,” Information and Computing 98, No. 2, 142–170 (1992).
6. K. L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem, Kluwer Academic Publishers, Boston, MA (1993).
7. G. J. Holzmann, “The Model Checker SPIN,” IEEE Transactions on Software Engineering 23, No. 5, 279–295 (May 1997).
8. R. J. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D. Notkin, and J. D. Reese, “Model Checking Large Software Specifications,” IEEE Transactions on Software Engineering 24, No. 7, 498–520 (July 1996).
9. J. M. Wing and M. Vaziri-Farahani, “Model Checking Software Systems: A Case Study,” Proceedings, Third ACM SIGSOFT Symposium on the Foundations of Software Engineering, Washington, DC (October 10–13, 1995), pp. 128–139.
10. This research was partially supported by the U.S. Department of Defense/Army and the Defense Advanced Research Projects Agency under Contract DAAH01-00-C-R231, by the National Science Foundation under Grant CCR-9708184, and by IBM Faculty Partnership Awards. The U.S. government is authorized to reproduce and distribute reprints for governmental purposes notwithstanding any copyright annotation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the Defense Advanced Research Projects Agency, the Air Force Research Laboratory/IFTD, the U.S. Department of Defense, the U.S. Army, the U.S. government, the National Science Foundation, or of IBM.
11. K. M. Olender and L. J. Osterweil, “Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation,” IEEE Transactions on Software Engineering 16, No. 3, 268–280 (March 1990).
12. M. B. Dwyer and L. A. Clarke, “Data Flow Analysis for Verifying Properties of Concurrent Programs,” Proceedings, Second ACM SIGSOFT Symposium on the Foundations of Software Engineering, New Orleans, LA (December 6–9, 1994), pp. 62–75.
13. M. B. Dwyer and L. A. Clarke, Flow Analysis for Verifying Specifications of Concurrent and Distributed Software, Technical Report 99-52, University of Massachusetts, Department of Computer Science, Amherst, MA (August 1999).
14. G. Naumovich, G. S. Avrunin, and L. A. Clarke, “Data Flow Analysis for Checking Properties of Concurrent Java Programs,” Proceedings, 21st International Conference on Software Engineering, Los Angeles, CA (May 16–22, 1999), pp. 399–410.
15. G. Naumovich, G. S. Avrunin, L. A. Clarke, and L. J. Osterweil, “Applying Static Analysis to Software Architectures,” Proceedings, Joint 6th European Software Engineering Conference and 5th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Zurich, Switzerland (September 22–25, 1997), pp. 77–93.
16. J. M. Cobleigh, L. A. Clarke, and L. J. Osterweil, “Verifying Properties of Process Definitions,” Proceedings, International Symposium on Software Testing and Analysis, Portland, OR (August 22–24, 2000), pp. 96–101.
17. A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques, and Tools, Addison-Wesley Publishing Co., Reading, MA (1986).
18. FLAVERS does not currently handle recursive subprograms, although standard techniques for dealing with recursion could be extended and incorporated.
19. R. N. Taylor, “Complexity of Analyzing the Synchronization Structure of Concurrent Programs,” Acta Informatica 19, No. 1, 57–84 (April 1983).
20. G. Naumovich and G. S. Avrunin, “A Conservative Data Flow Algorithm for Detecting All Pairs of Statements that May Happen in Parallel,” Proceedings, Sixth ACM SIGSOFT Symposium on the Foundations of Software Engineering, Lake Buena Vista, FL (November 3–5, 1998), pp. 24–34.
21. G. Naumovich, G. S. Avrunin, and L. A. Clarke, “An Efficient Algorithm for Computing MHP Information for Concurrent Java Programs,” Proceedings, Joint 7th European Software Engineering Conference and 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Toulouse, France (September 6–10, 1999), pp. 338–354.
22. G. Naumovich, L. A. Clarke, and L. J. Osterweil, “Efficient Composite Data Flow Analysis Applied to Concurrent Programs,” Proceedings, ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, Montreal, Canada (June 16, 1998), pp. 51–58.
23. T. J. Marlowe and B. G. Ryder, “Properties of Data Flow Frameworks: A Unified Model,” Acta Informatica 28, 121–163 (1990).
24. Clever bookkeeping can improve the efficiency of line 5 of the meta-algorithm. As presented, each tuple of node n is propagated to node m on every loop iteration. In our implementation, each node keeps track of what tuples it has propagated to its successors, so when line 5 is reached only new tuples are propagated.
25. J. M. Cobleigh, L. A. Clarke, and L. J. Osterweil, “The Right Algorithm at the Right Time: Comparing Data Flow Analysis Algorithms for Finite State Verification,” Proceedings, 23rd International Conference on Software Engineering, Toronto, Canada (May 12–19, 2001), pp. 37–46.
26. In this example, both philosophers pick up fork 1 and then fork 2, meaning one philosopher picks up the left fork first while the other philosopher picks up the right fork first. This is necessary to prevent deadlock in the system.
27. The variable “done” is used to break the loop to allow the program to terminate, since FLAVERS currently considers only tuples that reach the final node. Although we do not address this issue in this paper, work has been done on extending our approach to prove properties over infinite executions. See G. Naumovich and L. A. Clarke, “Extending FLAVERS to Check Properties on Infinite Executions of Concurrent Software Systems,” Proceedings, Workshop on Engineering Automation for Software Intensive System Integration, Monterey, CA (June 18–22, 2001), pp. 126–135.
28. FLAVERS requires that FSAs be total, meaning that they have a transition from every state on every event in the alphabet. The FSA in Figure 1 and the other FSAs that we show are not total in order to make them more compact and easier to understand. They can easily be made total, by adding a trap state that is nonaccepting and has all self-loop transitions and by adding transitions from the existing states of the FSAs to this trap state on events where transitions do not already exist.
29. When inlining was performed, variables in called methods were renamed to avoid collisions. Thus, in the philosopher1 task, success1_1 represents the variable success in the method up and success1_2 represents the variable success in the method down. Similarly, for the philosopher2 task, variables success2_1 and success2_2 are used.
30. We can do better than this by using a partial order optimization that can reduce the number of MIP edges by noting that certain interleavings are equivalent with respect to the property and constraints. Thus, it is only necessary to consider one interleaving from each equivalence class. See G. Naumovich, L. A. Clarke, and J. M. Cobleigh, “Using Partial Order Techniques to Improve Performance of Data Flow Analysis Based Verification,” Proceedings, ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, Toulouse, France (September 6, 1999), pp. 57–65.
31. D. Jackson and M. Vaziri, “Finding Bugs with a Constraint Solver,” Proceedings, International Symposium on Software Testing and Analysis, Portland, OR (August 21–23, 2000), pp. 14–25.
32. R. N. Taylor, F. C. Belz, L. A. Clarke, L. Osterweil, R. W. Selby, J. C. Wileden, A. L. Wolf, and M. Young, “Foundations for the Arcadia Environment Architecture,” Proceedings, ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments (November 1988), pp. 1–13.
33. G. S. Avrunin, J. C. Corbett, M. B. Dwyer, C. S. Psreanu, and S. F. Siegel, Comparing Finite-State Verification Techniques for Concurrent Software, Technical Report 99-69, University of Massachusetts, Department of Computer Science, Amherst, MA (November 1999).
34. K. Forester, C. MacFarlane, M. Cameron, and G. Bolcer, Chiron-1 User Manual, Arcadia Document UCI-93-07, University of California, Irvine, CA (September 1993).
35. G. S. Avrunin, U. A. Buy, J. C. Corbett, L. K. Dillon, and J. C. Wileden, “Automated Analysis of Concurrent Systems with the Constrained Expression Toolset,” IEEE Transactions on Software Engineering 17, No. 11, 1204–1222 (November 1991).
36. In this experiment, FLAVERS often had the worst performance on the smaller problems, but it was the only FSV system that began its analysis by dealing with actual source code, rather than an abstract model of source code.
37. L. J. Osterweil and L. D. Fosdick, “DAVE—A Validation Error Detection and Documentation System for FORTRAN Programs,” Software—Practice and Experience 6, 473–486 (1976).
38. K. M. Olender and L. J. Osterweil, “Interprocedural Static Analysis of Sequencing Constraints,” ACM Transactions on Software Engineering and Methodology 1, No. 1, 21–52 (January 1992).
39. P. Godefroid, “Model Checking for Programming Languages Using VeriSoft,” Proceedings, 24th ACM Symposium on Principles of Programming Languages, Paris, France (January 15–17, 1997), pp. 174–186.
40. G. J. Holzmann, “Logic Verification of ANSI-C Code with SPIN,” Proceedings, Seventh SPIN Workshop, Stanford, CA (August 30–September 1, 2000), pp. 131–147.
41. W. Visser, K. Havelund, G. Brat, and S.-J. Park, “Model Checking Programs,” Proceedings, Fifteenth IEEE International Conference on Automated Software Engineering (September 2000), pp. 3–12.
42. T. Ball and S. K. Rajamani, “Automatically Validating Temporal Safety Properties of Interfaces,” Proceedings, Eighth SPIN Workshop, Toronto, Canada (May 19–20, 2001), pp. 101–122.
43. T. Ball and S. K. Rajamani, “Bebop: A Symbolic Model Checker for Boolean Programs,” Proceedings, Seventh SPIN Workshop, Stanford, CA (August 30–September 1, 2000), pp. 113–130.
44. J. C. Corbett, M. B. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. S. Psreanu, Robby, and H. Zheng, “Bandera: Extracting Finite-State Models from Java Source Code,” Proceedings, 22nd International Conference on Software Engineering, Limerick, Ireland (June 4–11, 2000).
45. M. B. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. S. Psreanu, Robby, W. Visser, and H. Zhen, “Tool-Supported Program Abstraction for Finite-State Verification,” Proceedings, 23rd International Conference on Software Engineering, Toronto, Canada (May 12–19, 2001), pp. 177–187.
46. M. B. Dwyer, J. Hatcliff, and H. Zheng, “Slicing Software for Model Construction,” Proceedings, ACM/SIGPLAN Symposium on Partial Evaluation and Semantic-Based Program Manipulation, San Antonio, TX (January 22–23, 1999), pp. 105–118.
47. D. Engler, B. Chelf, A. Chou, and S. Hallem, “Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions,” Proceedings, Fourth Symposium on Operating Systems Design and Implementation, San Diego, CA (October 23–25, 2000).
48. A. T. Chamillard, L. A. Clarke, and G. S. Avrunin, An Empirical Comparison of Static Concurrency Analysis Techniques, Technical Report 96-84, University of Massachusetts, Department of Computer Science, Amherst, MA (May 1996).
49. A. Pnueli, “The Temporal Logic of Programs,” Proceedings, Eighteenth Symposium on Foundations of Computer Science, Providence, RI (October 31–November 2, 1977), pp. 46–57.
50. E. A. Emerson, “Temporal and Modal Logic,” Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, J. van Leeuwen, Editor, Elsevier Science Publishers (1990), 995–1072.
51. M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, “Patterns in Property Specifications for Finite-State Verification,” Proceedings, 21st International Conference on Software Engineering, Los Angeles, CA (May 1999), pp. 16–22.