--------- Foundational papers on VPAs/nested word languages -------

  1. Visibly pushdown languages.
    Rajeev Alur, P. Madhusudan
    Annual ACM Symposium on Theory of Computing (STOC), Chicago, IL, USA, 2004.
    Online link

  2. Adding Nesting Structure to Words.
    R. Alur, P. Madhusudan
    Developments in Language Theory (DLT),
    Santa Barbara, USA, 2006.
    Online link

    ----------------- Relating VPAs and tree automata -----------

  3. Marrying words and trees
    R. Alur
    Symposium on Principles of Database Systems (PODS), Beijing, China, 2007.
    Online link

  4. Streaming Tree Automata
    Olivier Gauwin, Joachim Niehren, Yves Roos
    Information Processing Letters (2008)
    Online link

  5. Visibly Pushdown Languages and Term Rewriting
    Jacques Chabin and Pierre Réty
    Frontiers of Combining Systems (FroCos), LNCS 4720
    Online link

    ---------------- Congruences and Minimization of VPAs---------------

  6. Congruences for visibly pushdown languages
    R. Alur, V. Kumar, P. Madhusudan, M. Viswanathan
    Int'l Coll. on Automata, Lang. and Prog. (ICALP), Lisboa, Portugal, 2005.
    Online link

  7. Minimization, Learning, and Conformance Testing of Boolean Programs
    V. Kumar, P. Madhusudan, M. Viswanathan
    International Conference on Concurrency Theory (CONCUR), Bonn, Germany, 2006.
    Online link

  8. Minimizing Variants of Visibly Pushdown Automata
    Patrick Chervet, Igor Walukiewicz
    International Symposium on Mathematical Foundations of Computer Science (MFCS), Ceský Krumlov, Czech Republic, 2007.
    Online link

    ------- Temporal/modal logics with applications to verification ------

  9. A Temporal Logic for Nested Calls and Returns
    Rajeev Alur, K. Etessami, P. Madhusudan
    Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Barcelona, Spain, 2004.
    Online link

  10. A fixpoint calculus for local and global program flows
    R. Alur, S. Chaudhuri, P. Madhusudan
    Principles of Programming Languages (POPL), Charleston, USA, 2006.
    Online link

  11. First-Order and Temporal Logics for Nested Words
    Rajeev Alur, Marcelo Arenas, Pablo Barcelo, Kousha Etessami, Neil Immerman and Leonid Libkin
    Annual IEEE Symposium on Logic in Computer Science Wroclaw, Poland
    Online link

  12. The Complexity of CaRet + Chop
    Laura Bozzelli
    International Symposium on Temporal Representation and Reasoning (TIME), Montreal, Canada, 2008.

  13. Propositional dynamic logic with recursive programs
    Christof Löding, Carsten Lutz, Olivier Serre
    International Conference on Foundations of Software Science and Computation Structures (FOSSACS), Vienna, Austria, 2006.
    Online link

  14. Propositional dynamic logic with recursive programs
    Christof Löding, Carsten Lutz, Olivier Serre
    Journal of Logic and Algebraic Programming, 73:51-69, 2007.
    Online link

  15. Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages
    Laura Bozzelli
    International Conference on Concurrency Theory (CONCUR), Lisbon, Portugal, 2007.

    --------- (More) Applications to Verification --------

  16. Instrumenting C Programs with Nested Word Monitors
    Swarat Chaudhuri, Rajeev Alur
    International SPIN Workshop on Model Checking Software (SPIN), Berlin, Germany.
    Online link

  17. Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --
    Grigore Rosu, Feng Chen and Thomas Ball
    International Workshop on Runtime Verification (RV), Budapest, Hungary, 2008.
    Online link

  18. Context-Bounded Analysis of Concurrent Queue Systems
    S. La Torre, P. Madhusudan, G. Parlato
    Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary, 2008.
    Online link

    ---------------------- Applications to XML -----------------

  19. Visibly pushdown expression effects for XML stream processing
    Corin Pitcher
    ACM Sigplan Workshop on Programming Language Technologies for XML (PLAN-X), Longbeach, California, USA.
    Online link

  20. Visibly Pushdown Automata for Streaming XML
    V. Kumar, P. Madhusudan, M. Viswanathan
    Int'l World Wide Web Conference (WWW) Alberta, Canada, 2007.
    Online link

  21. Query Automata for Nested Words
    P. Madhusudan, Mahesh Viswanathan.
    Unpublished manuscript.
    Online link

  22. Querying Streaming XML Using Visibly Pushdown Automata
    Robert Clark
    University of Illinois Technical Report
    Online link
    Undergraduate thesis with P. Madhusudan; provides a translation from XPath to query VPAs.

    --------- Applications to Programming Languages --------

  23. Third-order Idealized Algol with iteration is decidable
    Andrzej S. Murawski, Igor Walukiewicz
    Int'l Conf. on Foundations of Software Science and Computational Structures (FOSSACS), Edinburgh, UK.
    Online link

  24. Reachability games and game semantics: comparing nondeterministic programs
    Andrzej S. Murawski
    Annual IEEE Symposium on Logic in Computer Science, Pittsburgh, Pennsylvania
    Online link

  25. VPA-Based Aspects: Better Support for AOP over Protocols
    Dong Ha Nguyen, Mario Südholt
    IEEE International Conference on Software Engineering and Formal Methods (SEFM), Pune, India, 2006.

  26. Property-preserving evolution of components using VPA-based aspects
    Dong Ha Nguyen, Mario Südholt
    International Symposium on Distributed Objects and Applications (DOA'07), Vilamoura, Algarve, Portugal, 2007. Pune, India, 2006.
    Online link

  27. Towards correct evolution of components using VPA-based aspects
    Dong Ha Nguyen, Mario Südholt
    ECOOP Workshop on Reflection, AOP and Meta-Data for Software Evolution (RAM-SE), Berlin, Germany, 2007.
    Online link

  28. Detecting Interference Among Aspects
    E. Katz, S. Katz, W. Havinga, T. Staijen, N. Weston, F. Taiani, A. Rashid, D. H. Nguyen, M. Südholt
    Deliverable, European Network of Excellence on Aspect-Oriented Software Development (AOSD)
    Online link

    ---------------------- Further Theory of VPAs -----------------

  29. Visibly pushdown games.
    C. Löding, P. Madhusudan, O. Serre
    Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Chennai, India, 2004.
    Online link

  30. Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
    Jiří Srba
    EACSL Annual Conference on Computer Science Logic (CSL), Szeged, Hungary, 2006.
    Online link

  31. A Grammatical Representation of Visibly Pushdown Languages
    Joachim Baran, Howard Barringer
    International Workshop on Logic, Language, Information and Computation (WOLLIC), Rio de Janeiro, Brazil.

  32. The word problem for visibly pushdown languages described by grammars
    Salvatore La Torre, Margherita Napoli, Mimmo Parente
    Formal Methods in System Design, Volume 31, Issue 3, 2007.

  33. On the Membership Problem for Visibly Pushdown Languages
    Salvatore La Torre, Margherita Napoli, Mimmo Parente
    International Symposium on Automated Technology for Verification and Analysis (ATVA), Beijing, China.

  34. Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization
    Marcelo Arenas, Pablo Barceló, Leonid Libkin
    International Colloquium on Automata, Languages and Programming (ICALP), Wroclaw, Poland, 2007.
    Online link

  35. Regularity problems for visibly pushdown languages
    Vince Bárány, Christof Löding, Olivier Serre
    Annual Symposium on Theoretical Aspects of Computer Science (STACS), Marseille, France, 2006.
    Online link

    ---------------------- Complexity Theory -----------------

  36. Arithmetizing classes around NC^1 and L
    Nutan Limaye, Meena Mahajan, B. V. Raghavendra Rao
    To appear in Theory of Computing systems, Special issue of STACS 2007.
    Conference version: Symposium on Theoretical Aspects of Computer Science, Aachen, Germany, 2007.
    Online link
    Note: The conference version has an error: see Erratum. The journal version and the paper by Limaye, Mahajan, and Meyer in CSR'08 fixes the error.

  37. On the Complexity of Membership and Counting in Height-Deterministic Pushdown Automata
    Nutan Limaye, Meena Mahajan, Antoine Meyer
    Computer Science - Theory and Applications, International Computer Science Symposium in Russia (CSR), Moscow, Russia, 2008.
    Online link

  38. An Infinite Automaton Characterization of Double Exponential Time
    S. La Torre, P. Madhusudan, G. Parlato
    EACSL Annual Conference on Computer Science Logic (CSL), Bertinoro, Italy, 2008.
    Online link

    --------- Multiply nested words/ multi-stack VPAs --------

  39. A Robust Class of Context-Sensitive Languages
    S. La Torre, P. Madhusudan, G. Parlato
    22nd IEEE Symp. on Logic in Computer Science (LICS), Wroclaw, Poland, 2007.
    Online link

  40. A Note on Nested Words
    Andreas Blass, Yuri Gurevich
    Manuscript
    Online link

  41. 2-Visibly Pushdown Automata
    Dario Carotenuto, Aniello Murano and Adriano Peron
    International Conference on Developments in Language Theory (DLT), Turku, Finland, 2007.
    Online link
    Note: The determinization construction in this paper is wrong, and in fact, 2-VPAs are not determinizable. We do not know whether they are still closed under complement.
    See here for a proof of non-determinizability and the error.

  42. Realizability of Concurrent Recursive Programs
    Benedikt Bollig, Manuela-Lidia Grindei, and Peter Habermehl
    Research Report LSV-08-29, Laboratoire Spécification et Vérification, ENS Cachan, France,2008.
    Online link

  43. On the expressive power of 2-stack visibly pushdown automata
    Benedikt Bollig
    Research Report LSV-07-27, Laboratoire Spécification et Vérification, ENS Cachan, France, 2007.
    Online link

  44. A note on an extension of PDL
    Stefan Göller, Dirk Nowotka
    Journal of Applied Logic
    Online link

  45. Games on Multi-Stack Pushdown Systems
    Anil Seth
    Symposium on Logical Foundations of Computer Science, Deerfield Beach, Florida, USA, 2009.

    --------- Extensions of VPAs --------

  46. Languages of nested trees
    R. Alur, S. Chaudhuri, P. Madhusudan
    Computer Aided Verification (CAV), Seattle, USA, 2006.
    Online link

  47. Synchronization of Pushdown Automata
    Didier Caucal
    International Conference on Developments in Language Theory (DLT), Santa Barbara, USA, 2006.

  48. Visibly Tree Automata with Memory and Constraints
    Hubert Comon-Lundh, Florent Jacquemard, Nicolas Perrin
    Logical Methods in Computer Science, Vol.4(2), Paper 8, 2008.
    Online link

  49. Tree Automata with Memory, Visibility and Structural Constraints
    Hubert Comon-Lundh, Florent Jacquemard, Nicolas Perrin
    International Conference on Foundations of Software Science and Computational Structures (FOSSACS), Braga, Portugal.
    Online link

  50. Synchronization of Grammars
    Didier Caucal, Stéphane Hassen
    Computer Science - Theory and Applications, International Computer Science Symposium in Russia (CSR), Moscow, Russia, 2008.
    Online link

  51. Height-Deterministic Pushdown Automata
    Dirk Nowotka and Jiří Srba
    International Symposium on Mathematical Foundations of Computer Science, Ceský Krumlov, Czech Republic,
    Online link

  52. Visibly Pushdown Transducers
    Jean-François Raskin and Frédéric Servais
    International Colloquium on Automata, Languages and Programming (ICALP), Reykjavik, Iceland, 2008.
    Online link

  53. Decision Problems for the Verification of Real-Time Software
    Michael Emmi and Rupak Majumdar
    International Workshop on Hybrid Systems: Computation and Control, Santa Barbara, CA, USA.
    Online link

---------------------- Tools ------------------------

  • VPAlib: Visibly Pushdown Automata Library
    Ha Nguyen, École des Mines de Nantes, France.
    Basic constructions on VPAs are implemented.

  • VPAchecker
    Nguyen Van TangHa Nguyen, JAIST, Japan.
    A Prototype Tool for Automatic Checking Universality and Inclusion of Visibly Pushdown Automata

  • PAL
    Swarat Chaudhuri, Rajeev Alur
    A language and tool for monitoring C programs against nested word specifications.

  • MOP/JavaMOP PTCaret
    Feng Chen, Grigore Rosu, Thomas Ball
    Monitoring tool for Past Time Linear Temporal Logic with Calls and Returns (Past-Time CaRet)

  • Querying XML using VPAs
    Jerry Chen
    Undergraduate thesis project (under Madhusudan) at UIUC. Can either (a) given a VPA and an XML document, report using a streaming algorithm whether the document is accepted by the VPA, or (b) given a query VPA and an XML document, output using a streaming query processor the set of all positions that satisfy the query expressed by the query VPA.