Thomas Noll
- noll at cs.rwth-aachen.de
- Address
- Room 4211 (Faculty of CS, building E1 (2353), 2nd floor)
Ahornstraße 55
D-52074 Aachen - Phone
- +49 241 80 21213
I am an associate professor (apl. Prof.) at the Software Modeling and Verification Group (MOVES), headed by Prof. Joost-Pieter Katoen, in the Faculty of Computer Science at RWTH Aachen University. The office is located at the Computer Science Center. My current research interests include:
- Static Program Analysis for Software Optimisation and Verification
- Compilation of Quantum Software
- Reliability, Safety and Security of Hardware/Software Systems
- Formal Verification of Artificial Neural Networks
Conferences and Workshops
Publications
Courses and Seminars
Supervision of Theses
Administration
Publications
| 2026 | |
|---|---|
| DOI | Martin Baum. Heuristic circuit mapping strategies for the SpinBus architecture, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2026. |
| Samuel Akinlaja. Which probabalistic programs are modelcheckable?, 2026. | |
| DOI | Jonas Seidel. Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2026. |
| Xufei Xie. Visualizing execution-schedules for conveyor-based quantum computing hardware, 2026. | |
| Felix Euting. Distribution transformers for probabilistic programs: a study of inductive definability, 2026. | |
| 2025 | |
| DOI | Thomas Noll, Christina Gehnen, Roy Hermanns. Quantum Computing: From Weakest Preconditions to Voltage Pulses, Principles of verification: cycling the probabilistic landscape, Part 1 / Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk, editors, 201-229, Springer, 2025. |
| DOI | . Principles of verification: cycling the probabilistic landscape, Part 1, xix, 447 Seiten : Illustrationen, Diagramme, Springer, 2025. |
| DOI | . Principles of verification: cycling the probabilistic landscape : essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday, Part 2, xiv, 395 Seiten : Illustrationen, Springer, 2025. |
| DOI | . Principles of verification: cycling the probabilistic landscape : essays dedicated to Joost-Pieter Katoen on the occasion of his 60th Birthday, Part 3, xv, 503 Seiten : Illustrationen, Diagramme, Springer, 2025. |
| DOI | Dominik Geißler. Automata-based semantics for the probabilistic programming language ReDiP, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025. |
| DOI | Emil Beothy-Elo. Effective quantifier-based reasoning for quantitative deductive verification, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025. |
| Elbeck Lazaridi. Implementing the denotational semantics of probabilistic programs, 2025. | |
| DOI | Marcel Eissing. On the relation of rely-guarantee and assume-guarantee reasoning, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025. |
| Johannes Peter Valentin Gaidetzka. Quantum circuit optimization through eliminating and deferring mid-circuit measurements, 2025. | |
| Glen Jordan Grant. Exploration of certificate sharing for neural network verification, 2025. | |
| Sophia Greiwe. Implementation of PRNG-based elimination of intermediate measurements in quantum circuits, 2025. | |
| DOI | Mareike Metzler. Evaluating tool support for fault tree analysis of satellite constellations, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025. |
| Dobromir Panayotov. Scalable qubit routing on the conveyor-based SpinBus architecture, 2025. | |
| Rico Stanosek. Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates, 2025. | |
| Sascha Thiemann. Compilation of quantum programs with control flow primitives in superposition, 2025. | |
| Muhammad Asad Murtaza Butt. Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies, 2025. | |
| DOI | Dominic Sebastian Meiser. Multi‐agent path finding for reversible conveyors, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025. |
| DOI | Christopher Jan-Steffen Brix, Julia Walczak, Nils Michael Lommen, Thomas Noll. Using GPUs And LLMs Can Be Satisfying for Nonlinear Real Arithmetic Problems, ICLR 2025 Workshop: VerifAI: AI Verification in the Wild : ICLR 2025 Workshop VerifAI Singapore, Apr 27 2025, 1-53, 2025. |
| 2024 | |
| DOI | Alexander Ferber. Combining integer programs and graph grammars: Theory and implementation in Attestor, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024. |
| DOI | Tom Biskup. Invariant-based strategy synthesis for nondeterministic probabilistic programs, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024. |
| DOI | Naomi Barth. Compositional control-flow reduction for probabilistic model checking, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024. |
| DOI | Johannes Lehmann. Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024. |
| DOI | Songran Shi. Application of Reinforcement Learning to the Game of Reversi++, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024. |
| DOI | Anastasiia Petrova. Model checking pPDA vs unambiguous automata, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024. |
| DOI | Dinis Vitorino. Most probable explanations in Bayesian Networks via weighted programming, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024. |
| Frederik Heigold. Semantics-preserving transformation of Java source code, 2024. | |
| Roy Hermanns. Optimized routing for shuttling-based quantum processing architectures, 2024. | |
| Jakob Sprang. Heuristic synthesis of spare parts inventories using dynamic fault trees, 2024. | |
| Sven Büge. Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm, 2024. | |
| DOI | Patrick Nossol. Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024. |
| Daniel Johannes Zilken. Distributional invariants for probabilistic programs, 2024. | |
| Yejun Tang. Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks, 2024. | |
| Julia Walczak. Testing the applicability of robustness evaluation methods for neural networks on nonlinear real arithmetic problems using α-β-CROWN and foolbox, 2024. | |
| Patrick Arens. MARVEL: A stepwise debugging tool for Markov models in the PRISM-language, 2024. | |
| 2023 | |
| DOI | Yussur Mustafa Oraji. Evaluating static analysis techniques to accelerate data race detection for MPI RMA, 1 Online-Ressource : Diagramme, RWTH Aachen University, 2023. |
| DOI | Sascha Müller. Synthesizing FDIR recovery strategies for space systems, 1 Online-Ressource : Illustrationen, Diagramme, RWTH Aachen University, 2023. |
| DOI | . 22. Kolloquium Programmiersprachen und Grundlagen der Programmierung, 1 Online-Ressource, RWTH Aachen University, Department of Computer Science, 2023. |
| Felix Faber. Comparison of symbolic maximal end component decomposition algorithms, 61 Seiten : Illustrationen, Diagramme, 2023. | |
| Gergana Tropcheva. Strategy computation for a Markovian disease spread model, 2023. | |
| Umut Yigit Dural. Automatic algorithm selection for probabilistic model checking using machine learning, 2023. | |
| Jialei Yao. Representing Markov models by extending the intermediate model checking language, 67 Seiten : Illustrationen, 2023. | |
| Timm Spork. Approximate probabilistic bisimulations and quotienting, 186 Seiten : Illustrationen, 2023. | |
| Stefan Busch. Slicing COBOL software for program understanding, 2023. | |
| Daniel Alexander Heinen. Architecture-oriented safety verification of transformer networks via program analysis, 2023. | |
| Ebru Kusak. Automated assessment of regular expressions, 2023. | |
| Lasse Woude. Evaluation of out-of-distribution detection techniques for dataset filtering, 2023. | |
| 2022 | |
| DOI | Kevin Batz, Ira Justus Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll. Foundations for Entailment Checking in Quantitative Separation Logic, Programming Languages and Systems : 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings / edited by Ilya Sergey, 57-84, Springer International Publishing, 2022. |
| Simon Schotten, Thorsten Büker, Wiebke Lenze, Bastian Kogel, Thomas Noll, Mario Fietze, Jana Berger. Einblick DZSF-Projekt "Identifikation von Kapazitätsengpässen", 33-37, DVV Media Group, Eurailpress, 2022. | |
| Darion Haase. A unified slicing framework for probabilistic programs, 2022. | |
| Lisa Pühl. Verification of neural networks using binary tree search for branching, 2022. | |
| DOI | Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll. Towards Concurrent Quantitative Separation Logic, 33rd International Conference on Concurrency Theory (CONCUR 2022) / Herausgeber: Bartek Klin, Slawomir Lasota, Anca Muscholl, 25:1-25:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. |
| DOI | Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll. Towards Concurrent Quantitative Separation Logic, [1]-62, 2022. |
| . 50 Jahre Studiengang Informatik an der RWTH Aachen : Ein Streifzug in Text und Bild, 152 Seiten : Illustrationen, Diagramme, Fachgruppe Informatik in der Fakultät für Mathematik, Informatik und Naturwissenschaften der RWTH Aachen, 2022. | |
| DOI | Mohamed Khalifa. Termination analysis of procedural pointer programs modelled by graph grammars, 1 Online-Ressource : Diagramme, RWTH Aachen University, 2022. |
| DOI | Philipp Berger, Wiebke Lenze, Thomas Noll, Simon Schotten, Thorsten Büker, Mario Fietze, Bastian Kogel. Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining, Formal Methods for Industrial Critical Systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14–15, 2022, Proceedings / edited by Jan Friso Groote, Marieke Huisman, 121-133, Springer, 2022. |
| Jan Jeremy Tugsbayar. Verification of leader election protocols for dynamic networks, 2022. | |
| Dominic Sebastian Meiser. Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation, 2022. | |
| DOI | Wiebke Lenze, Bastian Kogel, Simon Schotten, Thorsten Büker, Thomas Noll, Philipp Berger, Mario Fietze. Identification of Bottlenecks in Rail Infrastructure, Proceedings of the Fifth International Conference on Railway Technology: Research, Development and Maintenance Edited by J. Pombo Civil-Comp Conferences. - Volume 1, 23.12, Civil-Comp Press, 2022. |
| Denis Kuksaus. Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung, 2022. | |
| Jan Erik Karuc. Verifying parametric Markov models using decision diagrams, 2022. | |
| DOI | Christina Gehnen. POMDP-based execution models for probabilistic programs with partial observability, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2022. |
| Jonas Seidel. Comparison of heuristics for branching in neural network verification, 75 Seiten : Illustrationen, 2022. | |
| Caroline Jabs. Novelty-detection-based split selection heuristics for neural network verification, 2022. | |
| Ben Sturgis. Automatic verification of loop invariants in weighted programs, 2022. | |
| Christian Blumenthal. Inference in discrete probabilistic programs using probability generating functions, 2022. | |
| Laura Bamberger. Implementation of an LTL model checker for probabilistic pushdown automata, 2022. | |
| 2021 | |
| DOI | Dario Veltri. Learning probabilistic automata with SMT solving, 71 Seiten, RWTH Aachen University, 2021. |
| Mengying Xue. Efficient analysis of time-bounded reachability in markov automata, 2021. | |
| DOI | Ira Justus Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte. Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars, Graph Transformation : 14th International Conference, ICGT 2021, Held As Part of STAF 2021, Virtual Event, June 24-25, 2021, Proceedings, 283-293, Springer International Publishing, 2021. |
| Domenic Quirl. IDE-Ready parsing of compile-time dynamic languages, 2021. | |
| Patrick Arens. Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs, 2021. | |
| Marvin Jansen. Decidability and complexity of entailment checking in quantitative separation logic, 2021. | |
| Niklas Kotowski. Accelerating symbolic simulation to analyze the effect of delays in train timetables, 70 S., 2021. | |
| DOI | Sascha Müller, Adeline Jordon, Andreas Gerndt, Thomas Noll. A Modular Approach to Non-deterministic Dynamic Fault Trees, Computer Safety, Reliability, and Security : 40th International Conference, SAFECOMP 2021, York, UK, September 8–10, 2021, Proceedings / edited by Ibrahim Habli, Mark Sujan, Friedemann Bitsch, 243-257, Springer International Publishing, 2021. |
| DOI | Alexander Hoppen, Thomas Noll. A Debugger for Probabilistic Programs, Software Engineering and Formal Methods : 19th International Conference, SEFM 2021, Virtual Event, December 6–10, 2021, Proceedings / edited by Radu Calinescu, Corina S. Păsăreanu, 282-289, Springer, 2021. |
| Felix Tomski. Developing an on-the-fly vector clock exchange for distributed memory systems using the generic tool infrastructure, 89 S., 2021. | |
| Fabian Gasser. Analysis of concurrent probabilistic programs with shared variables, 27 Seiten, 2021. | |
| DOI | Christina Gehnen. Automata-based model checking of recursive systems, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2021. |
| 2020 | |
| DOI | Tim Felix Lange, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen. IC3 software model checking, 135-161, Springer, 2020. |
| Thomas Vogt. Learning RFSA in Reverse, 2020. | |
| DOI | Dan-Tuong Le. Quantitative Analysis of Counterexample Generation for Automata Learning, 2020. |
| DOI | Christopher Jan-Steffen Brix, Thomas Noll. Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs, 12 Seiten, 2020. |
| DOI | Sascha Müller, Liana Mikaelyan, Andreas Gerndt, Thomas Noll. Synthesizing and optimizing FDIR recovery strategies from fault trees, 102478, Elsevier Science, 2020. |
| Alexander Hoppen. Design and implementation of an interactive exploration tool for probabilistic programs, 124 Seiten, 2020. | |
| Christopher Brix. Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds, 2020. | |
| DOI | Linus Heck. Gradient descent on parametric Markov Chains, 31 Seiten, 2020. |
| DOI | Mohamed Khalifa. Implementation of a Predicate-Guided Termination Analysis for Pointer Programs, 2020. |
| Adrian Gallus. RPrIC3: PrIC3 for expected rewards, 2020. | |
| DOI | Daniel Basgöze. Dynamic fault tree analysis using binary decision diagrams, 76 Seiten, 2020. |
| Lars Beckers. A petri net semantics for boolean-logic driven markov processes, 55 Seiten, 2020. | |
| Robin Drahovsky. Parameter synthesis in bayesian networks, 2020. | |
| 2019 | |
| DOI | Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs, 34, ACM, 2019. |
| DOI | Liana Mikaelyan, Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing and Optimizing FDIR Recovery Strategies from Fault Trees, Formal techniques for safety-critical systems : 6th International Workshop, FTSCS 2018, Gold Coast, Australia, November 16, 2018 : revised selected papers / Cyrille Artho, Peter Csaba Ölveczky, editors, 37-54, Springer, 2019. |
| DOI | Ira Justus Fesefeldt. Proving termination of pointer programs on top of symbolic execution, 118 S., 2019. |
| DOI | Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. COMPASS 3.0, Tools and algorithms for the construction and analysis of systems : 25th international conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019 : proceedings / Tomáš Vojnar, Lijun Zhang (Eds.). - Part 1, 379-385, Springer Open, 2019. |
| 2018 | |
| DOI | Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Graph-Based Shape Analysis Beyond Context-Freeness, Software engineering and formal methods : 16th International Conference, SEFM 2018, held as part of STAF 2018, Toulouse, France, June 27-29, 2018 : proceedings / Einar Broch Johnsen, Ina Schaefer (eds.), 271-286, Springer, 2018. |
| DOI | Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs, 159 Seiten, 2018. |
| DOI | Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Let this Graph Be Your Witness! : An Attestor for Verifying Java Pointer Programs, Computer Aided Verification : 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II / edited by Hana Chockler, Georg Weissenbacher, 3-11, Springer, 2018. |
| DOI | Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, Klaus Wehrle. Symbolic Liveness Analysis of Real-World Software, Computer Aided Verification : 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II / edited by Hana Chockler, Georg Weissenbacher, 447-466, Springer, 2018. |
| DOI | Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen. Improving Generalization in Software IC3, Model checking software : 25th International Symposium, SPIN 2018, Malaga, Spain, June 20-22, 2018 : proceedings / Maria del Mar Gallardo, Pedro Merino (eds.), 85-102, Springer, 2018. |
| DOI | Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic, LPAR-22 : 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning / editors: Gilles Barthe, Geoff Sutcliffe and Margus Veanes, 23-36, EasyChair, 2018. |
| DOI | Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing Failure Detection, Isolation, and Recovery Strategies from Nondeterministic Dynamic Fault Trees, 2018. |
| 2017 | |
| DOI | Christina Jansen. Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic, 1 Online-Ressource (xi, 286 Seiten) : Diagramme, 2017. |
| DOI | Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, Programming languages and systems : 26th European Symposium on Programming, ESOP 2017, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017 : proceedings / Hongseok Yang (ed.), 611-638, Springer, 2017. |
| DOI | Louis Wachtmeister, Thomas Noll. Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications, [embeddedworld Exibition & Conference, 2017-03-14 - 2017-03-16, Nuremberg, Germany], 5 Seiten, Zenodo, 2017. |
| DOI | Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees, AIAA Space and Astronautics Forum and Exposition 2017 : Orlando, Florida, USA, 12-14 September 2017 / American Institute of Aeronautics and Astronautics. - Volume 2, 1140-1149, Curran Associates, Inc., 2017. |
| Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. The COMPASS 3.0 Toolset, 2 Seiten, 2017. | |
| DOI | Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. Formal Methods for Aerospace Systems : Achievements and Challenges, Cyber-Physical System Design from an Architecture Analysis Viewpoint : Communications of NII Shonan Meetings / edited by Shin Nakajima, Jean-Pierre Talpin, Masumi Toyoshima, Huafeng Yu, 133-159, Springer Singapore, 2017. |
| Marieke Huisman, Thomas Noll, Makoto Tatsuta. Analysis and Verification of Pointer Programs : October 2-5, 2017, 15 Seiten, National Institute of Informatics, 2017. | |
| DOI | Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness, 44 Seiten, 2017. |
| 2016 | |
| DOI | Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 115 Seiten, 2016. |
| 2015 | |
| DOI | Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Verifying pointer programs using graph grammars, 157-162, Elsevier, 2015. |
| DOI | Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Juggrnaut: using graph grammars for abstracting unbounded heap structures, 159-203, Springer Science + Business Media B.V, 2015. |
| DOI | Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen, Thomas Noll. Compositional Analysis Using Component-Oriented Interpolation, Formal aspects of component software : 11th international symposium, FACS 2014, Bertinoro, Italy, September 10 - 12, 2014 ; revised selected papers / Ivan Lanese; Eric Madelaine (eds.), 69-85, Springer International Publishing, 2015. |
| DOI | Christoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic, Programming languages and systems : 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings / edited by Xinyu Feng, Sungwoo Park, 90-108, Springer International Publishing, 2015. |
| Kevin Van der Pol, Thomas Noll. Security Type Checking for MILS-AADL Specifications, [International Workshop on MILS: Architecture and Assurance for Secure Systems, 20.01.2015-20.01.2015, Amsterdam, Netherlands], 10 Seiten, 2015. | |
| Tim Lange, Martin R. Neuhäußer, Thomas Noll. IC3 Software Model Checking on Control Flow Automata, Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design (FMCAD 2015) : Austin, Texas, USA , September 27 - 30, 2015 / Edited by Roope Kaivola and Thomas Wahl, 97-104, FMCAD Inc, 2015. | |
| Kevin Van der Pol, Thomas Noll. Security Type Checking for MILS-AADL Specifications, 25 Folien, 2015. | |
| 2014 | |
| DOI | Christina Jansen, Florian Göbe, Thomas Noll. Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs, Graph transformation : 7th international conference, ICGT 2014, held as part of STAF 2014, York, UK, July 22 - 24, 2014 ; proceedings / Holger Giese ... (eds.), 65-80, Springer, 2014. |
| DOI | Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Panagiotis Katsaros, Konstantinos Mokos, Viet Yen Nguyen, Thomas Noll, Bart Postma, Marco Roveri. Spacecraft early design validation using formal methods, 20-35, Elsevier, 2014. |
| DOI | Christina Jansen, Thomas Noll. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs, Graph transformation : 7th international conference, ICGT 2014, held as part of STAF 2014, York, UK, July 22 - 24, 2014 ; proceedings / Holger Giese; Barbara König (eds.), 49-64, Springer, 2014. |
| DOI | Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu. Performance Analysis of Computing Servers : a case study exploiting a new GSPN semantics, Measurement, modelling, and evaluation of computing systems and dependability and fault-tolerance : 17th International GI/ITG Conference, MMB DFT 2014, Bamberg, Germany, March 17 - 19, 2014 ; proceedings / Kai Fischbach; Udo R. Krieger (eds.), 57-72, Springer, 2014. |
| DOI | Thomas Noll. Safety, Dependability and Performance Analysis of Aerospace Systems, Formal Techniques for Safety-Critical Systems : Third International Workshop, FTSCS 2014, Luxembourg, November 6-7, 2014. Revised Selected Papers / edited by Cyrille Artho, Peter Csaba Ölveczky, 17-31, Springer, 2014. |
| DOI | Dimitri Bohlender, Harold Yorick Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, Thomas Noll. A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models, Leveraging applications of formal methods, verification and validation : specialized techniques and applications ; 6th international symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8 - 11, 2014 ; proceedings, part II / Tiziana Margaria; Bernhard Steffen (eds.), 177-192, Springer, 2014. |
| Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. Formal Validation Methods in Model-Based Spacecraft Systems Engineering, Modeling and simulation-based systems engineering handbook / ed. Daniele Gianni ; Andrea D'Ambrogio ; Andreas Tolk, 340-375, Taylor,Francis, 2014. | |
| 2013 | |
| DOI | Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu. Model-Based Energy Optimization of Automotive Control Systems, 2013 Design, Automation & Test in Europe Conference & Exhibition (DATE 2013) : Grenoble, France, 18 - 22 March 2013 / [sponsors: EDAA, European Design and Automation Association ...], 761-766, IEEE, 2013. |
| DOI | Bernhard Ern, Viet Yen Nguyen, Thomas Noll. Characterization of Failure Effects on AADL Models, Computer safety, reliability, and security : 32nd International Conference, SAFECOMP 2013, Toulouse, France, September 24-27, 2013 ; proceedings / Friedemann Bitsch ... (ed.), 241-252, Springer, 2013. |
| DOI | Markus Bals, Christina Jansen, Thomas Noll. Incremental Construction of Greibach Normal Form for Context-Free Grammars, Proceedings : 2013 International Symposium on Theoretical Aspects of Software Engineering : 1-3 July 2013, Birmingham, United Kingdom, 165-168, IEEE Computer Society, 2013. |
| DOI | Tim Lange, Martin R. Neuhäußer, Thomas Noll. Speeding Up the Safety Verification of Programmable Logic Controller Code, Hardware and software: verification and testing : 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013 ; proceedings / Valeria Bertacco; Axel Legay (eds.), 44-60, Springer, 2013. |
| 2012 | |
| DOI | Kamal Barakat, Stefan Kowalewski, Thomas Noll. A Native Approach to Modeling Timed Behavior in the Pi-Calculus, IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering : Beijing, China, 4 – 6 July 2012 ; proceedings / Edited by Tiziana Margaria, Zongyan Qiu, and Hongli Yang, 253-256, IEEE, 2012. |
| DOI | Thomas Noll. Correctness, Safety and Fault Tolerance in Aerospace Systems : The ESA COMPASS Project, 42, Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2012. |
| 2011 | |
| DOI | Bastian Schlich, Thomas Noll, Jörg Brauer, Lucas Brutschy. Reduction of Interrupt Handler Executions for Model Checking Embedded Software, Hardware and software: verification and testing : 5th International Haifa Verification Conference, HCV 2009, Haifa, Israel, October 19-22, 2009 : revised selected papers / Kedar Namjoshi ... (eds.), Springer, 2011. |
| DOI | Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll. A Local Greibach Normal Form for Hyperedge Replacement Grammars, Language and automata theory and applications : 5th international conference, LATA 2011, Tarragona, Spain, May 26-31, 2011 ; proceedings / Adrian-Horia Dediu ... (eds.), 323-335, Springer, 2011. |
| Joost-Pieter Katoen, Thomas Noll. Trustworthy Aerospace Systems, 204-205, PS, PublicService.co.uk Ltd, 2011. | |
| DOI | Yuri Yushtein, Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Xavier Olive, Marco Roveri. System-Software Co-Engineering: Dependability and Safety Perspective, Proceedings, Fourth IEEE International Conference on Space Mission Challenges for Information Technology : SMC-IT 2011 : 2-4 August 2011, Palo Alto, California, USA, 18-25, IEEE CS Press, 2011. |
| 2010 | |
| DOI | Jörg Brauer, Thomas Noll, Bastian Schlich. Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software, SCOPES '10 Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems : St. Goar, Germany - June 29-30, 2010, ACM, 2010. |
| DOI | Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer. A Model Checker for AADL, Computer aided verification : 22nd international conference, CAV 2010, Edinburgh, UK, July 15-19, 2010 ; proceedings / Tayssir Touili; Byron Cook; Paul Jackson (eds.), 562-565, Springer, 2010. |
| Jörg Brauer, Volker Kamin, Stefan Kowalewski, Thomas Noll. Loop Refinement using Octagons and Satisfiability, SSV'10 : Proceedings of the 5th international conference on Systems software verification, 9 S., ACM, 2010. | |
| DOI | Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Safety, Dependability, and Performance Analysis of Extended AADL Models, Univ. Press, 2010. |
| 2009 | |
| DOI | Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems, Computer safety, reliability, and security : 28th international conference, SAFECOMP 2009, Hamburg, Germany, September 15-18, 2009 ; proceedings / Bettina Buth ... (eds.), 173-186, Springer, 2009. |
| DOI | Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. Codesign of Dependable Systems: A Component-Based Modeling Language, Seventh ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009): Cambridge, Massachusetts, July 13-15, 2009, 121-130, IEEE, 2009. |
| Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Model-Based Codesign of Critical Embedded Systems, Workshop Proceedings / ACES-MB 2009 : Proceedings of the 2nd International Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB 2009) ; held as part of the 2009 International Conference on Model Driven Engineering Languages and Systems (MoDELS'09) ; Denver, Colorado, USA, October 6, 2009 / Ed. by Stefan Van Baelen ..., 87-91, RWTH Aachen, 2009. | |
| Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Verification and Performance Evaluation of AADL Models (Tool Demonstration), ESEC-FSE’09 : Proceedings of the Joint 12th European Software Engineering Conference and 17th ACM SIGSOFT Symposium on the Foundations of Software Engineering ; August 24–28, 2009, Amsterdam, The Netherlands / Spons. by: ACM SIGSOFT, 285-286, ACM, 2009. | |
| 2008 | |
| DOI | Thomas Noll, Bastian Schlich. Delayed nondeterminism in model checking embedded systems assembly code, Hardware and software: verification and testing : third International Haifa Verification Conference, HVC 2007, Haifa, Israel, October 23 - 25, 2007 ; proceedings / Karen Yorav (ed.), 185-201, Springer, 2008. |
| DOI | Thomas Noll, Stefan Rieger. Verifying Dynamic Pointer-Manipulating Threads, FM 2008: formal methods : 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008 ; proceedings / Jorge Cuellar ... (eds.), 84-99, Springer, 2008. |
| DOI | Stefan Rieger, Thomas Noll. Abstracting Complex Data Structures by Hyperedge Replacement, Graph transformations : 4th International Conference, ICGT 2008, Leicester, United Kingdom, September 7-13, 2008 ; proceedings / Hartmut Ehrig; Reiko Heckel; Grzegorz Rozenberg; Gabriele Taentzer (eds.), 69-83, Springer, 2008. |
| DOI | Gerlind Herberich, Bastian Schlich, Carsten Weise, Thomas Noll. Proving correctness of an efficient abstraction for interrupt handling, 133-150, Elsevier Science, 2008. |
| DOI | Lars Helge Haß, Thomas Noll. Equational Abstractions for Reducing the State Space of Rewrite Theories, 139-154, Elsevier, 2008. |
| 2007 | |
| DOI | Thomas Noll, Stefan Rieger. Composing Transformations to Optimize Linear Code, Theoretical aspects of computing - ICTAC 2007 : 4th international colloquium, Macao, China, September 26-28, 2007 ; proceedings / Cliff B. Jones ... (eds.), 425-439, Springer, 2007. |
| Joost-Pieter Katoen, Thomas Noll, Stefan Rieger. Verifying concurrent list-manipulating programs by LTL model checking, 26 Bl. : graph. Darst., RWTH, Department of Computer Science, 2007. | |
| Joost-Pieter Katoen, Thomas Noll, Stefan Rieger. Verifying concurrent list-manipulating programs by LTL model checking, HAV 2007 : Workshop on Heap Analysis and Verification, March 25, 2007, Braga, Portugal ; [Informal Proceedings], 94-113, 2007. | |
| DOI | Martin R. Neuhäußer, Thomas Noll. Abstraction and model checking of core Erlang programs in Maude, 147-163, Elsevier, 2007. |
| DOI | Holger Blume, Daniel Becker, L. Rotenberg, Martin Botteck, Jörg Brakensiek, Thomas Noll. Hybrid Functional and Instruction-Level Power Modeling for Embedded and Heterogeneous Processor Architectures, 689-702, Elsevier, 2007. |
| 2006 | |
| DOI | Thomas Noll, Chanchal Kumar Roy. Towards automatic verification of Erlang programs by pi-calculus translation, Proceedings of the ACM SIGPLAN Workshop on Generic Programming 2006 : WGP 06, held 16 September 2006, Portland Oregon / ACM SIGPLAN, 38-50, ACM, 2006. |
| DOI | Klaus Indermark, Thomas Noll. Algebraic correctness proofs for compiling recursive function definitions with strictness information, 1-43, Springer, 2006. |
| Thomas Noll, Stefan Rieger. Optimization of straight-line code revisited, GI, 2006. | |
| 2005 | |
| Thomas Noll, Chanchal Kumar Roy. Modeling Erlang in the pi-Calculus, Erlang 05 : proceedings of the ACM SIGPLAN 2005 Erlang Workshop ; September 25, 2005, Tallin, Estonia ; [co-located with the Annual International Conference in Functional Programming (ICFP)] / sponsored by the Association for Computing Machinery, Special Interest Group on Programming Languages (SIGPLAN) / Erlang Workshop ¡4, 2005, Tallinn¿, 72-77, ACM Press, 2005. | |
| Thomas Noll, Chanchal Kumar Roy. Towards automatic verification of Erlang programs by pi-calculus translation, Erlang 05 : proceedings of the ACM SIGPLAN 2005 Erlang Workshop ; September 25, 2005, Tallin, Estonia ; [co-located with the Annual International Conference in Functional Programming (ICFP)] / sponsored by the Association for Computing Machinery, Special Interest Group on Programming Languages (SIGPLAN) / Erlang Workshop ¡4, 2005, Tallinn¿, 38-50, ACM Press, 2005. | |
| DOI | Martin Leucker, Thomas Noll, Perdita Stevens, Michael Weber. Functional programming languages for verification tools : a comparison of ML and Haskell, 184-194, Springer, 2005. |
| 2002 | |
| DOI | Benedikt Bollig, Martin Leucker, Thomas Noll. Generalised regular MSC languages, Foundations of software science and computation structures : 5th international conference ; proceedings / FOSSACS 2002, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8 - 12, 2002. Mogens Nielsen; Uffe Engberg (ed.), 52-66, Springer, 2002. |
| 2001 | |
| . Kolloquium programmiersprachen und Grundlagen der Programmierung ; 11 (Simmerath-Rurberg) : 2001.10.07-11, 128 Bl.. : graph. Darst., RWTH, Department of Computer Science, 2001. | |
| Benedikt Bollig, Martin Leucker, Thomas Noll. Regular MSC languages, RWTH, 2001. | |
| Martin Leucker, Thomas Noll. Truth/SLC : a parallel verification platform for concurrent systems, Computer aided verification : 13th international conference, CAV 2001, Paris, France, July 18 - 22, 2001 ; proceedings / Gérard Berry ... (eds.), 255-259, Springer, 2001. | |
| DOI | Lars-Åke Fredlund, Dilian Gurov, Thomas Noll. Semi-automated verification of Erlang code, Proceedings / 16th Annual International Conference on Automated Software Engineering (ASE 2001) : 26 - 29 November 2001, Loew's Coronado Bay Resort, Coronado Island, San Diego, California / sponsored by IEEE Computer Society Techncial Committee on Software Engineering; ACM SIGSoft; ACM SIGArt, 319-323, IEEE Computer Society, 2001. |
| Thomas Arts, Thomas Noll. Verifying generic Erlang client-server implementations, Implementation of functional languages : 12th international workshop, Aachen, Germany, September 4 - 7, 2000 ; selected papers / IFL 2000. Markus Mohnen; Pieter Koopman (ed.), 37-52, Springer, 2001. | |
| Roland Büschkes, Thomas Noll, Mark Borning. Transaction-based anomaly detection in communication networks, 9th International Conference on Telecommunication Systems - Modeling and Analysis, March, 15 - 18, 2001, Dallas, Texas, USA / sponsored by Edwin L. Cox School of Business, Southern Methodist University ... Conference general chair: Bezalel Gavish, 2001. | |
| DOI | L.-A. Fredlund, D. Gurov, Thomas Noll. The Erlang verification tool, Tools and algorithms for the construction and analysis of systems : 7th international conference ; proceedings / TACAS 2001, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2 - 6, 2001. Tiziana Margaria; Wang Yi (eds.), 582-585, Springer, 2001. |
| DOI | Thomas Noll. A rewriting logic implementation of Erlang, 206-224, Elsevier Science, 2001. |
| 2000 | |
| Thomas Arts, Thomas Noll. Verifying generic Erlang client-server implementations, 26 Bl., RWTH, Fachgruppe Informatik, 2000. | |
| Mads Dam, Thomas Noll. Context-representable processes, Verification of infinite-state systems : 2.-7.4.2000 ; Seminar 00141 / Schloß Dagstuhl Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI) / Bouajjani, A. ... Hrsg, 19-22, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), 2000. | |
| Thomas Arts, Thomas Noll. Verifying generic Erlang Client-Server implementations, Proceedings of the 12. International Workshop on Implementation of Functional Languages : [IFL 2000] ; Aachen, Germany, 4.-7.9.2000 / Mohnen, M. [u.a.] Hrsg, 387-402, RWTH, Fachgruppe Informatik, 2000. | |
| M. Leucker, Thomas Noll. Truth - a real-world application in Haskell; Ed.: Markus Mohnen ..., Proceedings of the 12. International Workshop on Implementation of Functional Languages : [IFL 2000] ; Aachen, Germany, September 4th-7th 2000, 363-380, RWTH Aachen, 2000. | |
| DOI | Thomas Noll, H. Vogler. The universality of higher-order attributed tree transducers, 45-75, Springer, 2000. |
| 1999 | |
| Thomas Noll, Heiko Vogler. On the universality of higher-order attributed tree transducers, 23 S. : graph. Darst., TU, Fak. Informatik, 1999. | |
| Thomas Noll. Kohärenzeigenschaften in termersetzungsbasierten Modellen für verteilte Systeme, 9. Theorietag der GI-Fachgruppe 0.1.5 'Automaten und Formale Sprachen' : Schauenburg-Elmshagen bei Kassel, 27.9.-29.9.1999 / Otto, F. [u.a.] Hrsg, 52-52, GhK, 1999. | |
| Thomas Noll. On coherence properties in term rewriting models of concurrency, CONCUR '99 - Concurrency Theory : 10. International Conference, Eindhoven, The Netherlands, 24.8.-27.8.1999 ; Proceedings / J. C. Baeten, 478-493, Springer, 1999. | |
| Thomas Noll, H. Vogler. On the universality of higher-order attribute grammars, International Workshop Grammers, Automata, and Logic on Graphs and Trees / Vogler, H. Hrsg, Techn. Univ., Fakultät Informatik, 1999. | |
| M. Lange, M. Leucker, Thomas Noll, S. Tobies. Truth - a verification platform for concurrent systems, tool support for system specification, development and verification, Advances in Computing Science - ASIAN '99 : Proceedings / 5. Asian Computing Science Conference, Phuket, Thailand, 10.12.-12.12.1999 / Thiagarajan, P. S. [u.a.] Hrsg, 150-159, Springer, 1999. | |
| DOI | Martin Leucker, Thomas Noll. Rapid prototyping of specification language implementations, Proceedings / IEEE International Workshop on Rapid Systems Prototyping : June 16 - 18, 1999, Clearwater, Florida, USA / sponsored by IEEE Computer Society Technical Committee on Simulation ..., 60-65, IEEE Computer Soc., 1999. |
| 1998 | |
| M. Lange, M. Leucker, Thomas Noll, S. Tobies. Truth. A verification, Platform for Concurrent Systems. Proc. of Tools '98, Christian-Albrechts-Universität, 1998. | |
| Can Adam Albayrak, Thomas Noll. The WHILE hierarchy of program schemes is infinite, Foundations of software science and computation structures : first international conference, FoSSaCS '98, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS '98, Lisbon, Portugal, March 28 - April 4, 1998 ; proceedings / Maurice Nivat (ed.), 35-47, Springer, 1998. | |
| 1996 | |
| Thomas Noll, Stefan Rossmanith. Parallel evaluation of LR-attributed grammars, Proceedings of the Poster Session of CC 96: Intern. Conf. on Compiler Construction, Linköping, 22.-26.4.1996, 105-112, 1996. | |
| 1995 | |
| Thomas Noll. Klassen applikativer Programmschemata und ihre Berechnungsstärke; Als Ms. gedr., II, 154 S. : graph. Darst., Shaker, 1995. | |
| 1993 | |
| A. Kindler, Thomas Noll, B. Steffen. Hierarchical parallelization of imperative programs, Proc. EuroMicro Workshop on Parallel and Distributed Process. 1993, 178-184, 1993. | |
| Thomas Noll. On the first-order equivalence of call-by-name and call-by-value, Workshop Programmiersprachen u. Grundl. d. Programmier. Garmisch-Partenkirchen 1993, 175-186, Univ. der Bundeswehr, 1993. | |
| 1992 | |
| Thomas Noll, H. Vogler. Top-down parsing with simultaneous evaluation of noncircular attribute grammars, 1992. | |
| Show all | |