A generic approach to the static analysis of concurrent programs with procedures

ABSTRACT

We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this model are undecidable, because the emptiness problem for the intersection of context-free languages, which is undecidable, can be reduced to them. In this paper we propose an algebraic framework for defining abstractions (upper approximations) of context-free languages. We consider two classes of abstractions: finite-chain abstractions, which are abstractions whose domains do not contain any infinite chains, and commutative abstractions corresponding to classes of languages that contain a word if and only if they contain all its permutations. We show how to compute such approximations by combining automata theoretic techniques with algorithms for solving systems of polynomial inequations in Kleene algebras.

REFERENCES

• 1: Johann Blieberger , Bernd Burgstaller , Bernhard Scholz, Symbolic Data Flow Analysis for Detecting Deadlocks in Ada Tasking Programs, Proceedings of the 5th Ada-Europe International Conference on Reliable Software Technologies, p.225-237, June 26-30, 2000
• 2: Ahmed Bouajjani , Javier Esparza , Oded Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking, Proceedings of the 8th International Conference on Concurrency Theory, p.135-150, July 01-04, 1997
• 3: James Curtis Corbett, Automated formal analysis methods for concurrent and real-time software, University of Massachusetts, Amherst, MA, 1992
• 4: Evelyn Duesterwald , Mary Lou Soffa, Concurrency analysis in the presence of procedures using a data-flow framework, Proceedings of the symposium on Testing, analysis, and verification, p.36-48, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120811]
• 5: Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.62-75, December 06-09, 1994, New Orleans, Louisiana, United States
• 6: Javier Esparza , David Hansel , Peter Rossmanith , Stefan Schwoon, Efficient Algorithms for Model Checking Pushdown Systems, Proceedings of the 12th International Conference on Computer Aided Verification, p.232-247, July 15-19, 2000
• 7: Javier Esparza , Jens Knoop, An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis, Proceedings of the Second International Conference on Foundations of Software Science and Computation Structure, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, p.14-30, March 22-28, 1999
• 8: Javier Esparza , Andreas Podelski, Efficient algorithms for pre* and post* on interprocedural parallel flow graphs, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-11, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325697]
• 9: Mark W. Hopkins , Dexter C. Kozen, Parikh's Theorem in Commutative Kleene Algebra, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.394, July 02-05, 1999
• 10: D. Lugiez , Ph. Schnoebelen, The regular viewpoint on PA-processes, Theoretical Computer Science, v.274 n.1-2, p.89-115, March 6, 2002 [doi>10.1016/S0304-3975(00)00306-6 ]
• 11: Nicolas Mercouroff, An Algorithm for Analyzing Communicating Processes, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.312-325, March 25-28, 1991
• 12: Gleb Naumovich , George S. Avrunin, 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, p.24-34, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 13: G. Ramalingam, Context-sensitive synchronization-sensitive analysis is undecidable, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.416-430, March 2000 [doi>10.1145/349214.349241]
• 14: Martin C. Rinard, Analysis of Multithreaded Programs, Proceedings of the 8th International Symposium on Static Analysis, p.1-19, July 16-18, 2001
• 15: Richard N. Taylor, A general-purpose algorithm for analyzing concurrent programs, Communications of the ACM, v.26 n.5, p.361-376, May 1983 [doi>10.1145/69586.69587]
• 16: Eran Yahav, Verifying safety properties of concurrent Java programs using 3-valued logic, ACM SIGPLAN Notices, v.36 n.3, p.27-40, March 2001

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems

General Terms:
Algorithms, Reliability, Theory, Verification

Keywords:
abstraction, concurrent programs with procedures, kleene algebras, pushdown systems, static analysis, verification