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