Vineet Kahlon
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.
- A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, LNCS 1243, pages 135--150, 1997.]] Google Scholar
Digital Library
- A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek. Reachability analysis of multithreaded software with asynchronous communica-tion. In FSTTCS, 2005.]] Google ScholarDigital Library
- 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.]]Google Scholar
- A. Bouajjani, M. Olm, and T. Touili. Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems. In CONCUR, 2005.]] Google ScholarDigital Library
- S. Chaki, E. Clarke, N. Kidd, T.Reps, and T.Touili. Verifying concurrent message-passing c programs with recursive calls. In TACAS, 2006.]] Google ScholarDigital Library
- E. A. Emerson. Temporal and Modal Logic. In Handbook of Theoretical Computer Science, Volume B, pages 997--1072, 1998.]] Google ScholarDigital Library
- E.A. Emerson and V. Kahlon. Model checking guarded protocols. In LICS, 2003.]]Google ScholarCross Ref
- J. Esparza and A. Podelski. Efficient Algorithms for pre and post on Interprocedural Parallel Flow Graphs. In POPL, 2000.]] Google ScholarDigital Library
- V. Kahlon and A. Gupta. An Automata-Theoretic Approach for Model Checking Threads for LTL Properties. In LICS, 2006.]] Google ScholarDigital Library
- V. Kahlon, F. Ivančić, and A. Gupta. Reasoning about threads communicating via locks. In CAV, 2005.]] Google ScholarDigital Library
- A. Lal, G. Balakrishnan, and T. Reps. Extended weighted pushdown systems. In CAV, 2005.]]Google Scholar
- D. Lugiez and Ph. Schnoebelen. The Regular Viewpoint on PA-Processes. In Theor. Comput. Sci., volume 274(1--2), 2002.]] Google ScholarDigital Library
- S. Qadeer, S. K. Rajamani, and J. Rehof. Summarizing procedures in concurrent programs. In POPL, pages 245--255, 2004.]] Google ScholarDigital Library
- S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, 2005.]] Google ScholarDigital Library
- G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. In ACM Trans. Program. Lang. Syst., volume 22(2), pages 416--430, 2000.]] Google ScholarDigital Library
- T. W. Reps, S. Schwoon, S. Jha, and D. Melski. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Science of Computer Programming, volume 58(1--2), 2005.]] Google ScholarDigital Library
- I. Walukeiwicz. Model checking ctl properties of pushdown systems. In FSTTCS, LNCS 1974, pages 127--138, 2000.]] Google ScholarDigital Library
Index Terms
- On the analysis of interacting pushdown systems
Recommendations
On the analysis of interacting pushdown systems
Proceedings of the 2007 POPL ConferencePushdown 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 ...
Model checking dynamic pushdown networks
AbstractA dynamic pushdown network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded programs with (possibly recursive) procedure calls and thread ...
Pushdown module checking
Model checking is a useful method to verify automatically the correctness of a system with respect to a desired behavior, by checking whether a mathematical model of the system satisfies a formal specification of this behavior. ...
Comments