Publications

2015

[1]	A Comparison of Mechanisms for Integrating Handwritten and Generated Code for Object-Oriented Programming Languages (Timo Greifenberg, Katrin Hölldobler, Carsten Kolassa, Markus Look, Pedram Mir Seyed Nazari, Klaus Müller, Antonio Navarro Pérez, Dimitri Plotnikov, Dirk Reiss, Alexander Roth, Bernhard Rumpe, Martin Schindler, Andreas Wortmann), In , SciTe Press, 2015. (Proceedings of the 3rd International Conference on Model-Driven Engineering and Software Development : Angers, France, 9 - 11 February 2015) [bibtex] [pdf] [doi]
[2]	Counterexamples for Expected Rewards (Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker), Chapter in FM 2015: Formal Methods, Springer International Publishing, 2015. [bibtex]
[3]	A greedy approach for the efficient repair of stochastic models (Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen), Chapter in NASA Formal Methods, Springer International Publishing, 2015. [bibtex]
[4]	A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata (Johanna Nellen, Erika Ábrahám, Benedikt Wolters), Chapter in Formalisms for Reuse and Systems Integration, Springer, 2015. [bibtex]
[5]	Understanding Probabilistic Programs (Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo), Chapter in Correct System Design, Springer International Publishing, 2015. [bibtex]
[6]	Conditioning in Probabilistic Programming (Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver, Federico Olmedo), In arXiv preprint arXiv:1504.00198, 2015. [bibtex]
[7]	Online Appointment Scheduling in the Random Order Model (Oliver Göbel, Thomas Kesselheim, Andreas Tönnis), In , 2015. [bibtex]
[8]	PROPhESY: A PRObabilistic ParamEter SYnthesis Tool (Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, Erika Ábrahám), Chapter in Computer Aided Verification, Springer International Publishing, 2015. [bibtex]
[9]	Unterstützung der Fahrplanfeinkonstruktion mit Optimierungsverfahren (Frédéric Weymann, Nils Nießen), In Eisenbahntechnische Rundschau, DVV Media Group, Eurailpress, volume 3, 2015. [bibtex] [pdf]
[10]	Verbesserung der Disposition des Eisenbahnbetriebs durch innovative Optimierungsverfahren (Frédéric Weymann, Nils Nießen), In ZEVrail : Zeitschrift für das gesamte System Bahn, Siemens, volume 139, 2015. (http://www.zevrail.de/artikel/verbesserung-der-disposition-des-eisenbahnbetriebs-durch-innovative-optimierungsverfahren) [bibtex] [pdf]
[11]	AProVE: Termination and Memory Safety of C Programs - (Competition Contribution) (Thomas Ströder, Cornelius Aschermann, Florian Frohn, Jera Hensel, Jürgen Giesl), Chapter in Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Christel Baier, Cesare Tinelli, eds.), Springer, volume 9035, 2015. [bibtex]
[12]	Verifying pointer programs using graph grammars (Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll), In Science of Computer Programming, volume , 2015. [bibtex] [pdf] [doi]
[13]	Equipment Interconnection Models in Discrete Manufacturing (Sten Grüner, Peter Weber, Constantin Wagner, Ulrich Epple), In IFAC-PapersOnLine, volume 48, 2015. () [bibtex] [pdf] [doi]
[14]	On the Hardness of Almost-Sure Termination (Benjamin Lucien Kaminski, Joost-Pieter Katoen), In CoRR, volume abs/1506.01930, 2015. [bibtex] [pdf]
[15]	Conditioning in Probabilistic Programming (Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver, Federico Olmedo), In CoRR, volume abs/1504.00198, 2015. [bibtex] [pdf]
[16]	Synthesizing structured reactive programs via deterministic tree automata (Benedikt Brütsch), In Information and Computation, volume 242, 2015. () [bibtex] [pdf] [doi]

[17]	A RESTful Extension of OPC UA (Sten Grüner, Julius Pfrommer, Florian Palm), In [Communication in Automation ; May 27-29, 2015, Palma de Mallorca, Spain / 11th IEEE World Conference on Factory Communication Systems], IEEE, 2015. ([Communication in Automation ; May 27-29, 2015, Palma de Mallorca, Spain / 11th IEEE World Conference on Factory Communication Systems]) [bibtex] [pdf] [doi]
[18]	Challenges in the Modelling and Operation of Physically Coupled Systems of Systems (Ulrich Epple, David Kampert), In MATHMOD 2015 : 8th Vienna Conference on Mathematical Modelling, February 18 - 20, 2015, Vienna University of Technology, Austria ; abstract volume / F. Breitenecker; A. Kugi; I. Troch, eds. [IFAC, International Federation of Automatic Control], ARGESIM, volume 44, 2015. (MATHMOD 2015 : 8th Vienna Conference on Mathematical Modelling, February 18 - 20, 2015, Vienna University of Technology, Austria ; abstract volume / F. Breitenecker; A. Kugi; I. Troch, eds. [IFAC, International Federation of Automatic Control]) [bibtex] [pdf]
[19]	A Framework for Simulation, Optimization and Information Management of Physically-Coupled Systems of Systems (David Kampert, Shaghayegh Nazari, Christian Sonntag, Ulrich Epple, Sebastian Engell), In [INCOM 2015 : 15th IFAC/IEEE/IFIP/IFORS Symposium on Information Control Problems in Manufacturing ; May 11-13, 2015, Ottawa, Canada], IFAK, 2015. ([INCOM 2015 : 15th IFAC/IEEE/IFIP/IFORS Symposium on Information Control Problems in Manufacturing ; May 11-13, 2015, Ottawa, Canada]) [bibtex] [pdf]
[20]	Automatic Test Case Generation for PLC Programs using Coverage Metrics (Hendrik Simon, Nico Friedrich, Sebastian Biallas, Stefan Hauck-Stattelmann, Bastian Schlich, Stefan Kowalewski), 2015. (To appear) [bibtex]
[21]	Automatische Testfallgenerierung für SPS-Programme mittels Zeilenüberdeckung (Sebastian Biallas, Hendrik Simon, Stefan Kowalewski, Stefan Hauck-Stattelmann, Bastian Schlich), 2015. (To appear) [bibtex]
[22]	Automatic Error Cause Localization of Faulty PLC Programs (Sebastian Biallas, Nico Friedrich, Hendrik Simon, Stefan Kowalewski), 2015. (To appear) [bibtex]

[23]	Inferring Lower Bounds for Runtime Complexity (Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, Thomas Ströder), Technical report, RWTH Aachen, 2015. [bibtex] [pdf]
[24]	Counterexamples in Probabilistic Verification (Nils Jansen), PhD thesis, RWTH Aachen University, 2015. [bibtex]
[25]	Classifications of Recognizable Infinitary Trace Languages and the Distributed Synthesis Problem (Namit Chaturvedi), Publikationsserver der RWTH Aachen University, 2015. (Prüfungsjahr: 2014. - Publikationsjahr: 2015; Aachen, Techn. Hochsch., Diss., 2014) [bibtex] [pdf]

2014

[26]	Analysis and Synthesis of Interactive Component and Connector Systems (Jan Ringert), Shaker, 2014. [bibtex]
[27]	open62541 : der offene OPC UA Stack (Florian Palm, Sten Grüner, Julius Pfrommer, Markus Graube, Leon Urbas), inIT/ifak, 2014. (KommA 2014 : 5. Jahreskolloquium Kommunikation in der Automation ; 18.11.2014, Lemgo) [bibtex] [pdf]
[28]	Queueing; 2. rev. and extended ed. (Nils Nießen), Eurailpress, 2014. (Railway timetabling $\&$ operations : analysis, modelling, optimisation, simulation, performance evaluation / ed. Ingo A. Hansen; Jörn Pachl. Authors Thomas Albrecht ...) [bibtex] [pdf]
[29]	Capacity of a railway network; 1. Aufl. (Christian Meirich), Pro Business, 2014. (Proceedings of the 8th Joint Workshop of the German Research Training Groups in Computer Science : Dagstuhl 2014, June 15 - 18, 2014 / A. Jentzsch ... (ed.). DFG, Deutsche Forschungsgemeinschaft) [bibtex] [pdf]
[30]	Generating Abstract Graph-Based Procedure Summaries for Pointer Programs (Christina Jansen, Thomas Noll), Springer, volume 8571, 2014. (Proc. 7th Int. Conf. on Graph Transformation (ICGT 2014)) [bibtex] [pdf]
[31]	Multidimensional Image Processing for Confocal Laser Scanning Fluorescence Microscopy - Qantitative Analysis of the Cytoskeleton (Gerlind Herberich), Sierke, Göttingen, 2014. ((Zugleich Dissertation RWTH Aachen 2014)) [bibtex]
[32]	A Model for Discrete Product Flows in Manufacturing Plants (Sten Grüner, Peter Weber, Ulrich Epple), IEEE, 2014. (ETFA 2014 : IEEE 19th International Conference on Emerging Technologies and Factory Automation) [bibtex] [pdf]
[33]	Rule-Based Engineering Using Declarative Graph Database Queries (Sten Grüner, Peter Weber, Ulrich Epple), IEEE, 2014. (Proceedings of IEEE 12th International Conference on Industrial Informatics (INDIN)) [bibtex] [pdf] [doi]

[34]	Minimal counterexamples for linear-time probabilistic verification (Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker), In Theoretical Computer Science, Elsevier, volume 549, 2014. [bibtex]
[35]	Counterexample Generation for Hybrid Automata (Johanna Nellen, Erika Ábrahám, Xin Chen, Pieter Collins), Chapter in Formal Techniques for Safety-Critical Systems, Springer, 2014. [bibtex]
[36]	Symbolic counterexample generation for large discrete-time Markov chains (Nils Jansen, Ralf Wimmer, Erika Abraham, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster), In Science of Computer Programming, Elsevier, volume 91, 2014. [bibtex]
[37]	Accelerating parametric probabilistic verification (Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker), Chapter in Quantitative Evaluation of Systems, Springer International Publishing, 2014. [bibtex]
[38]	Fast debugging of PRISM models (Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen), Chapter in Automated Technology for Verification and Analysis, Springer International Publishing, 2014. [bibtex]
[39]	Counterexample generation for discrete-time Markov models: An introductory survey (Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer), Chapter in Formal Methods for Executable Software Models, Springer International Publishing, 2014. [bibtex]
[40]	Eisenbahninfrastruktur ökonomisch planen (Nils Nießen, Bastian Kogel), In Zeitschrift für Verkehrswissenschaft, Verkehrs-Verl. Fischer, volume 85, 2014. [bibtex] [pdf]
[41]	Berücksichtigung des Zacken-Lücken-Problems bei der analytischen Kapaziätsermittlung (Nora Niebel, Nils Nießen), In Eisenbahntechnische Rundschau : ETR, DVV Media Group, Eurailpress, volume 63, 2014. [bibtex] [pdf]
[42]	Ergebnisdokumentation bahnbetrieblicher Untersuchungen (Christian Meirich, Nils Nießen, Thorsten Schaer), In Deine Bahn : DB, Bahn Fachverlag GmbH, volume 42, 2014. [bibtex] [pdf]
[43]	Operational versus weakest pre-expectation semantics for the probabilistic guarded command language (Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver), In Performance Evaluation, volume 73, 2014. (Special Issue on the 9th International Conference on Quantitative Evaluation of Systems) [bibtex] [pdf] [doi]
[44]	Zacken-Lücken-Problem in der Praxis (Ingolf Gast, Nora Niebel, Nils Nießen), In Deine Bahn : DB, Bahn Fachverlag GmbH, volume 42, 2014. [bibtex] [pdf]
[45]	Weak omega-Regular Trace Languages (Namit Chaturvedi, Marcus Gelderie), In CoRR, volume abs/1402.3199, 2014. [bibtex] [pdf]
[46]	Alternating Runtime and Size Complexity Analysis of Integer Programs (Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jürgen Giesl), Chapter in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014) (Erika Ábrahám, Klaus Havelund, eds.), Springer Berlin Heidelberg, volume 8413, 2014. [bibtex]
[47]	Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code (Sebastian Biallas, Stefan Kowalewski, Stefan Stattelmann, Bastian Schlich), In , IFAC, 2014. (Discrete Event Systems : [Proc. Proceedings of the 12th International Workshop on Discrete Event Systems, Cachan, France, 2014] / Conference Editor: Lesage, Jean-Jacques, Faure, Jean-Marc, Cury, Jose E. R., Lennartson, Bengt) [bibtex] [pdf] [doi]

[48]	A CEGAR approach for the reachability analysis of PLC-controlled chemical plants (J. Nellen, E. Abraham), In Information Reuse and Integration (IRI), 2014 IEEE 15th International Conference on, 2014. [bibtex] [doi]
[49]	Rule-based engineering using declarative graph database queries (S. Gruner, P. Weber, U. Epple), In Industrial Informatics (INDIN), 2014 12th IEEE International Conference on, 2014. [bibtex] [doi]
[50]	A model for discrete product flows in manufacturing plants (S. Gruner, P. Weber, U. Epple), In Emerging Technology and Factory Automation (ETFA), 2014 IEEE, 2014. [bibtex] [doi]
[51]	Toward a Structure Theory of Regular Infinitary Trace Languages (Namit Chaturvedi), In Automata, languages, and programming (ICALP 2014), PT II (J. Esparza, P. Fraigniaud, T. Husfeldt, E. Koutsoupias, eds.), Springer, volume 8573, 2014. (Automata, languages, and programming (ICALP 2014), PT II) [bibtex] [pdf]
[52]	Intelligente Automatisierungssysteme durch Integration von Modellen in Entwicklung und Laufzeitumgebung (David Kampert, Ulrich Epple), In Automation 2014 : 15. Branchentreff der Mess- und Automatisierungstechnik ; Kongresshaus Baden-Baden, 1. und 2. Juli 2014 / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik, VDI-Verl., 2014. (Buch + 1 CD-ROM) [bibtex]
[53]	Outside-In : Simplifying Systems by Integrating the Outside Perspective (David Kampert, Ulrich Epple), In 2014 11th International Multi-Conference on Systems, Signals & Devices (SSD 2014) : Castelldefels-Barcelona, Spain, 11 - 14 February 2014 ; [including 4 conferences] / [organized by Universitat Politècnica de Catalunya, BarcelonaTECH; IEEE ...], IEEE, 2014. [bibtex] [doi]
[54]	Applying Static Code Analysis on Industrial Controller Code (Stefan Stattelmann, Sebastian Biallas, Bastian Schlich, Stefan Kowalewski), In 19th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), IEEE, 2014. [bibtex]
[55]	Development and Execution of PLC Programs on Real-Time Capable Mobile Devices (Mathias Obster, Igor Kalkov, Stefan Kowalewski), In 19th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), IEEE, 2014. [bibtex] [pdf]
[56]	Primal Beats Dual on Online Packing LPs in the Random-order Model (Thomas Kesselheim, Andreas Tönnis, Klaus Radke, Berthold Vöcking), In Proceedings of the 46th Annual ACM Symposium on Theory of Computing, ACM Press, 2014. [bibtex] [pdf] [doi]
[57]	Synthesis of Deterministic Top-down Tree Transducers from Automatic Tree Relations (Christof Löding, Sarah Winter), In Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, September 10-12, 2014., 2014. [bibtex] [doi]
[58]	Synthesis of Component and Connector Models from Crosscutting Structural Views (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In Software Engineering, 2014. [bibtex]
[59]	Verifying component and connector models against crosscutting structural views (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In ICSE, 2014. [bibtex]
[60]	Online Independent Set Beyond the Worst-Case: Secretaries, Prophets, and Periods (Oliver Göbel, Martin Hoefer, Thomas Kesselheim, Thomas Schleiden, Berthold Vöcking), In Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, 2014. [bibtex] [pdf] [doi]
[61]	Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs (Christina Jansen, Florian Göbe, Thomas Noll), In Graph Transformation - 7th International Conference, ICGT 2014, Held as Part of STAF 2014, York, UK, July 22-24, 2014. Proceedings, 2014. [bibtex] [pdf] [doi]
[62]	ICE: A Robust Framework for Learning Invariants (Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider), In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, 2014. [bibtex] [pdf] [doi]
[63]	Networked Cooperative Platoon of Vehicles for Testing Methods and Verification Tools (Ibtissem Ben Makhlouf, Stefan Kowalewski), 2014. (PDF: http://cps-vo.org/node/12115) [bibtex]

[64]	Regelbasiertes Engineering mit Graphabfragen (Sten Grüner, Ulrich Epple), In Dagstuhl-Workshop MBEES : Modellbasierte Entwicklung eingebetteter Systeme X, Schloss Dagstuhl, Germany, März 05-07, 2014, fortiss GmbH, 2014. [bibtex] [pdf]
[65]	International Workshop on Comparision and Versioning of Software Models (CVSM 2014) (Pit Pietsch, Udo Kelter, Jan Oliver Ringert), In Software Engineering, 2014. [bibtex]
[66]	Reducing Deadlock and Livelock Freedom to Termination (Byron Cook, Stephen Magill, Matthew Parkinson, Thomas Ströder), In Proceedings of the 14th International Workshop on Termination (WST 2014) (Carsten Fuhs, ed.), 2014. [bibtex]

[67]	Simplification Problems for Games and Automata (Stefan Repke), PhD thesis, RWTH Aachen University, 2014. [bibtex]
[68]	Languages of Infinite Traces and Deterministic Asynchronous Automata (Namit Chaturvedi), Technical report, RWTH Aachen, 2014. [bibtex] [pdf]
[69]	Simplification problems for automata and games (Stefan Repke), Publikationsserver der RWTH Aachen University, 2014. (Zsfassung in dt. und engl. Sprache; Aachen, Techn. Hochsch., Diss., 2014) [bibtex] [pdf]
[70]	Applications of automata learning in verification and synthesis (Daniel Neider), Publikationsserver der RWTH Aachen University, 2014. (Aachen, Techn. Hochsch., Diss., 2014) [bibtex] [pdf]
[71]	Strategy machines : representation and complexity of strategies in infinite games (Marcus Gelderie), PhD thesis, , 2014. (Aachen, Techn. Hochsch., Diss., 2014) [bibtex] [pdf]
[72]	Synthesis of state space generators for model checking microcontroller code (Dominique Gückel), Fachgruppe Informatik, RWTH Aachen University, volume 2014,15, 2014. (Druck-Ausgabe: 2014. - Online-Ausgabe: 2015. Auch veröffentlicht auf dem Publikationsserver der RWTH Aachen University.; Aachen, Techn. Hochsch., Diss., 2014) [bibtex] [pdf]

2013

[73]	Regular model checking using solver technologies and automata learning (Daniel Neider, Nils Jansen), Chapter in NASA Formal Methods, Springer Berlin Heidelberg, 2013. [bibtex]
[74]	A symbiosis of interval constraint propagation and cylindrical algebraic decomposition (Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker), Chapter in Automated Deduction--CADE-24, Springer Berlin Heidelberg, 2013. [bibtex]
[75]	Symbolic Methods in Testing (Dagstuhl Seminar 13021) (Thierry Jéron, Margus Veanes, Burkhart Wolff), In Dagstuhl Reports, volume 3, 2013. [bibtex] [pdf] [doi]
[76]	Connectivity games over dynamic networks (Sten Grüner, Frank G. Radmacher, Wolfgang Thomas), In Theoretical computer science, Elsevier [u.a.], volume 493, 2013. (Druck-Ausgabe: 2013. - Online-First: 2012. - Online-Ausgabe: 2013) [bibtex] [pdf] [doi]
[77]	Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs (Lars Noschinski, Fabian Emmes, Jürgen Giesl), In Journal of Automated Reasoning, Springer Netherlands, volume 51, 2013. [bibtex]
[78]	Bericht und Beiträge vom internationalen Workshop it Comparison and Versioning of Software Models (CVSM 2013) vom 27. Februar 2013 (anläßlich der Multikonferenz Software Engineering (SE 2013), 26. Februar - 1. März 2013 in Aachen) (Udo Kelter, Pit Pietsch, Jan Oliver Ringert), In Softwaretechnik-Trends, volume 33, 2013. [bibtex]
[79]	Learning Universally Quantified Invariants of Linear Data Structures (Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider), In CoRR, volume abs/1302.2273, 2013. [bibtex] [pdf]
[80]	Abstract interpretation of microcontroller code: Intervals meet congruences (Jörg Brauer, Andy King, Stefan Kowalewski), In Science of Computer Programming. Methods of Software Design: Techniques and Applications, Elsevier, volume 78, issue 7, 2013. [bibtex]
[81]	On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers (Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám), Chapter in Algebraic Informatics (Traian Muntean, Dimitrios Poulakis, Robert Rolland, eds.), Springer Berlin Heidelberg, volume 8080, 2013. [bibtex] [pdf] [doi]

[82]	Incremental Construction of Greibach Normal Form (M. Bals, C. Jansen, T. Noll), In Theoretical Aspects of Software Engineering (TASE), 2013 International Symposium on, 2013. [bibtex] [doi]
[83]	High-level Counterexamples for Probabilistic Automata (Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Bernd Becker), In 10th International Conference on Quantitative Evaluation of Systems (QEST’13), 2013. [bibtex]
[84]	A Service Interface for Exchange of Property Information (David Kampert, Ulrich Epple), In IECON 2013 : 39th annual conference of the IEEE Industrial Electronics Society ; Vienna, Austria, 10 - 13 November 2013 / [sponsored by the Institute of Electrical and Electronics Engineers (IEEE); IEEE Industrial Electronics Society (IES)], IEEE, 2013. [bibtex] [doi]
[85]	An Engineerable Procedure Description Method for Industrial Automation (Liyong Yu, Sten Grüner, Ulrich Epple), In Proceedings of 2013 IEEE 18th International Conference on Emerging Technologies & Factory Automation : ETFA 2013 ; September, 10-13, 2013, Cagliari, Italy, IEEE, 2013. [bibtex] [doi]
[86]	Paradigms for Unified Runtime Systems in Industrial Automation (Sten Grüner, Ulrich Epple), In Proceedings of the 12th European Control Conference (ECC) : July 17 -19, 2013, Zuerich, Switzerland, 2013. [bibtex]
[87]	Dienste für den operativen Zugriff auf Merkmalinformation in der Automatisierung - Spezifikation - Integration - Anwendung (David Kampert, Ulrich Epple), In Automation 2013 : 14. Branchentreff der Mess- und Automatisierungstechnik ; Kongresshaus Baden-Baden, 25. und 26. Juni 2013 / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik, VDI-Verl., 2013. (Datentraeger: 1 CD-ROM) [bibtex]
[88]	Konzeption eines ebenenübergreifenden Laufzeitsystems für die Automation (Sten Grüner, Ulrich Epple), In Automation 2013 : 14. Branchentreff der Mess- und Automatisierungstechnik ; Kongresshaus Baden-Baden, 25. und 26. Juni 2013 / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik, VDI-Verl., 2013. (Datentraeger: 1 CD-ROM) [bibtex]
[89]	Strategy Composition in Compositional Games (Marcus Gelderie), In Automata, Languages and Programming (Fedor V. Fomin, Rusins Freivalds, Marta Kwiatkowska, David Peleg, eds.), 2013. [bibtex] [pdf]
[90]	Decidability Results on the Existence of Lookahead Delegators for NFA (Christof Löding, Stefan Repke), In Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS , 2013. [bibtex] [doi]
[91]	Engineering Delta Modeling Languages (Arne Haber, Katrin Hölldobler, Carsten Kolassa, Markus Look, Bernhard Rumpe, Klaus Müller, Ina Schaefer), In Proceedings of the 17th International Software Product Line Conference, ACM Press, 2013. [bibtex] [pdf] [doi]
[92]	Synthesis of component and connector models from crosscutting structural views (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In ESEC/SIGSOFT FSE, 2013. [bibtex]
[93]	High-Level Counterexamples for Probabilistic Automata (Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker), In Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, 2013. [bibtex] [pdf] [doi]
[94]	Regular Model Checking Using Solver Technologies and Automata Learning (Daniel Neider, Nils Jansen), In NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings, 2013. [bibtex] [pdf] [doi]
[95]	A Case Study on Model-Based Development of Robotic Systems using MontiArc with Embedded Automata (Jan Oliver Ringert, Bernhard Rumpe, Andreas Wortmann), In MBEES (Holger Giese, Michaela Huhn, Jan Phillips, Bernhard Schätz, eds.), fortiss GmbH, München, 2013. [bibtex]
[96]	Learning Universally Quantified Invariants of Linear Data Structures (Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider), In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, 2013. [bibtex] [pdf] [doi]
[97]	Verifikation von sicherheitsgerichteten SPS-Programmen mit Hilfe von Safety-Automaten (Sebastian Biallas, Volker Kamin, Stefan Kowalewski, Bastian Schlich, Stephan Sehestedt, Stefan Stattelmann), In Automation 2013 (VDI Wissensforum, ed.), VDI-Verlag, 2013. (Langfassung auf CD-ROM) [bibtex]
[98]	Comparison of Reachability Methods for Uncertain Linear Time-Invariant Systems (Ibtissem Ben Makhlouf, Paul Haensch, Stefan Kowalewski), In ECC13: European Control Conference , Zurich, Switzerland July 17-19,, EUCA, 2013. [bibtex]
[99]	Reachability Analysis for Managing Platoons at Intersections (Ibtissem Ben Makhlouf, Hilal Diab, Stefan Kowalewski), In 21st Mediterranean Conference on Control & Automation (MED) Platanias-Chania, Crete, Greece, June 25-28,, IEEE, 2013. [bibtex]
[100]	Boolean and Modular Abstractions for Programmable Logic Controllers (Sebastian Biallas, Dimitri Bohlender, Stefan Kowalewski), In Dependable Control of Discrete Systems (DCDS'13), IEEE, 2013. [bibtex]

[101]	Synthesizing Structured Reactive Programs via Deterministic Tree Automata (Benedikt Brütsch), In Proceedings 1st International Workshop on Strategic Reasoning (Fabio Mogavero, Aniello Murano, Moshe Y. Vardi, eds.), Open Publishing Association, volume 112, 2013. [bibtex] [doi]
[102]	From Software Architecture Structure and Behavior Modeling to Implementations of Cyber-Physical Systems (Jan Oliver Ringert, Bernhard Rumpe, Andreas Wortmann), In Software Engineering (Workshops) (Stefan Wagner, Horst Lichter, eds.), GI, volume 215, 2013. [bibtex]
[103]	International Workshop on Comparison and Versioning of Software Models (CVSM 2013) (Pit Pietsch, Udo Kelter, Jan Oliver Ringert), In Software Engineering (Stefan Kowalewski, Bernhard Rumpe, eds.), GI, volume 213, 2013. [bibtex]
[104]	Analyzing Runtime and Size Complexity of Integer Programs (Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jürgen Giesl), In Proceedings of the 13th International Workshop on Termination (WST 2013) (Johannes Waldmann, ed.), 2013. [bibtex]
[105]	Predicate Abstraction for Programmable Logic Controllers (Sebastian Biallas, Mirco Giacobbe, Stefan Kowalewski), In 18th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2013) (Charles Pecheur, Michael Dierkes, eds.), Springer Berlin Heidelberg, volume 8187, 2013. [bibtex] [pdf]

[106]	Algorithms for online buffering problems and applications to the power control of a hybrid electric vehicle (Melanie Winkler), PhD thesis, , 2013. (Zsfassung in engl. und dt. Sprache. - Prüfungsjahr: 2013. - Publikationsjahr: 2014; Aachen, Techn. Hochsch., Diss., 2013) [bibtex] [pdf]
[107]	Network design for railway infrastructure by means of linear programming (Jacob Spönemann), Publikationsserver der RWTH Aachen University, 2013. (Aachen, Techn. Hochsch., Diss., 2013) [bibtex] [pdf]
[108]	Graph Complexity Measures and Monotonicity (Roman Rabinovich), PhD thesis, RWTH Aachen University, 2013. [bibtex] [pdf]
[109]	Synthesis of winning strategies for interaction under partial information (Bernd Puchala), Publikationsserver der RWTH Aachen University, 2013. (Aachen, Techn. Hochsch., Diss., 2013) [bibtex] [pdf]
[110]	A study of pushdown games (Wladimir Fridman), Publikationsserver der RWTH Aachen University, 2013. (Zsfassung in dt. und engl. Sprache; Aachen, Techn. Hochsch., Diss., 2013) [bibtex] [pdf]
[111]	The Quantitative mu-Calculus (Diana Fischer), PhD thesis, RWTH Aachen University, 2013. [bibtex] [pdf]
[112]	Automatic abstraction for bit vectors using decision procedures (Jörg Brauer), Fachgruppe Informatik, RWTH Aachen University, volume 2013,14, 2013. (Zugl.: Aachen, Techn. Hochsch., Diss., 2013) [bibtex] [pdf]

2012

[113]

Hybrid Sequential Function Charts (Johanna Nellen, Erika Ábrahám), Kovač, volume 68, 2012. (Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen : MBMV 2012 ; [15. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen ... im März 2012 an der Technischen Universität Kaiserslautern] / Jens Brandt ... (Hrsg.)) [bibtex] [pdf]

[114]	Languages vs. $ømega$-Languages in Regular Infinite Games (N. Chaturvedi, J. Olschewski, W. Thomas), In International Journal of Foundations of Computer Science, volume 23, 2012. (Journal version of \citecot11. \copyright 2012 http://www.worldscinet.com/ijfcs/World Scientific Publishing Company) [bibtex] [pdf]
[115]	Abstract Interpretation of Microcontroller Code: Intervals meet Congruences (Jörg Brauer, Andy King, Stefan Kowalewski), In Science of Computer Programming, Elsevier, volume 77, 2012. (To appear) [bibtex] [pdf] [doi]
[116]	A Framework for Decentralized Access Control Using Finite State Automata (N. Chaturvedi, B. Meenakshi, A. Datta Chowdhury), Chapter in Modern Applications of Automata Theory (Deepak D'Souza, Priti Shankar, eds.), World Scientific, volume 2, 2012. [bibtex] [pdf]
[117]	The COMICS tool--Computing minimal counterexamples for DTMCs (Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker), Chapter in Automated Technology for Verification and Analysis, Springer Berlin Heidelberg, 2012. [bibtex]
[118]	Kernmodelle für die Systembeschreibung - Ein Konzept zur Vereinfachung (David Kampert, Ulrich Epple), In Atp-Edition : automatisierungstechnische Praxis, Oldenbourg Industrieverl., volume 54, 2012. [bibtex] [pdf]
[119]	Model-Based Management of Asset Information (David Kampert, Ulrich Epple, Martin Mertens), In Softwaretechnik-Trends, GI - Gesellschaft für Informatik, volume 32, 2012. [bibtex] [pdf]
[120]	SMT-RAT: An SMT-compliant nonlinear real arithmetic toolbox (Florian Corzilius, Ulrich Loup, Sebastian Junges, Erika Ábrahám), Chapter in Theory and Applications of Satisfiability Testing--SAT 2012, Springer Berlin Heidelberg, 2012. [bibtex]
[121]	Automated Runtime Complexity Analysis for Prolog by Term Rewriting (Thomas Ströder, Fabian Emmes, Peter Schneider-Kamp, Jürgen Giesl), Chapter in Proceedings of the 12th International Workshop on Termination (Georg Moser, ed.), University of Innsbruck, 2012. [bibtex]
[122]	A linear operational semantics for termination and complexity analysis of ISO prolog (Thomas Ströder, Fabian Emmes, Peter Schneider-Kamp, Jürgen Giesl, Carsten Fuhs), Chapter in Proceedings of the 21st International Conference on Logic-Based Program Synthesis and Transformation (Germán Vidal, ed.), Springer-Verlag, volume 7225, 2012. [bibtex]
[123]	Basics on Tree Automata (C. Löding), Chapter in Modern Applications of Automata Theory (Deepak D'Souza, Priti Shankar, eds.), World Scientific, 2012. [bibtex]
[124]	Efficient Inclusion Testing for Simple Classes of Unambiguous $ømega$-Automata (Dimitri Isaak, Christof Löding), In Information Processing Letters, Elsevier Science Publishers, volume 112, 2012. [bibtex] [pdf]
[125]	Proving non-looping non-termination automatically (Fabian Emmes, Tim Enger, Jürgen Giesl), Chapter in Proceedings of the 6th International Joint Conference on Automated Reasoning (Bernhard Gramlich, Dale Miller, Uli Sattler, eds.), Springer-Verlag, volume 7364, 2012. [bibtex]
[126]	An Interim Summary on Semantic Model Differencing (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In Softwaretechnik-Trends, volume 32, 2012. [bibtex]
[127]	Proving Non-Termination for Java Bytecode (Marc Brockschmidt, Thomas Ströder, Carsten Otto, Jürgen Giesl), Chapter in Proceedings of the 12th International Workshop on Termination (Georg Moser, ed.), University of Innsbruck, 2012. [bibtex]
[128]	Automated detection of non-termination and NullPointerExceptions for Java Bytecode (Marc Brockschmidt, Thomas Ströder, Carsten Otto, Jürgen Giesl), Chapter in Proceedings of the 2011 International Conference on Formal Verification of Object-Oriented Software (Bernhard Beckert, Ferruccio Damiani, Dilian Gurov, eds.), Springer-Verlag, volume 7421, 2012. [bibtex]
[129]	Solving Counter Parity Games (Dietmar Berwanger, Łukasz Kaiser, Simon Leßenich), Chapter in Mathematical Foundations of Computer Science 2012 (Branislav Rovan, Vladimiro Sassone, Peter Widmayer, eds.), Springer Berlin Heidelberg, volume 7464, 2012. [bibtex] [pdf] [doi]
[130]	Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme (Sebastian Biallas, Stefan Kowalewski, Bastian Schlich), In Automatisierungstechnische Praxis (atp EDITION), 54. Jahrgang, 7-8/2012, Oldenbourg Industrieverlag, 2012. [bibtex]

[131]	Regularity Problems for Weak Pushdown $ømega$-Automata and Games (Christof Löding, Stefan Repke), In Mathematical Foundations of Computer Science 2012 (Branislav Rovan, Vladimiro Sassone, Peter Widmayer, eds.), Springer Berlin / Heidelberg, volume 7464, 2012abstract=We show that the regularity and equivalence problems are decidable for deterministic weak pushdown $ømega$-automata, giving a partial answer to a question raised by Cohen and Gold in 1978. We prove the decidability by a reduction to the corresponding problems for determinis- tic pushdown automata on finite words. Furthermore, we consider the problem of deciding for pushdown games whether a winning strategy exists that can be implemented by a finite automaton. We show that this problem is already undecidable for games defined by one-counter automata or visibly pushdown automata with a safety condition.. (10.1007/978-3-642-32589-2_66) [bibtex] [pdf]
[132]	Operational Versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language (F. Gretz, J. Katoen, A McIver), In Quantitative Evaluation of Systems (QEST), 2012 Ninth International Conference on, 2012. [bibtex] [doi]
[133]	Symbolic Counterexample Generation for Discrete-Time Markov Chains. (Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker), In FACS, 2012. [bibtex]
[134]	Modeling Asset Information for Interoperable Software Systems (David Kampert, Ulrich Epple), In INDIN 2012: IEEE 10th International Conference on Industrial Informatics : 25 Jul - 27 Jul 2012, Beijing, China, IEEE, 2012. [bibtex]
[135]	Algorithmische Analyse von Sensornetzwerktopolgien (Sten Grüner, Ulrich Epple), In Automation 2012 : der 13. Branchentreff der Mess- und Automatisierungstechnik / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik, VDI-Verl., 2012. (CD-ROM) [bibtex]
[136]	SFC-based Process Description for Complex Automation Functionalities (Liyong Yu, Gustavo Quirós, Sten Grüner, Ulrich Epple), In EKA 2012 : Entwurf komplexer Automatisierungssysteme ; Beschreibungsmittel, Methoden,Werkzeuge und Anwendungen ; 12. Fachtagung mit Tutorium ; 08. Mai Tutorium 09. bis 10. Mai 2012 Fachtagung, Magdeburg, Denkfabrik im Wissenschaftshafen / Institut für Automation und Kommunikation e.V. Magdeburg, Ulrich Jumar, ifak, 2012. [bibtex]
[137]	Strategy Machines and Their Complexity (with addendum) (Marcus Gelderie), In Mathematical Foundations of Computer Science 2012 (Branislav Rovan, Vladimiro Sassone, Peter Widmayer, eds.), Springer Berlin / Heidelberg, volume 7464, 2012. (10.1007/978-3-642-32589-2_39) [bibtex] [pdf]
[138]	Invariants for LTI Systems with Uncertain Input (Paul Hänsch, Stefan Kowalewski), In Reachability Problems, Springer, 2012. [bibtex]
[139]	Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs (Jürgen Giesl, Thomas Ströder, Peter Schneider-Kamp, Fabian Emmes, Carsten Fuhs), In Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming, ACM Press, 2012. [bibtex]
[140]	Playing Pushdown Parity Games in a Hurry (Wladimir Fridman, Martin Zimmermann), In GandALF, 2012. [bibtex]
[141]	Down the Borel Hierarchy: Solving Muller Games via Safety Games (Daniel Neider, Roman Rabinovich, Martin Zimmermann), In Proceedings Third International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2012, Napoli, Italy, September 6-8, 2012., 2012. [bibtex] [pdf] [doi]
[142]	Learning Minimal Deterministic Automata from Inexperienced Teachers (Martin Leucker, Daniel Neider), In Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2012), Springer, volume 7609, 2012. [bibtex]
[143]	Computing Minimal Separating DFAs and Regular Invariants Using SAT and SMT Solvers (Daniel Neider), In Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis (ATVA 2012), Springer, volume 7561, 2012. [bibtex]
[144]	Inferring Definite Counterexamples Through Under-Approximation (Jörg Brauer, Axel Simon), In NASA Formal Methods, Springer, volume 7226, 2012. [bibtex] [pdf]
[145]	Automatische Wertebereichsanalyse von SPS-Programmen (Sebastian Biallas, Stefan Kowalewski, Bastian Schlich), In AUTOMATION 2012, Baden-Baden, Germany, VDI-Verlag, 2012. (Long version (12 pages) on CD-ROM) [bibtex]
[146]	Safety Verification of a Controlled Cooperative Platoon Under Loss of Communication Using Zonotopes (Ibtissem Ben Makhlouf, Hilal Diab, Stefan Kowalewski), In ADHS 2012, Eindhoven, NL, Inproceeding of the 4th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 12), 2012. [bibtex] [pdf]
[147]	Loop Leaping with Closures (Sebastian Biallas, Jörg Brauer, Andy King, Stefan Kowalewski), In 19th Static Analysis Symposium (Antoine Miné, David Schmidt, eds.), Springer Berlin Heidelberg, 2012. [bibtex]
[148]	Static Analysis of Lockless Microcontroller C Programs (Eva Beckschulze, Sebastian Biallas, Stefan Kowalewski), In Proceedings Seventh Conference on Systems Software Verification (SSV 2012), EPTCS, 2012. [bibtex] [pdf]
[149]	Arcade.PLC: A Verification Platform for Programmable Logic Controllers (Sebastian Biallas, Jörg Brauer, Stefan Kowalewski), In Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, ACM Press, 2012. [bibtex] [pdf]

[150]	A Counting Logic for Structure Transition Systems (Lukasz Kaiser, Simon Leßenich), In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (Patrick Cégielski, Arnaud Durand, eds.), Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, volume 16, 2012. [bibtex] [pdf] [doi]
[151]	A Model-Based Implementation of Function Block Diagram (Sten Grüner, David Kampert, Ulrich Epple), In Tagungsband / Dagstuhl-Workshop MBEES (MBEES 2012) : modellbasierte Entwicklung eingebetteter Systeme VIII ; model-based development of embedded systems ; 6.02.2012 - 8.02.2012 / Holger Giese ..., fortiss, 2012. [bibtex]
[152]	Banach-Mazur Games with Simple Winning Strategies (Erich Grädel, Simon Leßenich), In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (Patrick Cégielski, Arnaud Durand, eds.), Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, volume 16, 2012. [bibtex] [pdf] [doi]
[153]	Reachability Analysis of Linear Systems with Stepwise Constant Inputs (Paul Hänsch, Hilal Diab, Ibtissem Ben Makhlouf, Stefan Kowalewski), In 1st ETAPS Workshop on "Hybrid Autonomous Systems" (HAS 2011), Elsevier, 2012. (To appear) [bibtex]
[154]	Range and Value-Set Analysis for Programmable Logic Controllers (Sebastian Biallas, Stefan Kowalewski, Bastian Schlich), In Proceedings of the 11th International Workshop on Discrete Event Systems, IFAC, 2012. [bibtex] [pdf]
[155]	Adaptable Value-Set Analysis for Low-Level Code (Jörg Brauer, Rene Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, Mads Chr. Olesen), In 6th International Workshop on Systems Software Verification (SSV 2011), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. [bibtex] [pdf]

[156]	Automated Complexity Analysis for \textsfProlog by Term Rewriting (Thomas Ströder, Fabian Emmes, Jürgen Giesl, Peter Schneider-Kamp, Carsten Fuhs), Technical report, RWTH Aachen, 2012. [bibtex] [pdf]
[157]	Minimal counterexamples for refuting $ømega$-regular properties of Markov decision processes. Reports of SFB (Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker), Technical report, TR 14 AVACS 88, 2012. [bibtex]
[158]	Infinite regular games in the higher-order pushdown and the parametrized setting (Michaela Slaats), PhD thesis, RWTH Aachen, 2012. [bibtex] [pdf]
[159]	Strategy Machines and their Complexity (with addendum) (M. Gelderie), Technical report, RWTH-Aachen, 2012. [bibtex]
[160]	Verwaltung und Verarbeitung merkmalbasierter Informationen: vom Metamodell zur technologischen Realisierung; Als Ms. gedr. (Martin Mertens), Publikationsserver der RWTH Aachen University, volume 1207, 2012. (Druckausg.: Mertens, Martin: Verwaltung und Verarbeitung merkmalbasierter Informationen: vom Metamodell zur technologischen Realisierung; Zugl.: Aachen, Techn. Hochsch., Diss., 2011) [bibtex] [pdf]
[161]	Verification of continuous space stochastic systems (Alexandru Mereacre), Publikationsserver der RWTH Aachen University, 2012. (Zsfassung in engl. und dt. Sprache; Aachen, Techn. Hochsch., Diss., 2012) [bibtex] [pdf]

2011

[162]	Automated termination proofs for haskell by term rewriting (Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, René Thiemann), In ACM Transactions on Programming Languages and Systems, ACM Press, volume 33, 2011. [bibtex]
[163]	I-RiSC: an SMT-compliant solver for the existential fragment of real algebra (Ulrich Loup, Erika Ábrahám), Chapter in Algebraic Informatics, Springer Berlin Heidelberg, 2011. [bibtex]
[164]	GiNaCRA: A C++ library for real algebraic computations (Ulrich Loup, Erika Ábrahám), Chapter in NASA Formal Methods, Springer Berlin Heidelberg, 2011. [bibtex]
[165]	Hierarchical counterexamples for discrete-time Markov chains (Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker), Chapter in Automated Technology for Verification and Analysis, Springer Berlin Heidelberg, 2011. [bibtex]
[166]	Counterexample generation for Markov chains using SMT-based bounded model checking (Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám), Chapter in Formal Techniques for Distributed Systems, Springer Berlin Heidelberg, 2011. [bibtex]
[167]	Dependency triples for improving termination analysis of logic programs with cut (Thomas Ströder, Peter Schneider-Kamp, Jürgen Giesl), Chapter in Proceedings of the 20th International Conference on Logic-based Program Synthesis and Transformation (María Alpuente, ed.), Springer-Verlag, volume 6564, 2011. [bibtex]
[168]	Application of Static Analyses for State Space Reduction to Microcontroller Binary Code (Bastian Schlich, Jörg Brauer, Stefan Kowalewski), In Sci. Comput. Program., volume 76, 2011. [bibtex] [pdf]
[169]	A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems (Lars Noschinski, Fabian Emmes, Jürgen Giesl), Chapter in Proceedings of the 23rd International Conference on Automated Deduction (Nikolaj Bjørner, Viorica Sofronie-Stokkermans, eds.), Springer-Verlag, volume 6803, 2011. [bibtex]
[170]	Infinite games and automata theory (C. Löding), Chapter in Lectures in Game Theory for Computer Scientists (Krzysztof R. Apt, Erich Grädel, eds.), Cambridge University Press, 2011. [bibtex]
[171]	Proving Termination by Dependency Pairs and Inductive Theorem Proving (Carsten Fuhs, Jürgen Giesl, Michael Parting, Peter Schneider-Kamp, Stephan Swiderski), In Journal of Automated Reasoning, Springer Netherlands, volume 47, 2011. [bibtex]
[172]	A Little Synopsis on Streams, Stream Processing Functions, and State-Based Stream Processing (Jan Oliver Ringert, Bernhard Rumpe), In Int. J. Software and Informatics, volume 5, 2011. [bibtex]
[173]	On-The-Fly Path Reduction (Sebastian Biallas, Jörg Brauer, Dominique Gückel, Stefan Kowalewski), In Electronic Notes in Theoretical Computer Science, Elsevier, volume 274C, 2011. (4th International Workshop on Harnessing Theories for Tool Support in Software (TTSS 2010)) [bibtex] [pdf]

[174]	Infinite Games and Uniformization (W. Thomas), In Proceedings of the 4th Indian Conference on Logic and Its Applications, ICLA 2011 (M. Banerjee, A. Seth, eds.), Springer, volume 6521, 2011. [bibtex]
[175]	Connectivity Games over Dynamic Networks (Sten Grüner, Frank G. Radmacher, Wolfgang Thomas), In GandALF 2011 : Proceedings of Second International Symposium on Games, Automata, Logics and Formal Verification ; Minori, Italy, 15-17th June 2011 / Edited by: Giovanna D'Agostino ..., NICTA, 2011. [bibtex] [pdf] [doi]
[176]	Classifying Regular Languages via Cascade Products of Automata (Marcus Gelderie), In Language and Automata Theory and Applications (Adrian-Horia Dediu, Shunsuke Inenaga, Carlos Martín-Vide, eds.), Springer Berlin / Heidelberg, volume 6638, 2011. (The original publication is available at www.springerlink.com) [bibtex] [pdf]
[177]	A Local Greibach Normal Form for Hyperedge Replacement Grammars. (Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll), In LATA (Adrian Horia Dediu, Shunsuke Inenaga, Carlos Martín-Vide, eds.), Springer, volume 6638, 2011. [bibtex] [pdf]
[178]	SMT-based Counterexample Generation for Markov Chains. (Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abrahám), In MBMV, 2011. [bibtex]
[179]	On collaboratively conveying computer science to pupils (Erika Ábrahám, Nadine Bergner, Philipp Brauner, Florian Corzilius, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Johanna Nellen, Ulrik Schroeder), In Proceedings of the 11th Koli Calling International Conference on Computing Education Research, 2011. [bibtex]
[180]	Hardware Support for Efficient Testing of Embedded Software (Thomas Reinbacher, Andreas Steininger, Tobias Müller, Martin Horauer, Jörg Brauer, Stefan Kowalewski), In 7th ASME/IEEE Conference on Mechatronics and Embedded Systems and Applications (MESA 2011), ASME, 2011. [bibtex]
[181]	Testing Microcontroller Software Simulators (Thomas Reinbacher, Dominique Gückel, Martin Horauer, Stefan Kowalewski), In Informatik 2011, Gesellschaft für Informatik, 2011. [bibtex] [pdf]
[182]	Automated Test-Trace Inspection for Microcontroller Binary Code (Thomas Reinbacher, Jörg Brauer, Daniel Schachinger, Andreas Steininger, Stefan Kowalewski), In RV, Springer, 2011. [bibtex] [pdf]
[183]	Precise Control Flow Reconstruction Using Boolean Logic (Thomas Reinbacher, Jörg Brauer), In International Conference on Embedded Software (EMSOFT 2011) (Samarjit Chakraborty, Ahmed Jerraya, Sanjoy K. Baruah, Sebastian Fischmeister, eds.), ACM Press, 2011. [bibtex] [pdf]
[184]	Safety Verification of a Cooperative Vehicle Platoon with Uncertain Inputs Using Zonotopes (Ibtissem Ben Makhlouf, Jan Philipp Maschuw, Paul Hänsch, Hilal Diab, Stefan Kowalewski, Dirk Abel), In 18th IFAC World Congress, 2011, Milano, Italy, IFAC, 2011. [bibtex]
[185]	Distributed Synthesis for Regular and Contextfree Specifications (W. Fridman, B. Puchala), In Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science, MFCS 2011, Springer, 2011. [bibtex]
[186]	ADDiff: semantic differencing for activity diagrams (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In SIGSOFT FSE (Tibor Gyimóthy, Andreas Zeller, eds.), ACM Press, 2011. [bibtex]
[187]	CD2Alloy: Class Diagrams Analysis Using Alloy Revisited (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In MoDELS (Jon Whittle, Tony Clark, Thomas Kühne, eds.), Springer, volume 6981, 2011. [bibtex]
[188]	Semantically Configurable Consistency Analysis for Class and Object Diagrams (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In MoDELS (Jon Whittle, Tony Clark, Thomas Kühne, eds.), Springer, volume 6981, 2011. [bibtex]
[189]	Juggrnaut - An Abstract JVM (Jonathan Heinen, Henrik Barthels, Christina Jansen), In Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2011, Turin, Italy, October 5-7, 2011, Revised Selected Papers, 2011. [bibtex] [pdf] [doi]
[190]	Modal Object Diagrams (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In ECOOP, 2011. [bibtex]
[191]	CDDiff: Semantic Differencing for Class Diagrams (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In ECOOP, 2011. [bibtex]
[192]	Small Strategies for Safety Games (Daniel Neider), In Proceedings of the 9th Symposium on Automated Technology for Verification and Analysis (ATVA 2011), Springer, volume 6996, 2011. [bibtex]
[193]	Languages vs. $ømega$-Languages in Regular Infinite Games (N. Chaturvedi, J. Olschewski, W. Thomas), In Proceedings of the 15th International Conference on Developments in Language Theory, DLT 2011 (Giancarlo Mauri, Alberto Leporati, eds.), Springer, volume 6795, 2011. [bibtex] [pdf]
[194]	Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse (Sebastian Biallas, Stefan Kowalewski, Bastian Schlich), In AUTOMATION 2011, Baden-Baden, Germany, VDI-Verlag, 2011. [bibtex]
[195]	Existential Quantification as Incremental SAT (Jörg Brauer, Andy King, Jael Kriener), In Computer Aided Verification (CAV 2011) (Ganesh Gopalakrishnan, Shaz Qadeer, eds.), Springer, volume 6806, 2011. [bibtex] [pdf]
[196]	Approximate Quantifier Elimination for Propositional Boolean Formulae (Jörg Brauer, Andy King), In NASA Formal Methods Symposium (NFM 2011), Springer, volume 6617, 2011. [bibtex] [pdf]
[197]	Transfer Function Synthesis without Quantifier Elimination (Jörg Brauer, Andy King), In European Symposium on Programming (ESOP 2011), Springer, volume 6602, 2011. [bibtex] [pdf]
[198]	Automatically Deriving Symbolic Invariants for PLC Programs Written in IL (Sebastian Biallas, Jörg Brauer, Stefan Kowalewski, Bastian Schlich), In FORMS/FORMAT 2010 (Eckehard Schnieder, Geza Tarnai, eds.), Springer Berlin Heidelberg, 2011. [bibtex] [pdf]
[199]	SAT-Based Abstraction Refinement for Programmable Logic Controllers (Sebastian Biallas, Jörg Brauer, Stefan Kowalewski), In Dependable Control of Discrete Systems (DCDS'11), IEEE, 2011. [bibtex] [pdf]

[200]	Memory Reduction via Delayed Simulation (Marcus Gelderie, Michael Holtmann), In Proceedings International Workshop on Interactions, Games and Protocols Saarbrücken, Germany, 27th March 2011 (Johannes Reich, Bernd Finkbeiner, eds.), Open Publishing Association, volume 50, 2011. [bibtex] [doi]
[201]	Automatic Test-Case Derivation and Execution in Industrial Control (Sabrina von Styp, Gustavo Quirós, Liyong Yu), In iATPA 2011 : Proceedings of the Workshop on Industrial Automation Tool Integration for Engineering Project Automation ; Toulouse, France, Sep 9, 2011 / ed. by Thomas Moser ..., Sun SITE Central Europe, 2011. [bibtex] [pdf]
[202]	Graph-based Methods for Analysis and Synthesis of Programs (Thomas Ströder), In Proceedings of the Joint Workshop of the German Research Training Groups in Computer Science, GITO mbH Verlag, 2011. [bibtex]
[203]	Past Time LTL Runtime Verification for Microcontroller Binary Code (Thomas Reinbacher, Jörg Brauer, Martin Horauer, Andreas Steininger, Stefan Kowalewski), In 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2011) (Gwen Salaün, Bernhard Schätz, eds.), Springer, volume 6959, 2011. [bibtex] [pdf]
[204]	Comparing Continuous Behaviour in Model-based Development of Embedded Software (Jacob Palczynski, Carsten Weise, Sebastian Moj, Stefan Kowalewski), In Dagstuhl-Workshop MBEES: Modellbasierte Entwicklung eingebetteter Systeme VII (MBEES 2011), fortiss GmbH, 2011. [bibtex]
[205]	Estimation of Clock Drift in HiL Testing by Property-Based Conformance Check (Jacob Palczynski, Carsten Weise, Stefan Kowalewski, Daniel Ulmer), In Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW, TAIC PART) 2011, IEEE Computer Society, 2011. [bibtex]
[206]	Automatic Derivation of Abstract Semantics From Instruction Set Descriptions (Dominique Gückel, Stefan Kowalewski), In Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011), TU Dresden, 2011. [bibtex]
[207]	Degrees of Lookahead in Context-free Infinite Games (Wladimir Fridman, Christof Löding, Martin Zimmermann), In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (Marc Bezem, ed.), Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, volume 12, 2011. [bibtex] [pdf] [doi]
[208]	Analyzing Embedded Systems Code for Mixed-Critical Systems using Hybrid Memory Representations (Eva Beckschulze, Jörg Brauer, André Stollenwerk, Stefan Kowalewski), In 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops ISORCW 2011, IEEE, 2011. [bibtex] [pdf] [doi]

[209]	Memory and delay in regular infinite games (Michael Holtmann), Publikationsserver der RWTH Aachen University, 2011. (Zsfassung in dt. und engl. Sprache; Aachen, Techn. Hochsch., Diss., 2011) [bibtex] [pdf]
[210]	Memory and Delay in Regular Infinite Games (Michael Holtmann), PhD thesis, RWTH Aachen, 2011. [bibtex] [pdf]

2010

[211]

Interactively exploring elimination orderings in symbolic sparse Cholesky factorization (Michael Lülfesmann, Simon R. Lessenich, Hans Bücker), Elsevier, volume 1,1, 2010. (International Conference on Computational Science, ICCS 2010) [bibtex] [pdf] [doi]

[212]	Automated termination analysis for logic programs with cut (Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder, Alexander Serebrenik, René Thiemann), In Theory and Practice of Logic Programming, Cambridge University Press, volume 10, 2010. [bibtex]
[213]	Preface of STACS 2007 Special Issue (W. Thomas, P. Weil), In Theory Comput. Syst., volume 46, 2010. [bibtex]
[214]	When nobody else dreamed of these things - Axel Thue und die Termersetzung (W. Thomas), In Informatik Spektrum, Springer, volume 33, 2010. [bibtex]
[215]	Theoretische Informatik - ein Kurzprofil (W. Thomas), In Informatik Spektrum, Springer, volume 33, 2010. [bibtex]
[216]	On Monadic Theories of Monadic Predicates (W. Thomas), Chapter in Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday (A. Blass, N. Dershowitz, W. Reisig, eds.), Springer, volume 6300, 2010. [bibtex]
[217]	Theoretische Informatik (W. Thomas), In Informatik Spektrum, Springer, volume 33, 2010. [bibtex]
[218]	SMT-Solving for the First-Order Theory of the Reals (Erika Abraham, Ulrich Loup, Bernd Becker, Valeria Bertacoo, Rolf Drechsler, Masahiro Fujita), In Algorithms, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Germany$, 2010. [bibtex]
[219]	Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik. (Erika Ábrahám, Philipp Brauner, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Ulrik Schroeder), In DeLFI, volume 10, 2010. [bibtex]
[220]	A lazy SMT-solver for a non-linear subset of real algebra (Erika Ábrahám, Ulrich Loup, Florian Corzilius, Thomas Sturm), In Proc. of SMT, 2010. [bibtex]
[221]	Model Checking of Software for Microcontrollers (Bastian Schlich), In ACM Transactions in Embedded Computing Systems (TECS), ACM Press, volume 9, 2010. [bibtex] [doi]
[222]	Model Checking Embedded Software of an Industrial Knitting Machine (Thomas Reinbacher, Martin Horauer, Bastian Schlich, Jörg Brauer, Florian Scheuer), In International Journal of Information Technology, Communications and Convergenceonvergence, Inderscience Enterprises Ltd, 2010. [bibtex] [pdf]
[223]	Choice Functions and Well-Orderings over the Infinite Binary Tree (A. Carayol, C. Löding, D. Niwiński, I. Walukiewicz), In Central European Journal of Mathematics, Versita, volume 8, 2010. (Extended version of \citecalo07) [bibtex]

[224]	Formats of Winning Strategies for Six Types of Pushdown Games (W. Fridman), In Proceedings of the First Symposium on Games, Automata, Logic, and Formal Verification, GandALF 2010 (A. Montanari, M. Napoli, M. Parente, eds.), Electronic Proceedings in Theoretical Computer Science, volume 25, 2010. [bibtex]
[225]	DTMC model checking by SCC reduction (Erika Abrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker), In Quantitative Evaluation of Systems (QEST), 2010 Seventh International Conference on the, 2010. [bibtex]
[226]	First-Order Logic with Reachability Predicates on Infinite Systems (Stefan Schulz), In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) (Kamal Lodaya, Meena Mahajan, eds.), Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, volume 8, 2010. [bibtex] [pdf] [doi]
[227]	Testing Continuous Systems Conformance Using Cross Correlation (Jacob Palczynski, Carsten Weise, Stefan Kowalewski), In Proceedings of the 22nd IFIP International Conference on Testing Software and Systems: Short Papers, CRIM, 2010. [bibtex]
[228]	Reachability Games on Automatic Graphs (Daniel Neider), In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA 2010), Springer, volume 6482, 2010. [bibtex]
[229]	Degrees of Lookahead in Regular Infinite Games (Michael Holtmann, Lukasz Kaiser, Wolfgang Thomas), In Foundations of Software Science and Computational Structures (Luke Ong, ed.), Springer, volume 6014, 2010. [bibtex]
[230]	Synthesizing Simulators for Model Checking Microcontroller Binary Code (Dominique Gückel, Bastian Schlich, Jörg Brauer, Stefan Kowalewski), In Proceedings of the 13th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2010), IEEE, 2010. [bibtex] [pdf]
[231]	A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification (Dominique Gückel, Jörg Brauer, Stefan Kowalewski), In Industrial Embedded Systems (SIES 2010), Trento, Italy, IEEE, 2010. [bibtex] [pdf]
[232]	Online Capacity Maximization in Wireless Networks (Alexander Fanghänel, Sascha Geulen, Martin Hoefer, Berthold Vöcking), In Proceedings of the Twenty-second Annual ACM Symposium on Parallelism in Algorithms and Architectures, ACM Press, 2010. [bibtex] [pdf] [doi]
[233]	Towards Architectural Programming of Embedded Systems (Arne Haber, Jan Oliver Ringert, Bernhard Rumpe), In MBEES (Holger Giese, Michaela Huhn, Jan Phillips, Bernhard Schätz, eds.), fortiss GmbH, München, 2010. [bibtex]
[234]	Regret Minimization for Online Buffering Problems Using the Weighted Majority Algorithm (Sascha Geulen, Berthold Vöcking, Melanie Winkler), In COLT 2010 - The 23rd Conference on Learning Theory, Haifa, Israel, June 27-29, 2010, 2010. [bibtex] [pdf]
[235]	Regular cost functions over finite trees (T. Colcombet, C. Löding), In Twenty-Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 2010, IEEE Computer Society, 2010. [bibtex]
[236]	Obliging Games (K. Chatterjee, F. Horn, C. Löding), In 21st International Conference on Concurrency Theory, CONCUR 2010, Springer, volume 6269, 2010. [bibtex]
[237]	Equivalence and Inclusion Problem for Strongly Unambiguous Büchi Automata (Nicolas Bousquet, Christof Löding), In 4th International Conference on Language and Automata Theory and Applications, LATA 2010, Springer, volume 6031, 2010. [bibtex]
[238]	Loop Refinement using Octagons and Satisfiability (Jörg Brauer, Volker Kamin, Stefan Kowalewski, Thomas Noll), In Proceedings of the 5th international conference on Systems software verification, USENIX Association, 2010. [bibtex] [pdf]
[239]	The Automata Learning Framework (Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider, David R. Piegdon), In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV 2010), Springer, volume 6174, 2010. [bibtex]
[240]	Range Analysis of Microcontroller Code using Bit-Level Congruences (Jörg Brauer, Andy King, Stefan Kowalewski), In Formal Methods for Industrial Critical Systems (FMICS 2010), Antwerp, Belgium, Springer, volume 6371, 2010. [bibtex] [pdf]
[241]	Automatic Abstraction for Intervals using Boolean Formulae (Jörg Brauer, Andy King), In Static Analysis Symposium (SAS 2010), Perpignan, France, Springer, volume 6337, 2010. [bibtex] [pdf]
[242]	Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene (Sebastian Biallas, Georg Frey, Stefan Kowalewski, Bastian Schlich, Doaa Soliman), In Tagungsband Entwicklung und Betrieb komplexer Automatisierungssysteme (EKA 2010), ifak Magdeburg, 2010. [bibtex]

[243]	Synthesis of Behavioral Controllers for DES: Increasing Efficiency (K. Bollue, M. Slaats, E. Abraham, W. Thomas, D. Abel), In 10th Int. Workshop on Discrete-Event Systems (WODES'10), 2010. [bibtex]
[244]	Termination Analysis of Logic Programs with Cut Using Dependency Triples (Thomas Ströder, Jürgen Giesl, Peter Schneider-Kamp), In Proceedings of the 11th International Workshop on Termination (Peter Schneider-Kamp, ed.), 2010. [bibtex]
[245]	Test-Case Generation for Embedded Binary Code Using Abstract Interpretation (Thomas Reinbacher, Jörg Brauer, Martin Horauer, Andreas Steininger, Stefan Kowalewski), In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2010), Selected Papers, Mikulov, Czech Republic, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, volume 16, 2010. (Best Paper Award) [bibtex] [pdf]
[246]	A Manifesto for Semantic Model Differencing (Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe), In MoDELS Workshops (Jürgen Dingel, Arnor Solberg, eds.), Springer, volume 6627, 2010. [bibtex]
[247]	Symbolic and Timed Testing (Sabrina von Styp), In Proceedings of the Joint Workshop of the German Research Training Groups in Computer Science, Algorithmic synthesis of reactive and discrete-continuous systems, AlgoSyn 2010, May 31 - June 2, 2010, 2010. [bibtex] [pdf]
[248]	Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software (Jörg Brauer, Thomas Noll, Bastian Schlich), In Proceedings of the 13th International Workshop on Software and Compilers for Embedded Systems (SCOPES 2010), ACM Press, 2010. [bibtex] [pdf]
[249]	Counterexample-guided abstraction refinement for PLCs (Sebastian Biallas, Jörg Brauer, Stefan Kowalewski), In 5th International Workshop on Systems Software Verification (SSV 2010), Vancouver, Canada, USENIX Association, 2010. [bibtex] [pdf]

[250]	Dependency Triples for Improving Termination Analysis of Logic Programs with Cut (T. Ströder, P. Schneider-Kamp, J. Giesl), Technical report, RWTH Aachen, 2010. [bibtex] [pdf]
[251]	Learning Visibly One-Counter Automata in Polynomial Time (Daniel Neider, Christof Löding), Technical report, RWTH Aachen, 2010. [bibtex]
[252]	Stochastic multiplayer games : theory and algorithms (Michael Ummels), Pallas Publ., 2010. (Druck-Ausgabe: 2010. - Online-Ausgabe: 2011; Zugl.: Aachen, Techn. Hochsch., Diss., 2010) [bibtex] [pdf]
[253]	Aspects of Wardrop equilibria (Lars Olbrich), Publikationsserver der RWTH Aachen University, 2010. (Zusammenfassung in engl. und dt. Sprache; Aachen, Techn. Hochsch., Diss., 2010) [bibtex] [pdf]
[254]	Three-valued abstraction for stochastic systems (Daniel Klink), Hut, 2010. (Zsfassung in engl. und dt. Sprache; Aachen, Techn. Hochsch., Diss., 2010) [bibtex] [pdf]
[255]	Algorithmic railway capacity allocation in a competitive European railway market (Sebastian Georg Klabes), Publikationsserver der RWTH Aachen University, 2010. (Aachen, Techn. Hochsch., Diss., 2010) [bibtex] [pdf]

2009

[256]

Handbook of Hybrid Systems Control (Stefan Kowalewski, Mauro Garavello, Hervé Guéguen, Gerlind Herberich, Rom Langerak, Benedetto Piccoli, Jan Willem Polderman, Carsten Weise), Chapter in Hybrid Automata, Cambridge University Press, 2009. [bibtex]

[257]	Path Logics with Synchronization (W. Thomas), Chapter in Perspectives in Concurrency Theory (K. Lodaya, M. Mukund, R. Ramanujam, eds.), Universities Press, 2009. [bibtex]
[258]	DFG Research Training Group: Algorithmic Synthesis of Reactive and Discrete-Continuous Systems (AlgoSyn) (W. Thomas, K. Bollue, D. Gückel, G. Quiros, M. Slaats, M. Ummels), In it - Information Technology, volume 51, 2009. (http://www.atypon-link.com/OLD/doi/pdf/10.1524/itit.2009.0545?cookieSet=1link) [bibtex]
[259]	Termination Analysis by Dependency Pairs and Inductive Theorem Proving (Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp), Chapter in Proceedings of the 22nd International Conference on Automated Deduction (Renate A. Schmidt, ed.), Springer-Verlag, volume 5663, 2009. [bibtex]
[260]	Model Checking C Source Code for Embedded Systems (Bastian Schlich, Stefan Kowalewski), In International Journal on Software Tools for Technology Transfer (STTT), Springer, volume 11, 2009. [bibtex] [doi]
[261]	Parallel and Distributed Invariant Checking of Microcontroller Software (Jörg Brauer, Bastian Schlich, Stefan Kowalewski), In Electronic Notes in Theoretical Computer Science, Elsevier, volume 254, 2009. (Proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)) [bibtex] [pdf]
[262]	Interprocedural Pointer Analysis in Goanna (Jörg Brauer, Ralf Huuck, Bastian Schlich), In Electronic Notes in Theoretical Computer Science, Elsevier, volume 254, 2009. (Proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)) [bibtex] [pdf]

[263]	The Reachability Problem over Infinite Graphs (W. Thomas), In Proceedings of the 4th International Computer Science Symposium in Russia, CSR 2009 (A E. Frid, A. Morozov, A. Rybalchenko, K. W. Wagner, eds.), Springer, volume 5675, 2009. [bibtex]
[264]	Facets of Synthesis: Revisiting Church's Problem (W. Thomas), In Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2009, Springer, volume 5504, 2009. [bibtex]
[265]	Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies (P. Hänsch, M. Slaats, W. Thomas), In FCT 2009, Springer, volume 5699, 2009. [bibtex]
[266]	Synthesis of Behavioral Controllers for Discrete Event Systems with NCES-like Petri Net Models (K. Bollue, D. Abel, W. Thomas), In Proceedings of the European Control Conference, ECC 2009, 2009. [bibtex]
[267]	Realising deterministic behavior from multiple non-deterministic behaviors (Thomas Ströder, Maurice Pagnucco), In Proceedings of the 21st International Joint Conference on Artifical Intelligence, Morgan Kaufmann Publishers Inc., 2009. [bibtex]
[268]	Mapping Requirements Models to Mathematical Models in Control Systems Development (Dominik Schmitz, M. Zhang, Thomas Rose, Matthias Jarke, Andreas Polzer, Jacob Palczynski, Stefan Kowalewski, Michael Reke), In Model Driven Architecture - Foundations and Applications, 5th European Conference, ECMDA-FA 2009, Springer, volume 5562, 2009. [bibtex] [doi]
[269]	Reduction of Interrupt Handler Executions for Model Checking Embedded Software (B. Schlich, T. Noll, J. Brauer, L. Brutschy), In Haifa Verification Conference (HVC 2009), Haifa, Israel, Springer, volume 6405, 2009. [bibtex] [pdf]
[270]	Verifikation von SPS-Programmen in AWL mit Hilfe von direktem Model-Checking (Bastian Schlich, Stefan Kowalewski, Jörg Wernerus), In AUTOMATION 2009, Baden-Baden, Germany, VDI Verlag, 2009. [bibtex] [pdf]
[271]	Direct Model Checking of PLC Programs in IL (Bastian Schlich, Jörg Brauer, Jörg Wernerus, Stefan Kowalewski), In Dependable Control of Discrete Systems (DCDS'09), Bari, Italy, 2009. [bibtex] [pdf]
[272]	Refining Assembly Code Static Analysis for the Intel MCS-51 Microcontroller (Thomas Reinbacher, Jörg Brauer, Martin Horauer, Bastian Schlich), In Industrial Embedded Systems (SIES'09), Lausanne, Switzerland, IEEE Computer Society Press, 2009. [bibtex] [pdf] [doi]
[273]	Early Behaviour Modelling for Control Systems (Jacob Palczynski, Stefan Kowalewski), In UKSIM European Symposium on Computer Modeling and Simulation, IEEE Computer Society, volume 0, 2009. [bibtex] [doi]
[274]	Retargeting a Hardware-Dependent Model Checker by Using Architecture Description Languages (Dominique Gückel), In Doctoral Symposium on Systems Software Verification (DS SSV 2009), 2009. [bibtex] [pdf]
[275]	System Model-Based Definition of Modeling Language Semantics (Hans Grönniger, Jan Oliver Ringert, Bernhard Rumpe), In FMOODS/FORTE (David Lee, Antónia Lopes, Arnd Poetzsch-Heffter, eds.), Springer, volume 5522, 2009. [bibtex]

[276]	Teaching Erlang using robotics and player/stage (Sten Grüner, Thomas Lorentsen), In Proceedings of the 2009 ACM SIGPLAN Erlang Workshop ; Edinburgh, 5 September 2009 ; co-located with: ICFP'09 / sponsored by: ACM SIGPLAN, ACM Press, 2009. [bibtex] [doi]
[277]	Stack Bounds Analysis of Microcontroller Assembly Code (Jörg Brauer, Bastian Schlich, Thomas Reinbacher, Stefan Kowalewski), In Workshop on Embedded Security (WESS 2009), Grenoble, France, ACM Press, 2009. [bibtex] [pdf]

[278]	Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies (P. Hänsch, M. Slaats, W. Thomas), Technical report, RWTH Aachen, 2009. (Full version of \citehaslth09a) [bibtex]
[279]	First-Order Logic with Reachability Predicates over Infinite Systems (Stefan Schulz), Diploma thesis, RWTH-Aachen, 2009. [bibtex]
[280]	Combinatorial optimization and recognition of graph classes with applications to related models (George B. Mertzios), Publikationsserver der RWTH Aachen University, 2009. (Aachen, Techn. Hochsch., Diss., 2009) [bibtex] [pdf]
[281]	Logic and Automata over Infinite Trees (Christof Löding), Habilitation Thesis, RWTH Aachen, Germany, 2009. [bibtex]
[282]	Learning communicating and nondeterministic automata (Carsten Kern), RWTH Aachen, Department of Computer Science, volume 2009,17, 2009. (Zsfassung in engl. und dt. Sprache; Zugl.: Aachen, Techn. Hochsch., Diss., 2009) [bibtex] [pdf]

2008

[283]	Solution of Church's Problem: A Tutorial (W. Thomas), Chapter in New Perspectives on Games and interaction (K. Apt, R. van Rooij, eds.), Amsterdam University Press, volume 4, 2008. [bibtex]
[284]	Church's Problem and a Tour through Automata Theory (W. Thomas), Chapter in Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday (A. Avron, N. Dershowitz, A. Rabinovich, eds.), Springer, volume 4800, 2008. [bibtex]
[285]	Proving Correctness of an Efficient Abstraction for Interrupt Handling (Gerlind Herberich, Thomas Noll, Bastian Schlich, Carsten Weise), In Electronic Notes in Theoretical Computer Science, Elsevier, volume 217, 2008. (Proceedings of the 3rd International Workshop on Systems Software Verification (SSV 2008)) [bibtex] [doi]
[286]	Improving Context-Sensitive Dependency Pairs (Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutiérrez, Salvador Lucas, Peter Schneider-Kamp, René Thiemann), Chapter in Logic for Programming, Artificial Intelligence, and Reasoning (Iliano Cervesato, Helmut Veith, Andrei Voronkov, eds.), Springer-Verlag, volume 5330, 2008. [bibtex]

[287]	Model Transformations in Decidability Proofs for Monadic Theories (W. Thomas), In Proceedings of the 17th EACSL Annual Conference on Computer Science Logic, CLS 2008 (M. Kaminski, S. Martini, eds.), Springer, volume 5213, 2008. [bibtex]
[288]	Optimizing Winning Strategies in Regular Infinite Games (W. Thomas), In Proceedings of the 34th Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2008, Springer, volume 4910, 2008. [bibtex]
[289]	Lernverfahren für Automaten über linearisierten XML-Dokumenten (D. Neider), In Informatik Spektrum, Springer, 2008. [bibtex]
[290]	Optimal Strategy Synthesis for Request-Response Games (F. Horn, W. Thomas, N. Wallmeier), In Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008, Springer, volume 5311, 2008. [bibtex]
[291]	Positional Strategies for Higher-Order Pushdown Parity Games (A. Carayol, M. Slaats), In Mathematical Foundations of Computer Science 2008, Springer, volume 5162, 2008. [bibtex]
[292]	Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code (Bastian Schlich, Jann Löll, Stefan Kowalewski), In Formal Methods for Industrial Critical Systems (FMICS 2007), Berlin, Germany, Springer, volume 4916, 2008. [bibtex] [doi]
[293]	Modeling the Environment of Microcontrollers to Tackle the State-Explosion Problem in Model Checking (Bastian Schlich, Dominique Gückel, Stefan Kowalewski), In Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2008), Budapest, Hungary (G. Tarnai, E. Schnieder, eds.), L'Harmattan, 2008. [bibtex]
[294]	Modellbasierte Anforderungserfassung für softwarebasierte Regelungen (Dominik Schmitz, Peter Drews, Frank Heßeler, Matthias Jarke, Stefan Kowalewski, Jacob Palczynski, Andreas Polzer, Michael Reke, Thomas Rose), In Software Engineering, GI, volume 121, 2008. [bibtex]
[295]	Motivating Model Checking for Embedded Systems Software (Thomas Reinbacher, Michael Kramer, Martin Horauer, Bastian Schlich), In Mechatronic and Embedded Systems and Applications (MESA08), Beijing, China, IEEE Computer Society Press, 2008. [bibtex] [doi]
[296]	Challenges in Embedded Model Checking --- A Simulator for the [mc]square Model Checker (Thomas Reinbacher, Michael Kramer, Martin Horauer, Bastian Schlich), In Industrial Embedded Systems (SIES 2008), Le Grande Motte, France, IEEE Computer Society Press, 2008. [bibtex] [doi]
[297]	Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code (Thomas Noll, Bastian Schlich), In Hardware and Software: Verification and Testing (HVC 2007), Haifa, Israel, Springer, volume 4899, 2008. [bibtex] [doi]
[298]	Learning Automata for Streaming XML Documents (Daniel Neider), In Informatiktage 2008. Fachwissenschaftlicher Informatik-Kongress, 14. und 15. März 2008, B-IT Bonn-Aachen International Center for Information Technology in Bonn, 2008. [bibtex]
[299]	The Nesting-Depth of Disjunctive mu-calculus for Tree Languages and the Limitedness Problem (T. Colcombet, C. Löding), In Proceedings of the 17th EACSL Annual Conference on Computer Science Logic CSL 2008, Springer, volume 5213, 2008. [bibtex]
[300]	The Non-Deterministic Mostowski Hierarchy and Distance-Parity Automata (T. Colcombet, C. Löding), In Proceedings of the 35th International Colloquium on Automata, Languages and Programming, ICALP 2008, Springer, volume 5126, 2008. [bibtex]
[301]	Direct Support for Model Checking of Abstract State Machines by Utilizing Simulation (Jörg Beckers, Daniel Klünder, Stefan Kowalewski, Bastian Schlich), In Abstract State Machines, B and Z (ABZ 2008), London, UK, Springer, volume 5238, 2008. [bibtex] [doi]

[302]

Logic and games on automatic structures (Lukasz Kaiser), Publikationsserver der RWTH Aachen University, 2008. (Aachen, Techn. Hochsch., Diss., 2008) [bibtex] [pdf]