| 2020 |
|---|
[bibtex]
|
Christopher Brix, Thomas Noll. Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs, 2020. arXiv:2006.09040
|
[bibtex]
|
Sascha Müller, Liana Mikaelyan, Andreas Gerndt, Thomas Noll. Synthesizing and optimizing FDIR recovery strategies from fault trees, Science of computer programming 196, pages 102478, 2020.
|
| 2019 |
|---|
|
[bibtex]
|
Tim Felix Lange, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen. IC3 software model checking, International journal on software tools for technology transfer , 2019.
|
|
[bibtex]
|
Liana Mikaelyan, Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing and Optimizing FDIR Recovery Strategies from Fault Trees, 6th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), Volume 1008 of Communications in computer and information science, pages 37-54, Springer, 2019.
|
|
[bibtex]
|
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs, Proceedings of the ACM on programming languages 3 (POPL), pages 34, 2019.
|
| 2018 |
|---|
|
[bibtex]
|
Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing Failure Detection, Isolation, and Recovery Strategies from Nondeterministic Dynamic Fault Trees, Journal of Aerospace Information Systems , 2018.
|
|
[bibtex]
|
Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic, 13th International Workshop on the Implementation of Logics (IWIL 2018), Kalpa Publications in Computing, pages 23-36, 2018.
|
|
[bibtex]
|
Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen. Improving Generalization in Software IC3, 23rd International Symposium on Model Checking Software (Spin 2018), LNCS, pages 85-102, Springer, 2018.
|
|
[bibtex]
|
Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, Klaus Wehrle. Symbolic Liveness Analysis of Real-World Software, 30th International Conference on Computer Aided Verification (CAV 2018), Volume 10982 of LNCS, pages 447-466, Springer, 2018.
|
|
[bibtex]
|
Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Let this Graph Be Your Witness! : An Attestor for Verifying Java Pointer Programs, 30th International Conference on Computer Aided Verification (CAV 2018), Volume 10982 of LNCS, pages 3-11, Springer, 2018.
|
|
[bibtex]
|
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs, 2018. arXiv:1802.10467
|
|
[bibtex]
|
Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Graph-Based Shape Analysis Beyond Context-Freeness, International Conference on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, pages 271-286, Springer, 2018.
|
| 2017 |
|---|
|
[bibtex]
|
Louis Wachtmeister, Thomas Noll. Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications, embeddedworld Exibition & Conference, 5 pages, Zenodo, 2017.
|
|
[bibtex]
|
Christina Jansen. Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic, PhD Thesis, RWTH Aachen University, 286 pages, 2017.
|
|
[bibtex]
|
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 26th European Symposium on Programming (ESOP 2017), Volume 10201 of LNCS, pages 611-638, Springer, 2017.
|
|
[bibtex]
|
Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness, 2017. arXiv:1705.03754
|
|
[bibtex]
|
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, pages 1140-1149, Curran Associates, Inc., 2017.
|
|
[bibtex]
|
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. The COMPASS 3.0 Toolset, 5th International Symposium on Model Based Safety Assessment (IMBSA 2017), 2 pages, 2017.
|
|
[bibtex]
|
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, Springer eBook Collection : Computer Science, pages 133-159, Springer, 2017.
|
|
[bibtex]
|
Marieke Huisman, Thomas Noll, Makoto Tatsuta. Analysis and Verification of Pointer Programs : October 2-5, 2017, Volume 2017-04 of NII Shonan Meeting Report, 15 pages, National Institute of Informatics, 2017.
|
| 2016 |
|---|
|
[bibtex]
|
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 2016. arXiv:1610.07041
|
| 2015 |
|---|
|
[bibtex]
|
Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen, Thomas Noll. Compositional Analysis Using Component-Oriented Interpolation, International Symposium on Formal Aspects of Component Software (FACS 2014), Volume 8997 of LNCS, pages 69-85, Springer, 2015.
|
|
[bibtex]
|
Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Verifying pointer programs using graph grammars, Science of computer programming 97 (1), pages 157-162, 2015.
|
|
[bibtex]
|
Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Juggrnaut: using graph grammars for abstracting unbounded heap structures, Formal methods in system design 47 (2), pages 159-203, 2015.
|
|
[bibtex]
|
Kevin Van der Pol, Thomas Noll. Security Type Checking for MILS-AADL Specifications, International Workshop on MILS: Architecture and Assurance for Secure Systems, pages 25 Folien, 2015.
|
|
[bibtex]
|
Christoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic, 13th Asian Symposium on Programming Languages and Systems (APLAS 2015) (APLAS 2015), Volume 9458 of LNCS, pages 90-108, Springer, 2015.
|
|
[bibtex]
|
Tim Lange, Martin R. Neuhäußer, Thomas Noll. IC3 Software Model Checking on Control Flow Automata, 15th Conference on Formal Methods in Computer - Aided Design (FMCAD 2015), pages 97-104, FMCAD Inc, 2015.
|
|
[bibtex]
|
Kevin Van der Pol, Thomas Noll. Security Type Checking for MILS-AADL Specifications, International Workshop on MILS: Architecture and Assurance for Secure Systems, 10 pages, 2015.
|
| 2014 |
|---|
|
[bibtex]
|
Christina Jansen, Thomas Noll. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs, Graph transformation, LNCS, pages 49-64, Springer, 2014.
|
|
[bibtex]
|
Christina Jansen, Florian Göbe, Thomas Noll. Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs, Graph transformation (ICGT 2014), Volume 8571 of LNCS, pages 65-80, Springer, 2014.
|
|
[bibtex]
|
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, Reliability engineering & system safety 132, pages 20-35, 2014.
|
|
[bibtex]
|
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 (MMB DFT 2014), Volume 8376 of LNCS, pages 57-72, Springer, 2014.
|
|
[bibtex]
|
Thomas Noll. Safety, Dependability and Performance Analysis of Aerospace Systems, Formal Techniques for Safety-Critical Systems (FTSCS 2014), Volume 476 of Communications in Computer and Information Science, pages 17-31, Springer, 2014.
|
|
[bibtex]
|
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 (ISoLA 2014), Volume 8803 of LNCS, pages 177-192, Springer, 2014.
|
|
[bibtex]
|
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, pages 340-375, Taylor and Francis, 2014.
|
| 2013 |
|---|
|
[bibtex]
|
Tim Lange, Martin R. Neuhäußer, Thomas Noll. Speeding Up the Safety Verification of Programmable Logic Controller Code, Hardware and software, Volume 8244 of LNCS, pages 44-60, Springer, 2013.
|
|
[bibtex]
|
Markus Bals, Christina Jansen, Thomas Noll. Incremental Construction of Greibach Normal Form for Context-Free Grammars, Proceedings, pages 165-168, IEEE Computer Society, 2013.
|
|
[bibtex]
|
Bernhard Ern, Viet Yen Nguyen, Thomas Noll. Characterization of Failure Effects on AADL Models, Computer safety, reliability, and security (SAFECOMP 2013), Volume 8153 of LNCS, pages 241-252, Springer, 2013.
|
|
[bibtex]
|
Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu. Model-Based Energy Optimization of Automotive Control Systems, Proceedings of the Conference on Design, Automation and Test in Europe, pages 761-766, EDA Consortium, 2013.
|
| 2012 |
|---|
|
[bibtex]
|
Thomas Noll. Correctness, Safety and Fault Tolerance in Aerospace Systems : The ESA COMPASS Project, Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2012.
|
|
[bibtex]
|
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, pages 253-256, IEEE, 2012.
|
| 2011 |
|---|
|
[bibtex]
|
Bastian Schlich, Thomas Noll, Jörg Brauer, Lucas Brutschy. Reduction of Interrupt Handler Executions for Model Checking Embedded Software, Hardware and software, Volume 6405 of LNCS, Springer, 2011.
|
|
[bibtex]
|
Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll. A Local Greibach Normal Form for Hyperedge Replacement Grammars, Language and automata theory and applications (LATA 2011), Volume 6638 of LNCS, pages 323-335, Springer, 2011.
|
|
[bibtex]
|
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), pages 18-25, IEEE CS Press, 2011.
|
|
[bibtex]
|
Joost-Pieter Katoen, Thomas Noll. Trustworthy Aerospace Systems, Public service review 11, pages 204-205, 2011.
|
| 2010 |
|---|
|
[bibtex]
|
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Safety, Dependability, and Performance Analysis of Extended AADL Models, Computer journal 51, 2010.
|
|
[bibtex]
|
Jörg Brauer, Volker Kamin, Stefan Kowalewski, Thomas Noll. Loop Refinement using Octagons and Satisfiability, SSV'10, pages 9 S., ACM, 2010.
|
|
[bibtex]
|
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer. A Model Checker for AADL, Computer aided verification (CAV 2010), Volume 6174 of LNCS, pages 562-565, Springer, 2010.
|
|
[bibtex]
|
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, ACM Digital Library, ACM, 2010.
|
| 2009 |
|---|
|
[bibtex]
|
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, pages 285-286, ACM, 2009.
|
|
[bibtex]
|
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, Volume 507 of CEUR Workshop Proceedings, pages 87-91, RWTH Aachen, 2009.
|
|
[bibtex]
|
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), pages 121-130, IEEE, 2009.
|
|
[bibtex]
|
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 (SAFECOMP 2009), Volume 5775 of LNCS, pages 173-186, Springer, 2009.
|
| 2008 |
|---|
|
[bibtex]
|
Thomas Noll, Stefan Rieger. Verifying Dynamic Pointer-Manipulating Threads, FM 2008, Volume 5014 of LNCS, pages 84-99, Springer, 2008.
|
|
[bibtex]
|
Thomas Noll, Bastian Schlich. Delayed nondeterminism in model checking embedded systems assembly code, Hardware and software, Volume 4899 of LNCS, pages 185-201, Springer, 2008.
|
|
[bibtex]
|
Lars Helge Haß, Thomas Noll. Equational Abstractions for Reducing the State Space of Rewrite Theories, Electronic notes in theoretical computer science : ENTCS 238 (3), pages 139-154, 2008.
|
|
[bibtex]
|
Stefan Rieger, Thomas Noll. Abstracting Complex Data Structures by Hyperedge Replacement, Graph transformations (ICGT 2008), Volume 5214 of LNCS, pages 69-83, Springer, 2008.
|
|
[bibtex]
|
Gerlind Herberich, Bastian Schlich, Carsten Weise, Thomas Noll. Proving correctness of an efficient abstraction for interrupt handling, Electronic notes in theoretical computer science : ENTCS 217, pages 133-150, 2008.
|
| 2007 |
|---|
|
[bibtex]
|
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, Embedded software design : journal of systems architecture 2007, pages 689-702, 2007.
|
|
[bibtex]
|
Martin R. Neuhäußer, Thomas Noll. Abstraction and model checking of core Erlang programs in Maude, Electronic notes in theoretical computer science : ENTCS 176 (4), pages 147-163, 2007.
|
|
[bibtex]
|
Joost-Pieter Katoen, Thomas Noll, Stefan Rieger. Verifying concurrent list-manipulating programs by LTL model checking, HAV 2007, pages 94-113, 2007.
|
|
[bibtex]
|
Joost-Pieter Katoen, Thomas Noll, Stefan Rieger. Verifying concurrent list-manipulating programs by LTL model checking, Volume 2007,6 of Aachener Informatik-Berichte, pages 26 Bl. : graph. Darst., RWTH, Department of Computer Science, 2007.
|
|
[bibtex]
|
Thomas Noll, Stefan Rieger. Composing Transformations to Optimize Linear Code, Theoretical aspects of computing - ICTAC 2007, Volume 4711 of LNCS, pages 425-439, Springer, 2007.
|
| 2006 |
|---|
|
[bibtex]
|
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), pages 38-50, ACM, 2006.
|
|
[bibtex]
|
Thomas Noll, Stefan Rieger. Optimization of straight-line code revisited, Softwaretechnik-Trends 26 (2), 2006.
|
|
[bibtex]
|
Klaus Indermark, Thomas Noll. Algebraic correctness proofs for compiling recursive function definitions with strictness information, Acta informatica 43 (1), pages 1-43, 2006.
|
| 2005 |
|---|
|
[bibtex]
|
Martin Leucker, Thomas Noll, Perdita Stevens, Michael Weber. Functional programming languages for verification tools : a comparison of ML and Haskell, International journal on software tools for technology transfer : STTT 7 (2), pages 184-194, 2005.
|
|
[bibtex]
|
Thomas Noll, Chanchal Kumar Roy. Towards automatic verification of Erlang programs by pi-calculus translation, Erlang 05, pages 38-50, ACM Press, 2005.
|
|
[bibtex]
|
Thomas Noll, Chanchal Kumar Roy. Modeling Erlang in the pi-Calculus, Erlang 05, pages 72-77, ACM Press, 2005.
|
| 2002 |
|---|
|
[bibtex]
|
Benedikt Bollig, Martin Leucker, Thomas Noll. Generalised regular MSC languages, Foundations of software science and computation structures, Volume 2303 of LNCS, pages 52-66, Springer, 2002.
|
| 2001 |
|---|
|
[bibtex]
|
Lars-Åke Fredlund, Dilian Gurov, Thomas Noll. Semi-automated verification of Erlang code, Proceedings / 16th Annual International Conference on Automated Software Engineering (ASE 2001), pages 319-323, IEEE Computer Society, 2001.
|
|
[bibtex]
|
Klaus Indermark, Thomas Noll. Kolloquium programmiersprachen und Grundlagen der Programmierung ; 11 (Simmerath-Rurberg) : 2001.10.07-11, Volume 2001,11 of Aachener Informatik-Berichte, pages 128 Bl.. : graph. Darst., RWTH, Department of Computer Science, 2001.
|
|
[bibtex]
|
Benedikt Bollig, Martin Leucker, Thomas Noll. Regular MSC languages, Volume 2001,5 of Aachener Informatik-Berichte, RWTH, 2001.
|
|
[bibtex]
|
Martin Leucker, Thomas Noll. Truth/SLC : a parallel verification platform for concurrent systems, Computer aided verification (CAV 2001), Volume 2102 of LNCS, pages 255-259, Springer, 2001.
|
|
[bibtex]
|
Thomas Arts, Thomas Noll. Verifying generic Erlang client-server implementations, Implementation of functional languages, Volume 2011 of LNCS, pages 37-52, Springer, 2001.
|
|
[bibtex]
|
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, 2001.
|
|
[bibtex]
|
L.-A. Fredlund, D. Gurov, Thomas Noll. The Erlang verification tool, Tools and algorithms for the construction and analysis of systems, Volume 2031 of LNCS, pages 582-585, Springer, 2001.
|
|
[bibtex]
|
Thomas Noll. A rewriting logic implementation of Erlang, Electronic notes in theoretical computer science : ENTCS 44 (2), pages 206-224, 2001.
|
| 2000 |
|---|
|
[bibtex]
|
M. Leucker, Thomas Noll. Truth - a real-world application in Haskell, Proceedings of the 12. International Workshop on Implementation of Functional Languages, Volume 2000,07 of Aachener Informatik-Berichte, pages 363-380, RWTH Aachen, 2000.
|
|
[bibtex]
|
Thomas Arts, Thomas Noll. Verifying generic Erlang Client-Server implementations, Proceedings of the 12. International Workshop on Implementation of Functional Languages, Volume 2000,07 of Aachener Informatik-Berichte, pages 387-402, RWTH, Fachgruppe Informatik, 2000.
|
|
[bibtex]
|
Mads Dam, Thomas Noll. Context-representable processes, Verification of infinite-state systems, Volume 271 of Dagstuhl-Seminar-Report, pages 19-22, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), 2000.
|
|
[bibtex]
|
Thomas Arts, Thomas Noll. Verifying generic Erlang client-server implementations, Volume 2000,08 of Aachener Informatik-Berichte, pages 26 Bl., RWTH, Fachgruppe Informatik, 2000.
|
| 1999 |
|---|
|
[bibtex]
|
Martin Leucker, Thomas Noll. Rapid prototyping of specification language implementations, Proceedings / IEEE International Workshop on Rapid Systems Prototyping, IEEE / IFIP International Symposium on Rapid System Prototyping. Proceedings, pages 60-65, IEEE Computer Soc., 1999.
|
|
[bibtex]
|
Thomas Noll, Heiko Vogler. On the universality of higher-order attributed tree transducers, Volume 99/05 of Technische Berichte / Technische Universität Dresden, Fakultät Informatik, pages 23 S. : graph. Darst., TU, Fak. Informatik, 1999.
|
| 1998 |
|---|
|
[bibtex]
|
Can Adam Albayrak, Thomas Noll. The WHILE hierarchy of program schemes is infinite, Foundations of software science and computation structures, Volume 1378 of LNCS, pages 35-47, Springer, 1998.
|
|
[bibtex]
|
M. Lange, M. Leucker, Thomas Noll, S. Tobies. Truth. A verification, Platform for Concurrent Systems. Proc. of Tools '98, Volume 98,03 of Bericht / Institut für Informatik und Praktische Mathematik der Christian-Albrechts-Universität zu Kiel, Christian-Albrechts-Universität, 1998.
|
| 1996 |
|---|
|
[bibtex]
|
Thomas Noll, Stefan Rossmanith. Parallel evaluation of LR-attributed grammars, pages 105-112, 1996.
|
[bibtex]
[bibtex]