On the analysis of interacting pushdown systems

ABSTRACT

Pushdown Systems (PDSs) have become an important paradigm for program analysis. Indeed, recent work has shown a deep connection between inter-procedural dataflow analysis for sequential programs and the model checking problem for PDSs. A natural extension of this framework to the concurrent domain hinges on the, somewhat less studied, problem of model checking Interacting Pushdown Systems. In this paper, we therefore focus on the model checking of Interacting Pushdown Systems synchronizing via the standard primitives - locks, rendezvous and broadcasts, for rich classes of temporal properties - both linear and branching time. We formulate new algorithms for model checking interacting PDSs for important fragments of LTL and the Mu-Calculus. Additionally, we also delineate precisely the decidability boundary for each of the standard synchronization primitives.

REFERENCES

• 1: 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
• 2: A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek. Reachability analysis of multithreaded software with asynchronous communica-tion. In FSTTCS, 2005.
• 3: A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In IJFCS, volume 14(4), pages 551--, 2003.
• 4: Ahmed Bouajjani , Markus Müller-Olm , Tayssir Touili, Regular symbolic analysis of dynamic networks of pushdown systems, Lecture Notes in Computer Science, Springer-Verlag, London, 2005 [doi>10.1007/11539452_36]
• 5: S. Chaki, E. Clarke, N. Kidd, T.Reps, and T.Touili. Verifying concurrent message-passing c programs with recursive calls. In TACAS, 2006.
• 6: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 7: E.A. Emerson and V. Kahlon. Model checking guarded protocols. In LICS, 2003.
• 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: Vineet Kahlon , Aarti Gupta, An Automata-Theoretic Approach for Model Checking Threads for LTL Propert, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.101-110, August 12-15, 2006 [doi>10.1109/LICS.2006.11]
• 10: V. Kahlon, F. Ivančić, and A. Gupta. Reasoning about threads communicating via locks. In CAV, 2005.
• 11: A. Lal, G. Balakrishnan, and T. Reps. Extended weighted pushdown systems. In CAV, 2005.
• 12: 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]
• 13: Shaz Qadeer , Sriram K. Rajamani , Jakob Rehof, Summarizing procedures in concurrent programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-255, January 14-16, 2004, Venice, Italy
• 14: S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, 2005.
• 15: 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]
• 16: Thomas Reps , Stefan Schwoon , Somesh Jha , David Melski, Weighted pushdown systems and their application to interprocedural dataflow analysis, Science of Computer Programming, v.58 n.1-2, p.206-263, October 2005 [doi>10.1016/j.scico.2005.02.009]
• 17: Igor Walukiewicz, Model Checking CTL Properties of Pushdown Systems, Proceedings of the 20th Conference on Foundations of Software Technology and Theoretical Computer Science, p.127-138, December 13-15, 2000

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Theory, Verification

Keywords:
LTL, concurrency, dataflow analysis, model checking, mu-calculus, pushdown systems