T. Ball, V. Levin, and S. K. Rajamani, A decade of software model checking with SLAM, Communications of the ACM, vol.54, issue.7, pp.68-76, 2011.
DOI : 10.1145/1965724.1965743

T. Ball and S. K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, SPIN, pp.113-130, 2000.
DOI : 10.1007/10722468_7

A. Bouajjani, J. Esparza, and O. Maler, Reachability analysis of pushdown automata: Application to model-checking, In CONCUR, pp.135-150, 1997.
DOI : 10.1007/3-540-63141-0_10

T. Cachat, Symbolic Strategy Synthesis for Games on Pushdown Graphs, ICALP, pp.704-715, 2002.
DOI : 10.1007/3-540-45465-9_60

URL : https://hal.archives-ouvertes.fr/hal-00019896

T. Cachat, Games on Pushdown Graphs and Extensions, 2003.

E. , A. Emerson, and C. S. Jutla, Tree automata, mu-calculus and determinacy (extended abstract), FOCS, pp.368-377, 1991.
DOI : 10.1109/sfcs.1991.185392

J. Esparza and S. Schwoon, A BDD-Based Model Checker for Recursive Programs, CAV, pp.324-336, 2001.
DOI : 10.1007/3-540-44585-4_30

A. Finkel, B. Willems, and P. Wolper, A direct symbolic approach to model checking pushdown systems, In INFINITY, vol.9, pp.27-37, 1997.

M. Hague and C. Ong, Winning Regions of Pushdown Parity Games: A Saturation Method, In CONCUR, vol.85, pp.384-398, 2009.
DOI : 10.1016/j.scico.2005.02.009

N. D. Jones and S. S. Muchnick, Even Simple Programs Are Hard To Analyze, Journal of the ACM, vol.24, issue.2, pp.338-350, 1977.
DOI : 10.1145/322003.322016

O. Kupferman, N. Piterman, and M. Y. Vardi, An Automata-Theoretic Approach to Infinite-State Systems, Essays in Memory of Amir Pnueli, pp.202-259, 2010.
DOI : 10.1109/LICS.1996.561357

N. Piterman and M. Y. Vardi, Global Model-Checking of Infinite-State Systems, CAV, pp.387-400, 2004.
DOI : 10.1007/978-3-540-27813-9_30

S. Schwoon, Model-checking Pushdown Systems, 2002.

O. Serre, Note on winning positions on pushdown games with ??-regular conditions, Information Processing Letters, vol.85, issue.6, pp.285-291, 2003.
DOI : 10.1016/S0020-0190(02)00445-3

URL : https://hal.archives-ouvertes.fr/hal-00009319

O. Serre, ContributionàContributionà létude des jeux sur des graphes de processusàprocessusà pile, 2004.

D. Suwimonteerabuth, F. Berger, S. Schwoon, and J. Esparza, jMoped: A Test Environment for Java Programs, CAV, pp.164-167, 2007.
DOI : 10.1007/978-3-540-73368-3_19

D. Suwimonteerabuth, S. Schwoon, and J. Esparza, jMoped: A Java Bytecode Checker Based on Moped, TACAS, pp.541-545, 2005.
DOI : 10.1007/978-3-540-31980-1_35

URL : http://www.informatik.uni-stuttgart.de/fmi/szs/publications/esparza/jmoped.pdf

D. Suwimonteerabuth, S. Schwoon, and J. Esparza, Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains, ATVA, pp.141-153, 2006.
DOI : 10.1007/11901914_13

I. Walukiewicz, Pushdown Processes: Games and Model-Checking, Information and Computation, vol.164, issue.2, pp.234-263, 2001.
DOI : 10.1006/inco.2000.2894

URL : https://doi.org/10.1006/inco.2000.2894

W. Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees, Theoretical Computer Science, vol.200, issue.1-2, pp.135-183, 1998.
DOI : 10.1016/S0304-3975(98)00009-7