References

  1. 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.
  2. 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.
  3. 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.
  4. Y. Bar-Hillel, M. Perles & E. Shamir (1961): On formal properties of simple phrase structure grammars. Z. Phonetik Sprachwiss. Kommunikat. 14, pp. 143–172.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. R. J Büchi (1964): Regular canonical systems. Archive for Mathematical Logic 6(3), pp. 91–111, doi:10.1007/BF01969548.
  13. 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.
  14. T. Cachat (2003): Games on Pushdown Graphs and Extensions. RWTH Aachen. Available at http://www.liafa.jussieu.fr/~txc/Download/Cachat-PhD.pdf.
  15. D. Caucal (1988): Récritures suffixes de mots. Research Report RR-0871. INRIA.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. M. Hague (2013): Saturation of Concurrent Collapsible Pushdown Systems. In: Proceedings of FSTTCS'13, pp. 313–325, doi:10.4230/LIPIcs.FSTTCS.2013.313.
  25. 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.
  26. 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.
  27. 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.
  28. 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.
  29. 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.
  30. 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.
  31. 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.
  32. A. Lal & T. W. Reps (2006): Improving Pushdown System Model Checking. In: Proceedings of CAV'06, pp. 343–357, doi:10.1007/11817963_32.
  33. 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.
  34. 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.
  35. A. N. Maslov (1976): Multilevel stack automata. Problems of Information Transmission 15, pp. 1170–1174.
  36. 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.
  37. 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.
  38. J. Sakarovitch (2009): Elements of Automata Theory. Cambridge University Press, doi:10.1017/CBO9781139195218.
  39. S. Schwoon (2002): Model-checking Pushdown Systems. Technical University of Munich.
  40. 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.
  41. 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.
  42. 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.
  43. 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.
  44. 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.
  45. 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.
  46. 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.
  47. 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.
  48. 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.
  49. 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.
  50. 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.
  51. 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.
  52. 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.
  53. 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.
  54. 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.
  55. 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.
  56. WALi: Weighted Automata Library. https://research.cs.wisc.edu/wpis/wpds/download.php.
  57. I. Walukiewicz (2001): Pushdown Processes: Games and Model-Checking. Inf. Comput. 164(2), pp. 234–263, doi:10.1006/inco.2000.2894.
  58. WPDS Library. http://www2.informatik.uni-stuttgart.de/fmi/szs/tools/wpds/.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org