Publications by Thomas Noll

2020
DOI [bibtex] [issue] Andreas Gerndt, Liana Mikaelyan, Sascha Müller, Thomas Noll. Synthesizing and optimizing FDIR recovery strategies from fault trees, Science of computer programming 196, pages 102478, Elsevier Science, 2020.
arXiv:2006.09040 [bibtex] [issue] Christopher Brix, Thomas Noll. Debona, 2020. https://arxiv.org/abs/2006.09040
2019
DOI [bibtex] [issue] Joost-Pieter Katoen, Martin R. Neuhäußer, Thomas Noll, Tim Felix Lange. IC3 software model checking, International journal on software tools for technology transfer 22 (2), pages 135–161, Springer, 2019.
DOI [bibtex] [issue] Andreas Gerndt, Liana Mikaelyan, Sascha Müller, 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, 37-54, Springer, 2019.
DOI fulltext PDF [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen, Kevin Batz, Thomas Noll. Quantitative separation logic, Proceedings of the ACM on programming languages 3 (POPL), pages 34, ACM, 2019.
2018
DOI [bibtex] [issue] Andreas Gerndt, Sascha Müller, Thomas Noll. Synthesizing Failure Detection, Isolation, and Recovery Strategies from Nondeterministic Dynamic Fault Trees, Journal of Aerospace Information Systems, 2018.
DOI [bibtex] [issue] Christoph Matheja, Florian Zuleger, Jens Katelaan, Thomas Noll. Harrsh, 13th International Workshop on the Implementation of Logics (IWIL 2018), Kalpa Publications in Computing, 23-36, 2018.
DOI [bibtex] [issue] Frederick Prinz, Joost-Pieter Katoen, Martin R. Neuhäußer, Thomas Noll, Tim Lange. Improving Generalization in Software IC3, 23rd International Symposium on Model Checking Software (Spin 2018), LNCS, 85-102, Springer, 2018.
DOI fulltext PDF [bibtex] [issue] Daniel Schemmel, Julian Büning, Klaus Wehrle, Oscar Soria Dustmann, Thomas Noll. Symbolic Liveness Analysis of Real-World Software, 30th International Conference on Computer Aided Verification (CAV 2018), Volume 10982 of LNCS, 447-466, Springer, 2018.
DOI [bibtex] [issue] Christina Jansen, Christoph Matheja, Hannah Arndt, Joost-Pieter Katoen, Thomas Noll. Let this Graph Be Your Witness!, 30th International Conference on Computer Aided Verification (CAV 2018), Volume 10982 of LNCS, 3-11, Springer, 2018.
arXiv:1802.10467 [bibtex] [issue] Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen, Kevin Batz, Thomas Noll. Quantitative Separation Logic, 159 Seiten, 2018. https://arxiv.org/abs/1802.10467
DOI [bibtex] [issue] Christina Jansen, Christoph Matheja, Hannah Arndt, Thomas Noll. Graph-Based Shape Analysis Beyond Context-Freeness, International Conference on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, 271-286, Springer, 2018.
2017
fulltext PDF [bibtex] [issue] Alessandro Cimatti, Harold Yorick Bruintjes, Joost-Pieter Katoen, Marco Bozzano, Stefano Tonetta, Thomas Noll. The COMPASS 3.0 Toolset, 5th International Symposium on Model Based Safety Assessment (IMBSA 2017), 2 Seiten, 2017.
DOI [bibtex] [issue] Christina Jansen, Christoph Matheja, Florian Zuleger, Jens Katelaan, Thomas Noll. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 26th European Symposium on Programming (ESOP 2017), Volume 10201 of LNCS, 611-638, Springer, 2017.
DOI [bibtex] [issue] Andreas Gerndt, Sascha Müller, Thomas Noll. Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees, AIAA Space and Astronautics Forum and Exposition 2017, 1140-1149, Curran Associates, Inc., 2017.
DOI fulltext PDF [bibtex] [issue] Louis Wachtmeister, Thomas Noll. Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications, embeddedworld Exibition & Conference, 5 Seiten, Zenodo, 2017.
DOI [bibtex] [issue] Alessandro Cimatti, Harold Yorick Bruintjes, Joost-Pieter Katoen, Marco Bozzano, Stefano Tonetta, Thomas Noll. Formal Methods for Aerospace Systems, Springer eBook Collection : Computer Science, 133-159, Springer, 2017.
arXiv:1705.03754 [bibtex] [issue] Christina Jansen, Christoph Matheja, Hannah Arndt, Thomas Noll. Heap Abstraction Beyond Context-Freeness, 44 Seiten, 2017. https://arxiv.org/abs/1705.03754
[bibtex] [issue] Makoto Tatsuta, Marieke Huisman, Thomas Noll. Analysis and Verification of Pointer Programs, Volume 2017-04 of NII Shonan Meeting Report, 15 Seiten, National Institute of Informatics, 2017.
2016
arXiv:1610.07041 [bibtex] [issue] Christina Jansen, Christoph Matheja, Florian Zuleger, Jens Katelaan, Thomas Noll. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 115 Seiten, 2016. https://arxiv.org/abs/1610.07041
2015
DOI [bibtex] [issue] Christina Jansen, Christoph Matheja, Thomas Noll. Tree-Like Grammars and Separation Logic, 13th Asian Symposium on Programming Languages and Systems (APLAS 2015), Volume 9458 of LNCS, 90-108, Springer, 2015.
DOI [bibtex] [issue] Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll. Verifying pointer programs using graph grammars, Science of computer programming 97 (1), pages 157-162, Elsevier, 2015.
DOI [bibtex] [issue] Benjamin Bittner, Joost-Pieter Katoen, Thomas Noll, Viet Yen Nguyen. Compositional Analysis Using Component-Oriented Interpolation, International Symposium on Formal Aspects of Component Software (FACS 2014), Volume 8997 of LNCS, 69-85, Springer, 2015.
DOI [bibtex] [issue] Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll. Juggrnaut, Formal methods in system design 47 (2), pages 159-203, Springer, 2015.
[bibtex] [issue] Kevin Van der Pol, Thomas Noll. Security Type Checking for MILS-AADL Specifications, International Workshop on MILS: Architecture and Assurance for Secure Systems, 10 Seiten, 2015.
fulltext PDF [bibtex] [issue] Martin R. Neuhäußer, Thomas Noll, Tim Lange. IC3 Software Model Checking on Control Flow Automata, 15th Conference on Formal Methods in Computer - Aided Design (FMCAD 2015), 97-104, FMCAD Inc, 2015.
[bibtex] [issue] Kevin Van der Pol, Thomas Noll. Security Type Checking for MILS-AADL Specifications, International Workshop on MILS: Architecture and Assurance for Secure Systems, 25 Folien, 2015.
2014
fulltext PDF [bibtex] [issue] Joost-Pieter Katoen, Thomas Noll, Viet Yen Nguyen. Formal Validation Methods in Model-Based Spacecraft Systems Engineering, 340-375, Taylor and Francis, 2014.
DOI [bibtex] [issue] Dimitri Bohlender, Harold Yorick Bruintjes, Jens Katelaan, Sebastian Junges, Thomas Noll, Viet Yen Nguyen. A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models, Volume 8803 of LNCS, 177-192, Springer, 2014.
DOI [bibtex] [issue] Thomas Noll. Safety, Dependability and Performance Analysis of Aerospace Systems, Volume 476 of Communications in Computer and Information Science, 17-31, Springer, 2014.
DOI [bibtex] [issue] Dirk Seifert, Hao Wu, Joost-Pieter Katoen, Thomas Noll, Thomas Santen. Performance Analysis of Computing Servers, Volume 8376 of LNCS, 57-72, Springer, 2014.
DOI [bibtex] [issue] Christina Jansen, Thomas Noll. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs, 8571, 49-64, Springer, 2014.
DOI [bibtex] [issue] Alessandro Cimatti, Bart Postma, Joost-Pieter Katoen, Konstantinos Mokos, Marco Bozzano, Marco Roveri, Panagiotis Katsaros, Thomas Noll, Viet Yen Nguyen. Spacecraft early design validation using formal methods, Reliability engineering & system safety 132, pages 20-35, Elsevier, 2014.
2013
[bibtex] [issue] Dirk Seifert, Hao Wu, Joost-Pieter Katoen, Thomas Noll, Thomas Santen. Model-Based Energy Optimization of Automotive Control Systems, Proceedings of the Conference on Design, Automation and Test in Europe, 761-766, EDA Consortium, 2013.
DOI [bibtex] [issue] Martin R. Neuhäußer, Thomas Noll, Tim Lange. Speeding Up the Safety Verification of Programmable Logic Controller Code, Volume 8244 of LNCS, 44-60, Springer, 2013.
DOI [bibtex] [issue] Christina Jansen, Markus Bals, Thomas Noll. Incremental Construction of Greibach Normal Form for Context-Free Grammars, Proceedings, 165-168, IEEE Computer Society, 2013.
DOI [bibtex] [issue] Bernhard Ern, Thomas Noll, Viet Yen Nguyen. Characterization of Failure Effects on AADL Models, Volume 8153 of LNCS, 241-252, Springer, 2013.
2012
DOI [bibtex] [issue] Thomas Noll. Correctness, Safety and Fault Tolerance in Aerospace Systems, pages 42, Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2012.
DOI [bibtex] [issue] 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, 253-256, IEEE, 2012.
2011
DOI [bibtex] [issue] Alessandro Cimatti, Joost-Pieter Katoen, Marco Bozzano, Marco Roveri, Thomas Noll, Viet Yen Nguyen, Xavier Olive, Yuri Yushtein. System-Software Co-Engineering, Proceedings, Fourth IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT 2011), 18-25, IEEE CS Press, 2011.
DOI [bibtex] [issue] Bastian Schlich, Jörg Brauer, Lucas Brutschy, Thomas Noll. Reduction of Interrupt Handler Executions for Model Checking Embedded Software, Hardware and software, Volume 6405 of LNCS, Springer, 2011.
DOI [bibtex] [issue] 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, 323-335, Springer, 2011.
[bibtex] [issue] Joost-Pieter Katoen, Thomas Noll. Trustworthy Aerospace Systems, Public service review 11, pages 204-205, PS, PublicService.co.uk Ltd, 2011.
2010
DOI [bibtex] [issue] Alessandro Cimatti, Joost-Pieter Katoen, Marco Bozzano, Marco Roveri, Ralf Wimmer, Thomas Noll, Viet Yen Nguyen. A Model Checker for AADL, Computer aided verification (CAV 2010), Volume 6174 of LNCS, 562-565, Springer, 2010.
fulltext PDF [bibtex] [issue] Jörg Brauer, Stefan Kowalewski, Thomas Noll, Volker Kamin. Loop Refinement using Octagons and Satisfiability, SSV'10, 9 S., ACM, 2010.
DOI [bibtex] [issue] Alessandro Cimatti, Joost-Pieter Katoen, Marco Bozzano, Marco Roveri, Thomas Noll, Viet Yen Nguyen. Safety, Dependability, and Performance Analysis of Extended AADL Models, Computer journal 51, Univ. Press, 2010.
DOI [bibtex] [issue] Bastian Schlich, Jörg Brauer, Thomas Noll. 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
DOI [bibtex] [issue] Alessandro Cimatti, Joost-Pieter Katoen, Marco Bozzano, Marco Roveri, Thomas Noll, Viet Yen Nguyen. Codesign of Dependable Systems, Seventh ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 121-130, IEEE, 2009.
DOI [bibtex] [issue] Alessandro Cimatti, Joost-Pieter Katoen, Marco Bozzano, Marco Roveri, Thomas Noll, Viet Yen Nguyen. The COMPASS Approach, Volume 5775 of LNCS, 173-186, Springer, 2009.
fulltext PDF [bibtex] [issue] Alessandro Cimatti, Joost-Pieter Katoen, Marco Bozzano, Marco Roveri, Thomas Noll, Viet Yen Nguyen. Model-Based Codesign of Critical Embedded Systems, Workshop Proceedings / ACES-MB 2009, Volume 507 of CEUR Workshop Proceedings, 87-91, RWTH Aachen, 2009.
[bibtex] [issue] Alessandro Cimatti, Joost-Pieter Katoen, Marco Bozzano, Marco Roveri, Thomas Noll, Viet Yen Nguyen. Verification and Performance Evaluation of AADL Models (Tool Demonstration), ESEC-FSE’09, 285-286, ACM, 2009.
2008
DOI [bibtex] [issue] Bastian Schlich, Carsten Weise, Gerlind Herberich, Thomas Noll. Proving correctness of an efficient abstraction for interrupt handling, Electronic notes in theoretical computer science 217, pages 133-150, Elsevier Science, 2008.
DOI [bibtex] [issue] Lars Helge Haß, Thomas Noll. Equational Abstractions for Reducing the State Space of Rewrite Theories, Electronic notes in theoretical computer science 238 (3), pages 139-154, Elsevier, 2008.
DOI [bibtex] [issue] Stefan Rieger, Thomas Noll. Abstracting Complex Data Structures by Hyperedge Replacement, Graph transformations (ICGT 2008), Volume 5214 of LNCS, 69-83, Springer, 2008.
DOI [bibtex] [issue] Bastian Schlich, Thomas Noll. Delayed nondeterminism in model checking embedded systems assembly code, Volume 4899 of LNCS, 185-201, Springer, 2008.
DOI [bibtex] [issue] Stefan Rieger, Thomas Noll. Verifying Dynamic Pointer-Manipulating Threads, Volume 5014 of LNCS, 84-99, Springer, 2008.
2007
DOI [bibtex] [issue] Stefan Rieger, Thomas Noll. Composing Transformations to Optimize Linear Code, Volume 4711 of LNCS, 425-439, Springer, 2007.
fulltext PDF [bibtex] [issue] Joost-Pieter Katoen, Stefan Rieger, Thomas Noll. Verifying concurrent list-manipulating programs by LTL model checking, HAV 2007, 94-113, 2007.
fulltext PDF [bibtex] [issue] Joost-Pieter Katoen, Stefan Rieger, Thomas Noll. Verifying concurrent list-manipulating programs by LTL model checking, Volume 2007,6 of Aachener Informatik-Berichte, 26 Bl. : graph. Darst., RWTH, Department of Computer Science, 2007.
DOI [bibtex] [issue] Martin R. Neuhäußer, Thomas Noll. Abstraction and model checking of core Erlang programs in Maude, Electronic notes in theoretical computer science 176 (4), pages 147-163, Elsevier, 2007.
2006
fulltext PDF [bibtex] [issue] Stefan Rieger, Thomas Noll. Optimization of straight-line code revisited, Softwaretechnik-Trends 26 (2), GI, 2006.
DOI [bibtex] [issue] Klaus Indermark, Thomas Noll. Algebraic correctness proofs for compiling recursive function definitions with strictness information, Acta informatica 43 (1), pages 1-43, Springer, 2006.
DOI [bibtex] [issue] Chanchal Kumar Roy, Thomas Noll. Towards automatic verification of Erlang programs by pi-calculus translation, Proceedings of the ACM SIGPLAN Workshop on Generic Programming 2006 (WGP 06), 38-50, ACM, 2006.
2005
[bibtex] [issue] Chanchal Kumar Roy, Thomas Noll. Modeling Erlang in the pi-Calculus, Erlang 05, 72-77, ACM Press, 2005.
DOI [bibtex] [issue] Martin Leucker, Michael Weber, Perdita Stevens, Thomas Noll. Functional programming languages for verification tools, International journal on software tools for technology transfer 7 (2), pages 184-194, Springer, 2005.
[bibtex] [issue] Chanchal Kumar Roy, Thomas Noll. Towards automatic verification of Erlang programs by pi-calculus translation, Erlang 05, 38-50, ACM Press, 2005.
2002
DOI [bibtex] [issue] Benedikt Bollig, Martin Leucker, Thomas Noll. Generalised regular MSC languages, Foundations of software science and computation structures, Volume 2303 of LNCS, 52-66, Springer, 2002.
2001
[bibtex] [issue] Thomas Arts, Thomas Noll. Verifying generic Erlang client-server implementations, Implementation of functional languages, Volume 2011 of LNCS, 37-52, Springer, 2001.
DOI [bibtex] [issue] Dilian Gurov, Lars-Åke Fredlund, Thomas Noll. Semi-automated verification of Erlang code, Proceedings / 16th Annual International Conference on Automated Software Engineering (ASE 2001), 319-323, IEEE Computer Society, 2001.
[bibtex] [issue] Martin Leucker, Thomas Noll. Truth/SLC, Computer aided verification (CAV 2001), Volume 2102 of LNCS, 255-259, Springer, 2001.
[bibtex] [issue] Mark Borning, Roland Büschkes, Thomas Noll. 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] [issue] D. Gurov, L.-A. Fredlund, Thomas Noll. The Erlang verification tool, Tools and algorithms for the construction and analysis of systems, Volume 2031 of LNCS, 582-585, Springer, 2001.
DOI [bibtex] [issue] Thomas Noll. A rewriting logic implementation of Erlang, Electronic notes in theoretical computer science 44 (2), pages 206-224, Elsevier Science, 2001.
fulltext PDF [bibtex] [issue] Benedikt Bollig, Martin Leucker, Thomas Noll. Regular MSC languages, Volume 2001,5 of Aachener Informatik-Berichte, RWTH, 2001.
2000
[bibtex] [issue] 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, 387-402, RWTH, Fachgruppe Informatik, 2000.
fulltext PDF [bibtex] [issue] 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, 363-380, RWTH Aachen, 2000.
[bibtex] [issue] Mads Dam, Thomas Noll. Context-representable processes, Volume 271 of Dagstuhl-Seminar-Report, 19-22, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), 2000.
[bibtex] [issue] Thomas Arts, Thomas Noll. Verifying generic Erlang client-server implementations, Volume 2000,08 of Aachener Informatik-Berichte, 26 Bl., RWTH, Fachgruppe Informatik, 2000.
1999
[bibtex] [issue] Heiko Vogler, Thomas Noll. On the universality of higher-order attributed tree transducers, Volume 99/05 of Technische Berichte / Technische Universität Dresden, Fakultät Informatik, 23 S. : graph. Darst., TU, Fak. Informatik, 1999.
DOI [bibtex] [issue] 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, 60-65, IEEE Computer Soc., 1999.