Extended Weighted Pushdown Systems

作者: Akash Lal , Thomas Reps , Gogul Balakrishnan

DOI: 10.1007/11513988_44

关键词: Data flow diagramTheoretical computer scienceCall siteReachability problemSet (abstract data type)Local variableComputer scienceDataflowGeneralizationNode (networking)

摘要: Recent work on weighted-pushdown systems shows how to generalize interprocedural-dataflow analysis answer “stack-qualified queries”, which the question “what dataflow values hold at a program node for particular set of calling contexts?” The generalization, however, does not account precise handling local variables. Extended-weighted-pushdown address this issue, and provide answers stack-qualified queries in presence variables as well.

参考文章(27)
Thomas W. Reps, Nicholas Kidd, David Melski, Akash Lal, WPDS++: A C++ library for weighted pushdown systems ,(2005)
Ravi Sethi, Jeffrey D. Ullman, Alfred V. Aho, Compilers: Principles, Techniques, and Tools ,(1986)
Javier Esparza, Stefan Schwoon, A BDD-Based Model Checker for Recursive Programs computer aided verification. pp. 324- 336 ,(2001) , 10.1007/3-540-44585-4_30
Gogul Balakrishnan, Thomas Reps, Analyzing Memory Accesses in x86 Executables compiler construction. pp. 5- 23 ,(2006) , 10.1007/978-3-540-24723-4_2
Ahmed Bouajjani, Javier Esparza, Oded Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking international conference on concurrency theory. pp. 135- 150 ,(1997) , 10.1007/3-540-63141-0_10
Jens Knoop, Bernhard Steffen, The Interprocedural Coincidence Theorem compiler construction. pp. 125- 140 ,(1992) , 10.1007/3-540-55984-1_13
T. Jensen, D. Le Metayer, T. Thorn, Verification of control flow based security properties ieee symposium on security and privacy. pp. 89- 103 ,(1999) , 10.1109/SECPRI.1999.766902
Alain Finkel, Bernard Willems, Pierre Wolper, A Direct Symbolic Approach to Model Checking Pushdown Systems (extended abstract) Electronic Notes in Theoretical Computer Science. ,vol. 9, pp. 27- 37 ,(1997) , 10.1016/S1571-0661(05)80426-8
William Landi, Barbara G. Ryder, A safe approximate algorithm for interprocedural pointer aliasing ACM SIGPLAN Notices. ,vol. 39, pp. 473- 489 ,(2004) , 10.1145/989393.989440
Steven S. Muchnick, Neil D. Jones, Program Flow Analysis: Theory and Application Prentice Hall Professional Technical Reference. ,(1981)