@article(Alur, author = "Rajeev Alur and P. Madhusudan", year = "2009", title = "Adding nesting structure to words", journal = "J. ACM", volume = "56", number = "3", url = "http://doi.acm.org/10.1145/1516512.1516518", ) @article(faouziORDERED, author = "Mohamed Faouzi Atig", year = "2012", title = "Model-Checking of Ordered Multi-Pushdown Automata", journal = "Logical Methods in Computer Science", volume = "8", number = "3", url = "http://dx.doi.org/10.2168/LMCS-8(3:20)2012", ) @inproceedings(ahmedLTL, author = "Mohamed Faouzi Atig and Ahmed Bouajjani and K. Narayan Kumar and Prakash Saivasan", year = "2012", title = "Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding", editor = "Supratik Chakraborty and Madhavan Mukund", booktitle = "ATVA", series = "Lecture Notes in Computer Science", volume = "7561", publisher = "Springer", pages = "152--166", url = "http://dx.doi.org/10.1007/978-3-642-33386-6_13", ) @article(Bodlaender, author = "Hans L. Bodlaender", year = "1993", title = "A Tourist Guide through Treewidth", journal = "Acta Cybern.", volume = "11", number = "1-2", pages = "1--22", url = "http://www.inf.u-szeged.hu/kutatas/actacybernetica/vol11n12/bodlaen/bodlaen.xml", ) @article(Buchi60, author = "J. B{\"{u}}chi", year = "1960", title = "Weak second-order Arithmetic and Finite Automata.", journal = "Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik", volume = "6", pages = "66--92", doi = "10.1002/malq.19600060105", ) @article(courcelle, author = "Bruno Courcelle", year = "1990", title = "The Monadic Second-Order Logic of Graphs. I. Recognizable Sets of Finite Graphs", journal = "Inf. Comput.", volume = "85", number = "1", pages = "12--75", url = "http://dx.doi.org/10.1016/0890-5401(90)90043-H", ) @inproceedings(javierLICS12, author = "Javier Esparza and Pierre Ganty and Rupak Majumdar", year = "2012", title = "A Perfect Model for Bounded Verification", booktitle = "LICS", publisher = "IEEE", pages = "285--294", url = "http://dx.doi.org/10.1109/LICS.2012.39", ) @inproceedings(Ganesh02, author = "Vijay Ganesh and Sergey Berezin and David L. Dill", year = "2002", title = "Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods", editor = "Mark Aagaard and John W. O'Leary", booktitle = "FMCAD", series = "Lecture Notes in Computer Science", volume = "2517", publisher = "Springer", pages = "171--186", url = "http://dx.doi.org/10.1007/3-540-36126-X_11", ) @techreport(Gomory60, author = "Ralph E. Gomory", year = "1960", title = "An algorithm for the mixed integer problem", type = "Technical Report", institution = "RAND Corporation", ) @article(Heussner, author = "Alexander Heu{\ss }ner", year = "2012", title = "Model Checking Communicating Processes: Run Graphs, Graph Grammars, and MSO", journal = "ECEASST", volume = "47", url = "http://journal.ub.tu-berlin.de/eceasst/article/view/725", ) @article(muschollQUEUE, author = "Alexander Heu{\ss }ner and J{\'e}r{\^o}me Leroux and Anca Muscholl and Gr{\'e}goire Sutre", year = "2012", title = "Reachability Analysis of Communicating Pushdown Systems", journal = "Logical Methods in Computer Science", volume = "8", number = "3", url = "http://dx.doi.org/10.2168/LMCS-8(3:23)2012", ) @inproceedings(phase, author = "Salvatore {La Torre} and P. Madhusudan and Gennaro Parlato", year = "2007", title = "A Robust Class of Context-Sensitive Languages", booktitle = "LICS", publisher = "IEEE Computer Society", pages = "161--170", url = "http://doi.ieeecomputersociety.org/10.1109/LICS.2007.9", ) @inproceedings(gennaroTACAS08, author = "Salvatore {La Torre} and P. Madhusudan and Gennaro Parlato", year = "2008", title = "Context-Bounded Analysis of Concurrent Queue Systems", editor = "C. R. Ramakrishnan and Jakob Rehof", booktitle = "TACAS", series = "Lecture Notes in Computer Science", volume = "4963", publisher = "Springer", pages = "299--314", url = "http://dx.doi.org/10.1007/978-3-540-78800-3_21", ) @inproceedings(salvatoreSCOPED, author = "Salvatore {La Torre} and Margherita Napoli", year = "2011", title = "Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations", editor = "Joost-Pieter Katoen and Barbara K{\"o}nig", booktitle = "CONCUR", series = "Lecture Notes in Computer Science", volume = "6901", publisher = "Springer", pages = "203--218", url = "http://dx.doi.org/10.1007/978-3-642-23217-6_14", ) @inproceedings(salvatoreLOGIC, author = "Salvatore {La Torre} and Margherita Napoli", year = "2012", title = "A Temporal Logic for Multi-threaded Programs", editor = "Jos C. M. Baeten and Thomas Ball and Frank S. de Boer", booktitle = "IFIP TCS", series = "Lecture Notes in Computer Science", volume = "7604", publisher = "Springer", pages = "225--239", url = "http://dx.doi.org/10.1007/978-3-642-33475-7_16", ) @inproceedings(scopedFSTTCS, author = "Salvatore {La Torre} and Gennaro Parlato", year = "2012", title = "Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width", editor = "Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan", booktitle = "FSTTCS", series = "LIPIcs", volume = "18", publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik", pages = "173--184", url = "http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2012.173", ) @article(Land60, author = "A. H. Land and A. G. Doig", year = "1960", title = "An Automatic Method of Solving Discrete Programming Problems", journal = "Econometrica", volume = "28", number = "3", pages = "497--520", doi = "10.2307/1910129", ) @article(LLL82, author = "A. K. Lenstra and H. W. Lenstra Jr. and L. Lovász", year = "1982", title = "Factoring polynomials with rational coefficients", journal = "Mathematische Annalen", volume = "261", number = "4", pages = "515--534", doi = "10.1007/BF01457454", ) @inproceedings(tree-width-popl, author = "P. Madhusudan and Gennaro Parlato", year = "2011", title = "The tree width of auxiliary storage", editor = "Thomas Ball and Mooly Sagiv", booktitle = "POPL", publisher = "ACM", pages = "283--294", url = "http://doi.acm.org/10.1145/1926385.1926419", ) @article(Papadimitriou81, author = "Christos H. Papadimitriou", year = "1981", title = "On the complexity of integer programming", journal = "J. ACM", volume = "28", number = "4", pages = "765--768", url = "http://doi.acm.org/10.1145/322276.322287", ) @article(parikh, author = "Rohit Parikh", year = "1966", title = "On Context-Free Languages", journal = "J. ACM", volume = "13", number = "4", pages = "570--581", url = "http://doi.acm.org/10.1145/321356.321364", ) @article(Pugh92, author = "William Pugh", year = "1992", title = "A Practical Algorithm for Exact Array Dependence Analysis", journal = "Commun. ACM", volume = "35", number = "8", pages = "102--114", url = "http://doi.acm.org/10.1145/135226.135233", ) @inproceedings(boundedCS, author = "Shaz Qadeer and Jakob Rehof", year = "2005", title = "Context-Bounded Model Checking of Concurrent Software", editor = "Nicolas Halbwachs and Lenore D. Zuck", booktitle = "TACAS", series = "Lecture Notes in Computer Science", volume = "3440", publisher = "Springer", pages = "93--107", url = "http://dx.doi.org/10.1007/978-3-540-31980-1_7", ) @article(Seese91, author = "Detlef Seese", year = "1991", title = "The Structure of Models of Decidable Monadic Theories of Graphs", journal = "Ann. Pure Appl. Logic", volume = "53", number = "2", pages = "169--195", url = "http://dx.doi.org/10.1016/0168-0072(91)90054-P", ) @inproceedings(Wolper95, author = "Pierre Wolper and Bernard Boigelot", year = "1995", title = "An Automata-Theoretic Approach to Presburger Arithmetic Constraints (Extended Abstract)", editor = "Alan Mycroft", booktitle = "SAS", series = "Lecture Notes in Computer Science", volume = "983", publisher = "Springer", pages = "21--32", url = "http://dx.doi.org/10.1007/3-540-60360-3_30", )