@inproceedings(abdulla2012dense, author = "P. A. Abdulla and M. F. Atig and J. Stenman", year = "2012", title = "Dense-timed pushdown automata", booktitle = "Logic in Computer Science (LICS), 2012 27th Annual IEEE Symposium on", organization = "IEEE", doi = "10.1109/LICS.2012.15", ) @inproceedings(PFJ12, author = "P. A. Abdulla and M. F. Atig and J. Stenman", year = "2012", title = "The Minimal Cost Reachability Problem in Priced Timed Pushdown Systems", booktitle = "LATA", doi = "10.1007/978-3-642-28332-1\_6", ) @incollection(abdulla2005decidability, author = "P. A. Abdulla and P. Mahata and R. Mayr", year = "2005", title = "Decidability of Zenoness, syntactic boundedness and token-liveness for dense-timed petri nets", booktitle = "FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science", publisher = "Springer", pages = "58--70", doi = "10.1007/978-3-540-30538-5\_6", ) @phdthesis(Alur91, author = "R. Alur", year = "1991", title = "{Techniques for Automatic Verification of Real-Time Systems}", school = "Dept. of Computer Sciences, Stanford University", ) @inproceedings(AlurD90, author = "R. Alur and D. L. Dill", year = "1990", title = "Automata For Modeling Real-Time Systems", booktitle = "ICALP", series = "LNCS", volume = "443", publisher = "Springer", pages = "322--335", doi = "10.1007/BFb0032042", ) @article(AlurD94, author = "R. Alur and D. L. Dill", year = "1994", title = "A Theory of Timed Automata", journal = "Theor. Comput. Sci.", volume = "126", number = "2", pages = "183--235", doi = "10.1016/0304-3975(94)90010-8", ) @inproceedings(BMP10, author = "M. Benerecetti and S. Minopoli and A. Peron", year = "2010", title = "Analysis of Timed Recursive State Machines", booktitle = "TIME", publisher = "IEEE Computer Society", pages = "61--68", doi = "10.1109/TIME.2010.10", ) @inproceedings(BER94, author = "A. Bouajjani and R. Echahed and R. Robbana", year = "1994", title = "On the Automatic Verification of Systems with Continuous Variables and Unbounded Discrete Data Structures", booktitle = "Hybrid Systems", series = "LNCS 999", publisher = "Springer", pages = "64--85", doi = "10.1007/3-540-60472-3\_4", ) @inproceedings(BEM97, author = "A. Bouajjani and J. Esparza and O. Maler", year = "1997", title = "Reachability Analysis of Pushdown Automata: Application to Model-Checking", booktitle = "CONCUR", series = "LNCS 1243", publisher = "Springer", pages = "135--150", doi = "10.1007/3-540-63141-0\_10", ) @inproceedings(BCFL04, author = "P. Bouyer and F. Cassez and E. Fleury and K. G. Larsen", year = "2004", title = "Optimal Strategies in Priced Timed Game Automata", booktitle = "FSTTCS", series = "LNCS 3328", publisher = "Springer", pages = "148--160", doi = "10.1007/978-3-540-30538-5\_13", ) @incollection(BL-litron08, author = "P. Bouyer and F. Laroussinie", year = "2008", title = "Model Checking Timed Automata", editor = "Stephan Merz and Nicolas Navet", booktitle = "Modeling and Verification of Real-Time Systems", publisher = "ISTE Ltd. -- John Wiley \& Sons, Ltd.", pages = "111--140", doi = "10.1002/9780470611012.ch4", ) @article(Dang03, author = "Z. Dang", year = "2003", title = "Pushdown timed automata: a binary reachability characterization and safety verification", journal = "Theor. Comput. Sci.", volume = "302", number = "1-3", pages = "93--121", doi = "10.1016/S0304-3975(02)00743-0", ) @article(DBIK04, author = "Z. Dang and T. Bultan and O. H. Ibarra and R. A. Kemmerer", year = "2004", title = "Past pushdown timed automata and safety verification", journal = "Theor. Comput. Sci.", volume = "313", number = "1", pages = "57--71", doi = "10.1016/j.tcs.2003.10.004", ) @inproceedings(DIBKS00, author = "Z. Dang and O. H. Ibarra and T. Bultan and R. A. Kemmerer and J. Su", year = "2000", title = "Binary Reachability Analysis of Discrete Pushdown Timed Automata", booktitle = "CAV", series = "LNCS 1855", publisher = "Springer", pages = "69--84", doi = "10.1007/10722167\_9", ) @inproceedings(EmmiM06, author = "M. Emmi and R. Majumdar", year = "2006", title = "Decision Problems for the Verification of Real-Time Software", booktitle = "HSCC", series = "LNCS 3927", publisher = "Springer", pages = "200--211", doi = "10.1007/11730637\_17", ) @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 = "CAV", series = "LNCS", volume = "1855", publisher = "Springer", 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 = "CAV", series = "LNCS", volume = "2102", publisher = "Springer", pages = "324--336", doi = "10.1007/3-540-44585-4\_30", ) @article(herbreteau2012efficient, author = "F. Herbreteau and B. Srivathsan and I. Walukiewicz", year = "2012", title = "Efficient emptiness check for timed b{\"u}chi automata", journal = "Formal Methods in System Design", volume = "40", number = "2", pages = "122--146", doi = "10.1007/s10703-011-0133-1", ) @article(Heussner:2012:LMCS, author = "A. Heu{\ss }ner and J. Leroux and A. Muscholl and G. Sutre", year = "2012", title = "Reachability Analysis of Communicating Pushdown Systems", journal = "Logical Methods in Computer Science", volume = "8", number = "3:23", pages = "1--20", doi = "10.2168/LMCS-8(3:23)2012", ) @phdthesis(Sch02b, author = "S. Schwoon", year = "2002", title = "Model-Checking Pushdown Systems", school = "Technische Universit{\"a}t M{\"u}nchen", ) @inproceedings(Tripakis99, author = "S. Tripakis", year = "1999", title = "Verifying Progress in Timed Systems", booktitle = "ARTS", series = "LNCS", volume = "1601", publisher = "Springer", pages = "299--314", doi = "10.1007/3-540-48778-6\_18", ) @inproceedings(Trivedi:2010, author = "A. Trivedi and D. Wojtczak", year = "2010", title = "Recursive timed automata", booktitle = "Proceedings of the 8th international conference on Automated technology for verification and analysis", series = "ATVA", pages = "306--324", doi = "10.1007/978-3-642-15643-4\_23", )