@article(A12,
 author       = "M. F. Atig",
 year         = "2012",
 title        = "Model-Checking of Ordered Multi-Pushdown Automata",
 journal      = "Logical Methods in Computer Science",
 volume       = "8",
 number       = "3",
 doi          = "10.2168/LMCS-8(3:20)2012",
)
@article(BLR11,
 author       = "T. Ball and V. Levin and S. K. Rajamani",
 year         = "2011",
 title        = "A decade of software model checking with SLAM",
 journal      = "Commun. ACM",
 volume       = "54",
 number       = "7",
 pages        = "68--76",
 doi          = "10.1145/1965724.1965743",
)
@inproceedings(BR00,
 author       = "T. Ball and S. K. Rajamani",
 year         = "2000",
 title        = "Bebop: A Symbolic Model Checker for Boolean Programs",
 booktitle    = "Proceedings of SPIN'00",
 pages        = "113--130",
 doi          = "10.1007/10722468\_7",
)
@article(Bar-hillel61,
 author       = "Y. Bar-Hillel and M. Perles and E. Shamir",
 year         = "1961",
 title        = "On formal properties of simple phrase structure grammars",
 journal      = "Z. Phonetik Sprachwiss. Kommunikat.",
 volume       = "14",
 pages        = "143–172",
)
@article(Benois69,
 author       = "M. Benois",
 year         = "1969",
 title        = "Parties rationnelles du groupe libre",
 journal      = "{C}omptes-{R}endus de l'{A}camd{\'e}mie des {S}ciences de {P}aris, S{\'e}rie {A}",
 volume       = "269",
 pages        = "1188--1190",
)
@article(Benois86,
 author       = "M. Benois and J. Sakarovitch",
 year         = "1986",
 title        = "On the Complexity of Some Extended Word Problems Defined by Cancellation Rules",
 journal      = "Inf. Process. Lett.",
 volume       = "6",
 pages        = "281--287",
 doi          = "10.1016/0020-0190(86)90087-6",
)
@inproceedings(BEM97,
 author       = "A. Bouajjani and J. Esparza and O. Maler",
 year         = "1997",
 title        = "Reachability Analysis of Pushdown Automata: Application to Model-Checking",
 booktitle    = "Proceedings of CONCUR'97",
 pages        = "135--150",
 doi          = "10.1007/3-540-63141-0\_10",
)
@inproceedings(BM04,
 author       = "A. Bouajjani and A. Meyer",
 year         = "2004",
 title        = "Symbolic Reachability Analysis of Higher-Order Context-Free Processes",
 booktitle    = "Proceedings of FSTTCS'04",
 pages        = "135--147",
 doi          = "10.1007/978-3-540-30538-5\_12",
)
@inproceedings(BCHS12,
 author       = "C. H. Broadbent and A. Carayol and M. Hague and O. Serre",
 year         = "2012",
 title        = "A Saturation Method for Collapsible Pushdown Systems",
 booktitle    = "Proceedings of ICALP'12",
 pages        = "165--176",
 doi          = "10.1007/978-3-642-31585-5\_18",
)
@inproceedings(BCHS13,
 author       = "C. H. Broadbent and A. Carayol and M. Hague and O. Serre",
 year         = "2013",
 title        = "C-SHORe: a collapsible approach to higher-order verification",
 booktitle    = "Proceedings of ICFP'13",
 pages        = "13--24",
 doi          = "10.1145/2500365.2500589",
)
@inproceedings(BK13,
 author       = "C. H. Broadbent and N. Kobayashi",
 year         = "2013",
 title        = "Saturation-Based Model Checking of Higher-Order Recursion Schemes",
 booktitle    = "Proceedings of CSL'13",
 pages        = "129--148",
 doi          = "10.4230/LIPIcs.CSL.2013.129",
)
@article(Buchi64,
 author       = "R. J B{\"u}chi",
 year         = "1964",
 title        = "Regular canonical systems",
 journal      = "Archive for Mathematical Logic",
 volume       = "6",
 number       = "3",
 pages        = "91--111",
 doi          = "10.1007/BF01969548",
)
@inproceedings(Cachat02,
 author       = "T. Cachat",
 year         = "2002",
 title        = "Symbolic Strategy Synthesis for Games on Pushdown Graphs",
 booktitle    = "Proceedings of ICALP'02",
 pages        = "704--715",
 doi          = "10.1007/3-540-45465-9\_60",
)
@phdthesis(Cachat03,
 author       = "T. Cachat",
 year         = "2003",
 title        = "Games on Pushdown Graphs and Extensions",
 school       = "RWTH Aachen",
 url          = "http://www.liafa.jussieu.fr/~txc/Download/Cachat-PhD.pdf",
)
@techreport(Caucal88,
 author       = "D. Caucal",
 year         = "1988",
 title        = "{R{\'e}critures suffixes de mots}",
 type         = "Research Report",
 number       = "RR-0871",
 institution  = "INRIA",
)
@inproceedings(Caucal90,
 author       = "D. Caucal",
 year         = "1990",
 title        = "On the Regular Structure of Prefix Rewriting",
 booktitle    = "Proceedings of CAAP'90",
 series       = "Lecture Notes in Computer Science",
 volume       = "431",
 publisher    = "Springer",
 pages        = "87--102",
 doi          = "10.1007/3-540-52590-4\_42",
)
@inproceedings(Caucal08,
 author       = "D. Caucal",
 year         = "2008",
 title        = "Deterministic graph grammars",
 editor       = "J{\"o}rg Flum and Erich Gr{\"a}del and Thomas Wilke",
 booktitle    = "Logic and Automata: History and Perspectives in Honor of Wolfgang Thomas",
 series       = "Texts in Logic and Games",
 volume       = "2",
 publisher    = "Amsterdam University Press",
 pages        = "169--250",
)
@inproceedings(CKSY05,
 author       = "E. M. Clarke and D. Kroening and N. Sharygina and K. Yorav",
 year         = "2005",
 title        = "SATABS: SAT-Based Predicate Abstraction for ANSI-C",
 booktitle    = "Proceedings of TACAS'05",
 pages        = "570--574",
)
@inproceedings(DTHL87,
 author       = "M. Dauchet and S. Tison and T. Heuillard and P. Lescanne",
 year         = "1987",
 title        = "Decidability of the Confluence of Ground Term Rewriting Systems",
 booktitle    = "Proceedings of LICS'87",
 pages        = "353--359",
)
@inproceedings(EHRS00,
 author       = "J. Esparza and D. Hansel and P. Rossmanith and S. Schwoon",
 year         = "2000",
 title        = "Efficient Algorithms for Model Checking Pushdown Systems",
 booktitle    = "Proceedings of CAV'00",
 pages        = "232--247",
 doi          = "10.1007/10722167\_20",
)
@inproceedings(ES01,
 author       = "J. Esparza and S. Schwoon",
 year         = "2001",
 title        = "A BDD-Based Model Checker for Recursive Programs",
 booktitle    = "Proceedings of CAV'01",
 pages        = "324--336",
 doi          = "10.1007/3-540-44585-4\_30",
)
@article(FWW97,
 author       = "A. Finkel and B. Willems and P. Wolper",
 year         = "1997",
 title        = "A direct symbolic approach to model checking pushdown systems",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "9",
 pages        = "27--37",
 doi          = "10.1007/3-540-45465-9\_60",
)
@article(Greibach67,
 author       = "S. A. Greibach",
 year         = "1967",
 title        = "A note on pushdown store automata and regular systems",
 journal      = "Proceedings of the American Mathematical Society",
 pages        = "263--268",
 doi          = "10.1090/S0002-9939-1967-0209086-1",
)
@inproceedings(H13,
 author       = "M. Hague",
 year         = "2013",
 title        = "Saturation of Concurrent Collapsible Pushdown Systems",
 booktitle    = "Proceedings of FSTTCS'13",
 pages        = "313--325",
 doi          = "10.4230/LIPIcs.FSTTCS.2013.313",
)
@inproceedings(HMOS08,
 author       = "M. Hague and A. S. Murawski and C.-H. Luke Ong and O. Serre",
 year         = "2008",
 title        = "Collapsible Pushdown Automata and Recursion Schemes",
 booktitle    = "Proceedings of LICS'08",
 pages        = "452--461",
 doi          = "10.1109/LICS.2008.34",
)
@article(HO08,
 author       = "M. Hague and C.-H. L. Ong",
 year         = "2008",
 title        = "Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems",
 journal      = "Logical Methods in Computer Science",
 volume       = "4",
 number       = "4",
 doi          = "10.2168/LMCS-4(4:14)2008",
)
@inproceedings(HO10,
 author       = "M. Hague and C.-H. L. Ong",
 year         = "2010",
 title        = "Analysing Mu-Calculus Properties of Pushdown Systems",
 booktitle    = "Proceedings of SPIN'10",
 pages        = "187--192",
 doi          = "10.1007/978-3-642-16164-3\_14",
)
@inproceedings(HagueO09,
 author       = "M. Hague and C.-H. Luke Ong",
 year         = "2009",
 title        = "Winning Regions of Pushdown Parity Games: A Saturation Method",
 booktitle    = "Proceedings of CONCUR'09",
 pages        = "384--398",
 doi          = "10.1007/978-3-642-04081-8\_26",
)
@article(JM77,
 author       = "N. D. Jones and S. S. Muchnick",
 year         = "1977",
 title        = "Even Simple Programs Are Hard To Analyze",
 journal      = "J. ACM",
 volume       = "24",
 number       = "2",
 pages        = "338--350",
 doi          = "10.1145/322003.322016",
)
@inproceedings(KNU02,
 author       = "T. Knapik and D. Niwinski and P. Urzyczyn",
 year         = "2002",
 title        = "Higher-Order Pushdown Trees Are Easy",
 booktitle    = "Proceedings of FoSSaCS'02",
 pages        = "205--222",
 doi          = "10.1007/3-540-45931-6\_15",
)
@inproceedings(KNUW05,
 author       = "T. Knapik and D. Niwinski and P. Urzyczyn and I. Walukiewicz",
 year         = "2005",
 title        = "Unsafe Grammars and Panic Automata",
 booktitle    = "Proceedings of ICALP'05",
 pages        = "1450--1461",
 doi          = "10.1007/11523468\_117",
)
@inproceedings(LR06,
 author       = "A. Lal and T. W. Reps",
 year         = "2006",
 title        = "Improving Pushdown System Model Checking",
 booktitle    = "Proceedings of CAV'06",
 pages        = "343--357",
 doi          = "10.1007/11817963\_32",
)
@inproceedings(LRB05,
 author       = "A. Lal and T. W. Reps and G. Balakrishnan",
 year         = "2005",
 title        = "Extended Weighted Pushdown Systems",
 booktitle    = "Proceedings of CAV'05",
 pages        = "434--448",
 doi          = "10.1007/11513988\_44",
)
@article(LL13,
 author       = "M. Lang and C. L{\"o}ding",
 year         = "2013",
 title        = "Modeling and Verification of Infinite Systems with Resources",
 journal      = "Logical Methods in Computer Science",
 volume       = "9",
 number       = "4",
 doi          = "10.2168/LMCS-9(4:22)2013",
)
@article(M76,
 author       = "A. N. Maslov",
 year         = "1976",
 title        = "Multilevel stack automata",
 journal      = "Problems of Information Transmission",
 volume       = "15",
 pages        = "1170--1174",
)
@inproceedings(Q08,
 author       = "S. Qadeer",
 year         = "2008",
 title        = "The Case for Context-Bounded Verification of Concurrent Programs",
 booktitle    = "Proceedings of the SPIN'08",
 publisher    = "Springer-Verlag",
 address      = "Berlin, Heidelberg",
 pages        = "3--6",
 doi          = "10.1007/978-3-540-85114-1\_2",
)
@article(RSJM05,
 author       = "T. W. Reps and S. Schwoon and S. Jha and D. Melski",
 year         = "2005",
 title        = "Weighted pushdown systems and their application to interprocedural dataflow analysis",
 journal      = "Sci. Comput. Program.",
 volume       = "58",
 number       = "1-2",
 pages        = "206--263",
 doi          = "10.1016/j.scico.2005.02.009",
)
@book(Sakarovitch09,
 author       = "J. Sakarovitch",
 year         = "2009",
 title        = "Elements of Automata Theory",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/CBO9781139195218",
)
@phdthesis(S02,
 author       = "S. Schwoon",
 year         = "2002",
 title        = "Model-checking Pushdown Systems",
 school       = "Technical University of Munich",
)
@phdthesis(Serre04,
 author       = "O. Serre",
 year         = "2004",
 title        = "Contribution \`a l’\'etude des jeux sur des graphes de processus \`a pile",
 school       = "Universit\'e Paris 7 -- Denis Diderot, UFR d’informatique",
 url          = "http://tel.archives-ouvertes.fr/tel-00011326",
)
@article(S08,
 author       = "A. Seth",
 year         = "2008",
 title        = "An Alternative Construction in Symbolic Reachability Analysis of Second Order Pushdown Systems",
 journal      = "Int. J. Found. Comput. Sci.",
 volume       = "19",
 number       = "4",
 pages        = "983--998",
 doi          = "10.1142/S012905410800608X",
)
@inproceedings(S09,
 author       = "A. Seth",
 year         = "2009",
 title        = "Games on Higher Order Multi-stack Pushdown Systems",
 booktitle    = "Proceedings of RP'09",
 pages        = "203--216",
 doi          = "10.1007/978-3-642-04420-5\_19",
)
@inproceedings(S10,
 author       = "A. Seth",
 year         = "2010",
 title        = "Global Reachability in Bounded Phase Multi-stack Pushdown Systems",
 booktitle    = "Proceedings of CAV'10",
 pages        = "615--628",
 doi          = "10.1007/978-3-642-14295-6\_53",
)
@inproceedings(ST11,
 author       = "F. Song and T. Touili",
 year         = "2011",
 title        = "Efficient CTL Model-Checking for Pushdown Systems",
 booktitle    = "Proceedings of CONCUR'11",
 pages        = "434--449",
 doi          = "10.1007/978-3-642-23217-6\_29",
)
@inproceedings(ST12b,
 author       = "F. Song and T. Touili",
 year         = "2012",
 title        = "{PuMoC}: a CTL model-checker for sequential programs",
 booktitle    = "Proceedings of ASE'12",
 pages        = "346--349",
 doi          = "10.1145/2351676.2351743",
)
@inproceedings(ST12,
 author       = "F. Song and T. Touili",
 year         = "2012",
 title        = "Pushdown Model Checking for Malware Detection",
 booktitle    = "Proceedings of TACAS'12",
 pages        = "110--125",
 doi          = "10.1007/978-3-642-28756-5\_9",
)
@inproceedings(ST13,
 author       = "F. Song and T. Touili",
 year         = "2013",
 title        = "{LTL} Model-Checking for Malware Detection",
 booktitle    = "Proceedings of TACAS'13",
 pages        = "416--431",
 doi          = "10.1007/978-3-642-36742-7\_29",
)
@inproceedings(ST13c,
 author       = "F. Song and T. Touili",
 year         = "2013",
 title        = "Model Checking Dynamic Pushdown Networks",
 booktitle    = "Proceedings of APLAS'13",
 pages        = "33--49",
 doi          = "10.1007/978-3-319-03542-0\_3",
)
@inproceedings(ST13b,
 author       = "F. Song and T. Touili",
 year         = "2013",
 title        = "{PoMMaDe}: pushdown model-checking for malware detection",
 booktitle    = "Proceedings of ESEC/FSE'13",
 pages        = "607--610",
 doi          = "10.1145/2491411.2494599",
)
@inproceedings(SBSE07,
 author       = "D. Suwimonteerabuth and F. Berger and S. Schwoon and J. Esparza",
 year         = "2007",
 title        = "jMoped: A Test Environment for Java Programs",
 booktitle    = "Proceedings of CAV'07",
 pages        = "164--167",
 doi          = "10.1007/978-3-540-73368-3\_19",
)
@inproceedings(SES08,
 author       = "D. Suwimonteerabuth and J. Esparza and S. Schwoon",
 year         = "2008",
 title        = "Symbolic Context-Bounded Analysis of Multithreaded Java Programs",
 booktitle    = "Proceedings of SPIN'08",
 pages        = "270--287",
 doi          = "10.1007/978-3-540-85114-1\_19",
)
@inproceedings(SSE05,
 author       = "D. Suwimonteerabuth and S. Schwoon and J. Esparza",
 year         = "2005",
 title        = "jMoped: A Java Bytecode Checker Based on Moped",
 booktitle    = "Proceedings of TACAS'05",
 pages        = "541--545",
 doi          = "10.1007/978-3-540-31980-1\_35",
)
@inproceedings(SSE06,
 author       = "D. Suwimonteerabuth and S. Schwoon and J. Esparza",
 year         = "2006",
 title        = "Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains",
 booktitle    = "Proceedings of ATVA'06",
 pages        = "141--153",
 doi          = "10.1007/11901914\_13",
)
@inproceedings(lTMP07,
 author       = "S. La Torre and P. Madhusudan and G. Parlato",
 year         = "2007",
 title        = "A Robust Class of Context-Sensitive Languages",
 booktitle    = "Proceedings of LICS'07",
 pages        = "161--170",
 doi          = "10.1109/LICS.2007.9",
)
@inproceedings(lTN11,
 author       = "S. La Torre and M. Napoli",
 year         = "2011",
 title        = "Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations",
 booktitle    = "Proceedings of CONCUR'11",
 pages        = "203--218",
 doi          = "10.1007/978-3-642-23217-6\_14",
)
@misc(WALi,
 author       = "{WALi: Weighted Automata Library}",
 howpublished = "\url {https://research.cs.wisc.edu/wpis/wpds/download.php}",
)
@article(W01,
 author       = "I. Walukiewicz",
 year         = "2001",
 title        = "Pushdown Processes: Games and Model-Checking",
 journal      = "Inf. Comput.",
 volume       = "164",
 number       = "2",
 pages        = "234--263",
 doi          = "10.1006/inco.2000.2894",
)
@misc(wpdsLib,
 author       = "{WPDS Library}",
 howpublished = "\url {http://www2.informatik.uni-stuttgart.de/fmi/szs/tools/wpds/}",
)