Publications by Thomas Noll

2023
DOI fulltext PDF [bibtex]
@proceedings{KPGP2023,
title = {22. Kolloquium Programmiersprachen und Grundlagen der Programmierung},
author = {},
editor = {Thomas Noll and Ira Justus Fesefeldt},
publisher = {RWTH Aachen University, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {AIB-2023-03},
pages = {1 Online-Ressource},
type = {Proceeding Article},
year = {2023},
doi = {10.18154/RWTH-2023-10034},
url = { https://publications.rwth-aachen.de/record/972197},
}×
[issue] 		Thomas Noll (ed), Ira Justus Fesefeldt (ed). 22. Kolloquium Programmiersprachen und Grundlagen der Programmierung, Volume AIB-2023-03 of Aachener Informatik-Berichte, 1 Online-Ressource, RWTH Aachen University, Department of Computer Science, 2023.
2022
DOI fulltext PDF [bibtex]
@conference{FECQSL2022,
title = {Foundations for Entailment Checking in Quantitative Separation Logic},
author = {Kevin Batz and Ira Justus Fesefeldt and Marvin Jansen and Joost-Pieter Katoen and Florian Keßler and Christoph Matheja and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {13240},
pages = {57-84},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-99336-8_3},
url = { https://publications.rwth-aachen.de/record/843799},
}×
[issue] 		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, 31. European Symposium on Programming (ESOP 2022), Volume 13240 of LNCS, 57-84, Springer, 2022.
fulltext PDF [bibtex]
@article{EDPIK2022,
title = {Einblick DZSF-Projekt "Identifikation von Kapazitätsengpässen"},
author = {Simon Schotten and Thorsten Büker and Wiebke Lenze and Bastian Kogel and Thomas Noll and Mario Fietze and Jana Berger},
publisher = {DVV Media Group, Eurailpress},
journal = {Eisenbahntechnische Rundschau},
volume = {71(5)},
pages = {pages 33-37},
type = {Journal Article},
year = {2022},
url = { https://publications.rwth-aachen.de/record/847020},
}×
[issue] 		Simon Schotten, Thorsten Büker, Wiebke Lenze, Bastian Kogel, Thomas Noll, Mario Fietze, Jana Berger. Einblick DZSF-Projekt "Identifikation von Kapazitätsengpässen", Eisenbahntechnische Rundschau 71 (5), pages 33-37, DVV Media Group, Eurailpress, 2022.
DOI fulltext PDF [bibtex]
@conference{TCQSL2022,
title = {Towards Concurrent Quantitative Separation Logic},
author = {Ira Justus Fesefeldt and Joost-Pieter Katoen and Thomas Noll},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
booktitle = {LIPIcs - Leibniz International Proceedings in Informatics},
volume = {243},
pages = {25:1-25:24},
type = {Conference Paper},
year = {2022},
doi = {10.4230/LIPICS.CONCUR.2022.25},
url = { https://publications.rwth-aachen.de/record/853299},
}×
[issue] 		Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll. Towards Concurrent Quantitative Separation Logic, 33. International Conference on Concurrency Theory (CONCUR 2022), Volume 243 of LIPIcs - Leibniz International Proceedings in Informatics, 25:1-25:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
DOI arXiv:2207.02822 fulltext PDF [bibtex]
@unpublished{TCQSL2022,
title = {Towards Concurrent Quantitative Separation Logic},
author = {Ira Justus Fesefeldt and Joost-Pieter Katoen and Thomas Noll},
pages = {[1]-62},
type = {Preprint},
year = {2022},
doi = {10.48550/ARXIV.2207.02822},
url = { https://arxiv.org/abs/2207.02822},
}×
[issue] 		Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll. Towards Concurrent Quantitative Separation Logic, [1]-62, 2022. https://arxiv.org/abs/2207.02822
DOI [bibtex]
@conference{ACBRIEM2022,
title = {Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining},
author = {Philipp Berger and Wiebke Lenze and Thomas Noll and Simon Schotten and Thorsten Büker and Mario Fietze and Bastian Kogel},
publisher = {Springer},
booktitle = {LNCS},
volume = {13487},
pages = {121-133},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-15008-1_9},
url = { https://publications.rwth-aachen.de/record/854106},
}×
[issue] 		Philipp Berger, Wiebke Lenze, Thomas Noll, Simon Schotten, Thorsten Büker, Mario Fietze, Bastian Kogel. Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining, 27. International Conference Formal Methods for Industrial Critical Systems (FMICS 2022), Volume 13487 of LNCS, 121-133, Springer, 2022.
DOI [bibtex]
@conference{IBRI2022,
title = {Identification of Bottlenecks in Rail Infrastructure},
author = {Wiebke Lenze and Bastian Kogel and Simon Schotten and Thorsten Büker and Thomas Noll and Philipp Berger and Mario Fietze},
publisher = {Civil-Comp Press},
booktitle = {Civil-Comp Conferences},
pages = {23.12},
type = {Conference Paper},
year = {2022},
doi = {10.4203/ccc.1.23.12},
url = { https://publications.rwth-aachen.de/record/961091},
}×
[issue] 		Wiebke Lenze, Bastian Kogel, Simon Schotten, Thorsten Büker, Thomas Noll, Philipp Berger, Mario Fietze. Identification of Bottlenecks in Rail Infrastructure, 5. International Conference on Railway Technology: Research, Development and Maintenance, Civil-Comp Conferences, 23.12, Civil-Comp Press, 2022.
2021
DOI [bibtex]
@conference{ACCBCHRG2021,
title = {Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars},
author = {Ira Justus Fesefeldt and Christoph Matheja and Thomas Noll and Johannes Schulte},
publisher = {Springer},
booktitle = {LNCS},
volume = {12741},
pages = {283-293},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-78946-6_15},
url = { https://publications.rwth-aachen.de/record/820755},
}×
[issue] 		Ira Justus Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte. Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars, 14. International Conference on Graph Transformation (ICGT21), Volume 12741 of LNCS, 283-293, Springer, 2021.
DOI [bibtex]
@conference{AMANDFT2021,
title = {A Modular Approach to Non-deterministic Dynamic Fault Trees},
author = {Sascha Müller and Adeline Jordon and Andreas Gerndt and Thomas Noll},
publisher = {Springer},
booktitle = {Programming and Software Engineering},
volume = {12852},
pages = {243-257},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-83903-1_16},
url = { https://publications.rwth-aachen.de/record/835216},
}×
[issue] 		Sascha Müller, Adeline Jordon, Andreas Gerndt, Thomas Noll. A Modular Approach to Non-deterministic Dynamic Fault Trees, 40. International Conference on Computer Safety, Reliability and Security (SAFECOMP 2021), Volume 12852 of Programming and Software Engineering, 243-257, Springer, 2021.
DOI [bibtex]
@conference{ADPP2021,
title = {A Debugger for Probabilistic Programs},
author = {Alexander Hoppen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {13085},
pages = {282-289},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-92124-8_16},
url = { https://publications.rwth-aachen.de/record/836481},
}×
[issue] 		Alexander Hoppen, Thomas Noll. A Debugger for Probabilistic Programs, 19. International Conference on Software Engineering and Formal Methods (SEFM 2021), Volume 13085 of LNCS, 282-289, Springer, 2021.
2020
DOI arXiv:2006.09040 [bibtex]
@unpublished{DDBNATBFARP2020,
title = {Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs},
author = {Christopher Jan-Steffen Brix and Thomas Noll},
pages = {12 Seiten},
type = {Preprint},
year = {2020},
doi = {10.48550/ARXIV.2006.09040},
url = { https://arxiv.org/abs/2006.09040},
}×
[issue] 		Christopher Jan-Steffen Brix, Thomas Noll. Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs, 12 Seiten, 2020. https://arxiv.org/abs/2006.09040
DOI fulltext PDF [bibtex]
@article{SF2020,
title = {Synthesizing and optimizing FDIR recovery strategies from fault trees},
author = {Sascha Müller and Liana Mikaelyan and Andreas Gerndt and Thomas Noll},
publisher = {Elsevier Science},
journal = {Science of computer programming},
volume = {196},
pages = {pages 102478},
type = {Journal Article},
year = {2020},
doi = {10.1016/j.scico.2020.102478},
url = { https://publications.rwth-aachen.de/record/796082},
}×
[issue] 		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, Elsevier Science, 2020.
2019
DOI fulltext PDF [bibtex]
@article{Q2019,
title = {Quantitative separation logic: a logic for reasoning about probabilistic pointer programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {3(POPL)},
pages = {pages 34},
type = {Journal Article},
year = {2019},
doi = {10.1145/3290347},
url = { https://publications.rwth-aachen.de/record/753722},
}×
[issue] 		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, ACM, 2019.
DOI [bibtex]
@conference{SOFRSFT2019,
title = {Synthesizing and Optimizing FDIR Recovery Strategies from Fault Trees},
author = {Liana Mikaelyan and Sascha Müller and Andreas Gerndt and Thomas Noll},
publisher = {Springer},
booktitle = {Communications in computer and information science},
volume = {1008},
pages = {37-54},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-12988-0_3},
url = { https://publications.rwth-aachen.de/record/759164},
}×
[issue] 		Liana Mikaelyan, Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing and Optimizing FDIR Recovery Strategies from Fault Trees, 6. International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), Volume 1008 of Communications in computer and information science, 37-54, Springer, 2019.
DOI [bibtex]
@article{I2019,
title = {IC3 software model checking},
author = {Tim Felix Lange and Martin R. Neuhäußer and Thomas Noll and Joost-Pieter Katoen},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {22(2)},
pages = {pages 135-161},
type = {Journal Article},
year = {2019},
doi = {10.1007/s10009-019-00547-x},
url = { https://publications.rwth-aachen.de/record/772976},
}×
[issue] 		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 22 (2), pages 135-161, Springer, 2019.
DOI fulltext PDF [bibtex]
@conference{C2019,
title = {COMPASS 3.0},
author = {Marco Bozzano and Harold Yorick Bruintjes and Alessandro Cimatti and Joost-Pieter Katoen and Thomas Noll and Stefano Tonetta},
publisher = {Springer},
booktitle = {LNCS},
volume = {11427},
pages = {379-385},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-17462-0_25},
url = { https://publications.rwth-aachen.de/record/860910},
}×
[issue] 		Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. COMPASS 3.0, 25. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Volume 11427 of LNCS, 379-385, Springer, 2019.
2018
DOI [bibtex]
@conference{GBSABCF2018,
title = {Graph-Based Shape Analysis Beyond Context-Freeness},
author = {Hannah Arndt and Christina Jansen and Christoph Matheja and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {10886},
pages = {271-286},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-92970-5_17},
url = { https://publications.rwth-aachen.de/record/748905},
}×
[issue] 		Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Graph-Based Shape Analysis Beyond Context-Freeness, 16. International Conference on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, 271-286, Springer, 2018.
DOI arXiv:1802.10467 [bibtex]
@unpublished{QSLALRPP2018,
title = {Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
pages = {159 Seiten},
type = {Preprint},
year = {2018},
doi = {10.48550/ARXIV.1802.10467},
url = { https://arxiv.org/abs/1802.10467},
}×
[issue] 		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. https://arxiv.org/abs/1802.10467
DOI [bibtex]
@conference{LGBYWAAVJPP2018,
title = {Let this Graph Be Your Witness!: An Attestor for Verifying Java Pointer Programs},
author = {Hannah Arndt and Christina Jansen and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {10982},
pages = {3-11},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-96142-2_1},
url = { https://publications.rwth-aachen.de/record/753069},
}×
[issue] 		Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Let this Graph Be Your Witness!: An Attestor for Verifying Java Pointer Programs, 30. International Conference on Computer Aided Verification (CAV 2018), Volume 10982 of LNCS, 3-11, Springer, 2018.
DOI fulltext PDF [bibtex]
@conference{SLARWS2018,
title = {Symbolic Liveness Analysis of Real-World Software},
author = {Daniel Schemmel and Julian Büning and Oscar Soria Dustmann and Thomas Noll and Klaus Wehrle},
publisher = {Springer},
booktitle = {LNCS},
volume = {10982},
pages = {447-466},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-96142-2_27},
url = { https://publications.rwth-aachen.de/record/753070},
}×
[issue] 		Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, Klaus Wehrle. Symbolic Liveness Analysis of Real-World Software, 30. International Conference on Computer Aided Verification (CAV 2018), Volume 10982 of LNCS, 447-466, Springer, 2018.
DOI [bibtex]
@conference{IGSI2018,
title = {Improving Generalization in Software IC3},
author = {Tim Lange and Frederick Prinz and Martin R. Neuhäußer and Thomas Noll and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
pages = {85-102},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-94111-0_5},
url = { https://publications.rwth-aachen.de/record/753079},
}×
[issue] 		Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen. Improving Generalization in Software IC3, 23. International Symposium on Model Checking Software (Spin 2018), LNCS, 85-102, Springer, 2018.
DOI [bibtex]
@conference{HATURSHSL2018,
title = {Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic},
author = {Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger},
publisher = {EasyChair},
booktitle = {EPiC series in computing},
volume = {57},
pages = {23-36},
type = {Conference Paper},
year = {2018},
doi = {10.29007/qwd8},
url = { https://publications.rwth-aachen.de/record/753090},
}×
[issue] 		Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic, 13. International Workshop on the Implementation of Logics (IWIL 2018), Volume 57 of EPiC series in computing, 23-36, EasyChair, 2018.
DOI [bibtex]
@article{SFDIRSNDFT2018,
title = {Synthesizing Failure Detection, Isolation, and Recovery Strategies from Nondeterministic Dynamic Fault Trees},
author = {Sascha Müller and Andreas Gerndt and Thomas Noll},
journal = {Journal of Aerospace Information Systems},
type = {Journal Article},
year = {2018},
doi = {10.2514/1.I010669},
url = { https://publications.rwth-aachen.de/record/753091},
}×
[issue] 		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.
2017
DOI [bibtex]
@conference{URRPSHSL2017,
title = {Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic},
author = {Christina Jansen and Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger},
publisher = {Springer},
booktitle = {LNCS},
volume = {10201},
pages = {611-638},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-662-54434-1_23},
url = { https://publications.rwth-aachen.de/record/713570},
}×
[issue] 		Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 26. European Symposium on Programming (ESOP 2017), Volume 10201 of LNCS, 611-638, Springer, 2017.
DOI fulltext PDF [bibtex]
@conference{ACMIFMAS2017,
title = {Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications},
author = {Louis Wachtmeister and Thomas Noll},
publisher = {Zenodo},
pages = {5 Seiten},
type = {Conference Paper},
year = {2017},
doi = {10.5281/zenodo.571173},
url = { https://publications.rwth-aachen.de/record/713571},
}×
[issue] 		Louis Wachtmeister, Thomas Noll. Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications, embeddedworld Exibition & Conference, 5 Seiten, Zenodo, 2017.
DOI [bibtex]
@conference{SFRSNDDFT2017,
title = {Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees},
author = {Sascha Müller and Andreas Gerndt and Thomas Noll},
publisher = {Curran Associates, Inc.},
pages = {1140-1149},
type = {Conference Paper},
year = {2017},
doi = {10.2514/6.2017-5163},
url = { https://publications.rwth-aachen.de/record/713575},
}×
[issue] 		Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees, AIAA Space and Astronautics Forum and Exposition, 1140-1149, Curran Associates, Inc., 2017.
fulltext PDF [bibtex]
@conference{TCT2017,
title = {The COMPASS 3.0 Toolset},
author = {Marco Bozzano and Harold Yorick Bruintjes and Alessandro Cimatti and Joost-Pieter Katoen and Thomas Noll and Stefano Tonetta},
pages = {2 Seiten},
type = {Conference Talk},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713576},
}×
[issue] 		Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. The COMPASS 3.0 Toolset, 5. International Symposium on Model Based Safety Assessment (IMBSA 2017), 2 Seiten, 2017.
DOI [bibtex]
@inbook{FMASAC2017,
title = {Formal Methods for Aerospace Systems: Achievements and Challenges},
author = {Marco Bozzano and Harold Yorick Bruintjes and Alessandro Cimatti and Joost-Pieter Katoen and Thomas Noll and Stefano Tonetta},
publisher = {Springer},
booktitle = {Springer eBook Collection : Computer Science},
pages = {133-159},
type = {Book Chapter},
year = {2017},
doi = {10.1007/978-981-10-4436-6_6},
url = { https://publications.rwth-aachen.de/record/713628},
}×
[issue] 		Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. Formal Methods for Aerospace Systems: Achievements and Challenges, Springer eBook Collection : Computer Science, 133-159, Springer, 2017.
[bibtex]
@techreport{AVPP2017,
title = {Analysis and Verification of Pointer Programs},
author = {Marieke Huisman and Thomas Noll and Makoto Tatsuta},
publisher = {National Institute of Informatics},
booktitle = {NII Shonan Meeting Report},
volume = {2017-04},
pages = {15 Seiten},
type = {Tech Report},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713633},
}×
[issue] 		Marieke Huisman, Thomas Noll, Makoto Tatsuta. Analysis and Verification of Pointer Programs, Volume 2017-04 of NII Shonan Meeting Report, 15 Seiten, National Institute of Informatics, 2017.
DOI arXiv:1705.03754 [bibtex]
@unpublished{HABCF2017,
title = {Heap Abstraction Beyond Context-Freeness},
author = {Hannah Arndt and Christina Jansen and Christoph Matheja and Thomas Noll},
pages = {44 Seiten},
type = {Preprint},
year = {2017},
doi = {10.48550/ARXIV.1705.03754},
url = { https://arxiv.org/abs/1705.03754},
}×
[issue] 		Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness, 44 Seiten, 2017. https://arxiv.org/abs/1705.03754
2016
DOI arXiv:1610.07041 [bibtex]
@unpublished{URRPSHSL2016,
title = {Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic},
author = {Christina Jansen and Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger},
pages = {115 Seiten},
type = {Preprint},
year = {2016},
doi = {10.48550/ARXIV.1610.07041},
url = { https://arxiv.org/abs/1610.07041},
}×
[issue] 		Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic, 115 Seiten, 2016. https://arxiv.org/abs/1610.07041
2015
DOI [bibtex]
@article{V2015,
title = {Verifying pointer programs using graph grammars},
author = {Jonathan Heinen and Christina Jansen and Joost-Pieter Katoen and Thomas Noll},
publisher = {Elsevier},
journal = {Science of computer programming},
volume = {97(1)},
pages = {pages 157-162},
type = {Journal Article},
year = {2015},
doi = {10.1016/j.scico.2013.11.012},
url = { https://publications.rwth-aachen.de/record/459638},
}×
[issue] 		Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Verifying pointer programs using graph grammars, Science of computer programming 97 (1), pages 157-162, Elsevier, 2015.
DOI [bibtex]
@article{J2015,
title = {Juggrnaut: using graph grammars for abstracting unbounded heap structures},
author = {Jonathan Heinen and Christina Jansen and Joost-Pieter Katoen and Thomas Noll},
publisher = {Springer},
journal = {Formal methods in system design},
volume = {47(2)},
pages = {pages 159-203},
type = {Journal Article},
year = {2015},
doi = {10.1007/s10703-015-0236-1},
url = { https://publications.rwth-aachen.de/record/571616},
}×
[issue] 		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, Springer, 2015.
DOI [bibtex]
@conference{CAUCOI2015,
title = {Compositional Analysis Using Component-Oriented Interpolation},
author = {Viet Yen Nguyen and Benjamin Bittner and Joost-Pieter Katoen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {8997},
pages = {69-85},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-15317-9_5},
url = { https://publications.rwth-aachen.de/record/571619},
}×
[issue] 		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, 69-85, Springer, 2015.
DOI [bibtex]
@conference{TLGSL2015,
title = {Tree-Like Grammars and Separation Logic},
author = {Christoph Matheja and Christina Jansen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {9458},
pages = {90-108},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-26529-2_6},
url = { https://publications.rwth-aachen.de/record/571620},
}×
[issue] 		Christoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic, 13. Asian Symposium on Programming Languages and Systems (APLAS 2015), Volume 9458 of LNCS, 90-108, Springer, 2015.
[bibtex]
@conference{STCMAS2015,
title = {Security Type Checking for MILS-AADL Specifications},
author = {Kevin Van der Pol and Thomas Noll},
pages = {10 Seiten},
type = {Conference Paper},
year = {2015},
url = { https://publications.rwth-aachen.de/record/571625},
}×
[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]
@conference{ISMCCFA2015,
title = {IC3 Software Model Checking on Control Flow Automata},
author = {Tim Lange and Martin R. Neuhäußer and Thomas Noll},
publisher = {FMCAD Inc},
pages = {97-104},
type = {Conference Paper},
year = {2015},
url = { https://publications.rwth-aachen.de/record/571629},
}×
[issue] 		Tim Lange, Martin R. Neuhäußer, Thomas Noll. IC3 Software Model Checking on Control Flow Automata, 15. Conference on Formal Methods in Computer - Aided Design (FMCAD 2015), 97-104, FMCAD Inc, 2015.
[bibtex]
@conference{STCMAS2015,
title = {Security Type Checking for MILS-AADL Specifications},
author = {Kevin Van der Pol and Thomas Noll},
pages = {25 Folien},
type = {Conference Talk},
year = {2015},
url = { https://publications.rwth-aachen.de/record/571756},
}×
[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
DOI [bibtex]
@article{S2014,
title = {Spacecraft early design validation using formal methods},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Panagiotis Katsaros and Konstantinos Mokos and Viet Yen Nguyen and Thomas Noll and Bart Postma and Marco Roveri},
publisher = {Elsevier},
journal = {Reliability engineering & system safety},
volume = {132},
pages = {pages 20-35},
type = {Journal Article},
year = {2014},
doi = {10.1016/j.ress.2014.07.003},
url = { https://publications.rwth-aachen.de/record/445610},
}×
[issue] 		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, Elsevier, 2014.
DOI [bibtex]
@conference{GAGBPSPP2014,
title = {Generating Abstract Graph-Based Procedure Summaries for Pointer Programs},
author = {Christina Jansen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
pages = {49-64},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-09108-2_4},
url = { https://publications.rwth-aachen.de/record/465755},
}×
[issue] 		Christina Jansen, Thomas Noll. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs, Graph transformation, LNCS, 49-64, Springer, 2014.
DOI [bibtex]
@conference{PACSG2014,
title = {Performance Analysis of Computing Servers: a case study exploiting a new GSPN semantics},
author = {Joost-Pieter Katoen and Thomas Noll and Thomas Santen and Dirk Seifert and Hao Wu},
publisher = {Springer},
booktitle = {LNCS},
volume = {8376},
pages = {57-72},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-05359-2_5},
url = { https://publications.rwth-aachen.de/record/465758},
}×
[issue] 		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, 57-72, Springer, 2014.
DOI [bibtex]
@conference{SDPAAS2014,
title = {Safety, Dependability and Performance Analysis of Aerospace Systems},
author = {Thomas Noll},
publisher = {Springer},
booktitle = {Communications in Computer and Information Science},
volume = {476},
pages = {17-31},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-17581-2_2},
url = { https://publications.rwth-aachen.de/record/465761},
}×
[issue] 		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, 17-31, Springer, 2014.
DOI [bibtex]
@conference{ARSMCPRTSM2014,
title = {A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models},
author = {Dimitri Bohlender and Harold Yorick Bruintjes and Sebastian Junges and Jens Katelaan and Viet Yen Nguyen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {8803},
pages = {177-192},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-662-45231-8_13},
url = { https://publications.rwth-aachen.de/record/465766},
}×
[issue] 		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, 177-192, Springer, 2014.
fulltext PDF [bibtex]
@inbook{FVMMBSSE2014,
title = {Formal Validation Methods in Model-Based Spacecraft Systems Engineering},
author = {Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll},
publisher = {Taylor and Francis},
pages = {340-375},
type = {Book Chapter},
year = {2014},
url = { https://publications.rwth-aachen.de/record/465771},
}×
[issue] 		Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. Formal Validation Methods in Model-Based Spacecraft Systems Engineering, 340-375, Taylor and Francis, 2014.
2013
DOI [bibtex]
@conference{MBEOACS2013,
title = {Model-Based Energy Optimization of Automotive Control Systems},
author = {Joost-Pieter Katoen and Thomas Noll and Thomas Santen and Dirk Seifert and Hao Wu},
publisher = {IEEE},
pages = {761-766},
type = {Conference Paper},
year = {2013},
doi = {10.7873/date.2013.162},
url = { https://publications.rwth-aachen.de/record/225824},
}×
[issue] 		Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu. Model-Based Energy Optimization of Automotive Control Systems, 16. Design, Automation & Test in Europe Conference & Exhibition (DATE 2013), 761-766, IEEE, 2013.
DOI [bibtex]
@conference{CFEAM2013,
title = {Characterization of Failure Effects on AADL Models},
author = {Bernhard Ern and Viet Yen Nguyen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {8153},
pages = {241-252},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-40793-2_22},
url = { https://publications.rwth-aachen.de/record/227570},
}×
[issue] 		Bernhard Ern, Viet Yen Nguyen, Thomas Noll. Characterization of Failure Effects on AADL Models, Computer safety, reliability, and security : 32. International Conference (SAFECOMP 2013), Volume 8153 of LNCS, 241-252, Springer, 2013.
DOI [bibtex]
@conference{ICGNFCFG2013,
title = {Incremental Construction of Greibach Normal Form for Context-Free Grammars},
author = {Markus Bals and Christina Jansen and Thomas Noll},
publisher = {IEEE Computer Society},
pages = {165-168},
type = {Conference Paper},
year = {2013},
doi = {10.1109/TASE.2013.42},
url = { https://publications.rwth-aachen.de/record/228042},
}×
[issue] 		Markus Bals, Christina Jansen, Thomas Noll. Incremental Construction of Greibach Normal Form for Context-Free Grammars, 2013 International Symposium on Theoretical Aspects of Software Engineering, 165-168, IEEE Computer Society, 2013.
DOI [bibtex]
@conference{SUSVPLCC2013,
title = {Speeding Up the Safety Verification of Programmable Logic Controller Code},
author = {Tim Lange and Martin R. Neuhäußer and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {8244},
pages = {44-60},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-319-03077-7_4},
url = { https://publications.rwth-aachen.de/record/228141},
}×
[issue] 		Tim Lange, Martin R. Neuhäußer, Thomas Noll. Speeding Up the Safety Verification of Programmable Logic Controller Code, 9. International Haifa Verification Conference (HVC 2013), Volume 8244 of LNCS, 44-60, Springer, 2013.
2012
DOI [bibtex]
@conference{ANAMTBPC2012,
title = {A Native Approach to Modeling Timed Behavior in the Pi-Calculus},
author = {Kamal Barakat and Stefan Kowalewski and Thomas Noll},
publisher = {IEEE},
pages = {253-256},
type = {Conference Paper},
year = {2012},
doi = {10.1109/TASE.2012.27},
url = { https://publications.rwth-aachen.de/record/129606},
}×
[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.
DOI [bibtex]
@misc{CSFTASTECP2012,
title = {Correctness, Safety and Fault Tolerance in Aerospace Systems: The ESA COMPASS Project},
author = {Thomas Noll},
publisher = {Schloss Dagstuhl, Leibniz-Zentrum für Informatik},
pages = {pages 42},
type = {Invited Abstract},
year = {2012},
doi = {10.4230/DagRep.2.7.30},
url = { https://publications.rwth-aachen.de/record/196294},
}×
[issue] 		Thomas Noll. Correctness, Safety and Fault Tolerance in Aerospace Systems: The ESA COMPASS Project, pages 42, Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2012.
2011
DOI [bibtex]
@conference{RIHEMCES2011,
title = {Reduction of Interrupt Handler Executions for Model Checking Embedded Software},
author = {Bastian Schlich and Thomas Noll and Jörg Brauer and Lucas Brutschy},
publisher = {Springer},
booktitle = {LNCS},
volume = {6405},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-19237-1_5},
url = { https://publications.rwth-aachen.de/record/116214},
}×
[issue] 		Bastian Schlich, Thomas Noll, Jörg Brauer, Lucas Brutschy. Reduction of Interrupt Handler Executions for Model Checking Embedded Software, 5. International Haifa Verification Conference, HCV 2009 (HCV 2009), Volume 6405 of LNCS, Springer, 2011.
DOI [bibtex]
@conference{ALGNFHRG2011,
title = {A Local Greibach Normal Form for Hyperedge Replacement Grammars},
author = {Christina Jansen and Jonathan Heinen and Joost-Pieter Katoen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {6638},
pages = {323-335},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-21254-3},
url = { https://publications.rwth-aachen.de/record/124910},
}×
[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 : 5. international conference (LATA 2011), Volume 6638 of LNCS, 323-335, Springer, 2011.
[bibtex]
@article{TAS2011,
title = {Trustworthy Aerospace Systems},
author = {Joost-Pieter Katoen and Thomas Noll},
publisher = {PS, PublicService.co.uk Ltd},
journal = {Public service review},
volume = {11},
pages = {pages 204-205},
type = {Journal Article},
year = {2011},
url = { https://publications.rwth-aachen.de/record/169201},
}×
[issue] 		Joost-Pieter Katoen, Thomas Noll. Trustworthy Aerospace Systems, Public service review 11, pages 204-205, PS, PublicService.co.uk Ltd, 2011.
DOI [bibtex]
@conference{SSCEDSP2011,
title = {System-Software Co-Engineering: Dependability and Safety Perspective},
author = {Yuri Yushtein and Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Xavier Olive and Marco Roveri},
publisher = {IEEE CS Press},
pages = {18-25},
type = {Conference Paper},
year = {2011},
doi = {10.1109/SMC-IT.2011.16},
url = { https://publications.rwth-aachen.de/record/227417},
}×
[issue] 		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, 4. IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT 2011), 18-25, IEEE CS Press, 2011.
2010
DOI [bibtex]
@conference{IAMCAIHS2010,
title = {Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software},
author = {Jörg Brauer and Thomas Noll and Bastian Schlich},
publisher = {ACM},
booktitle = {ACM Digital Library},
type = {Conference Paper},
year = {2010},
doi = {10.1145/1811212.1811216},
url = { https://publications.rwth-aachen.de/record/120063},
}×
[issue] 		Jörg Brauer, Thomas Noll, Bastian Schlich. Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software, 13. International Workshop on Software & Compilers for Embedded Systems (SCOPES '10), ACM Digital Library, ACM, 2010.
DOI [bibtex]
@conference{AMCA2010,
title = {A Model Checker for AADL},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri and Ralf Wimmer},
publisher = {Springer},
booktitle = {LNCS},
volume = {6174},
pages = {562-565},
type = {Conference Paper},
year = {2010},
doi = {10.1007/978-3-642-14295-6_48},
url = { https://publications.rwth-aachen.de/record/120064},
}×
[issue] 		Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer. A Model Checker for AADL, 22. international conference: Computer aided verification (CAV 2010), Volume 6174 of LNCS, 562-565, Springer, 2010.
fulltext PDF [bibtex]
@conference{LROS2010,
title = {Loop Refinement using Octagons and Satisfiability},
author = {Jörg Brauer and Volker Kamin and Stefan Kowalewski and Thomas Noll},
publisher = {ACM},
pages = {9 S.},
type = {Conference Paper},
year = {2010},
url = { https://publications.rwth-aachen.de/record/126462},
}×
[issue] 		Jörg Brauer, Volker Kamin, Stefan Kowalewski, Thomas Noll. Loop Refinement using Octagons and Satisfiability, 5. international conference on Systems software verification (SSV'10), 9 S., ACM, 2010.
DOI [bibtex]
@article{SDPAEAM2010,
title = {Safety, Dependability, and Performance Analysis of Extended AADL Models},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri},
publisher = {Univ. Press},
journal = {Computer journal},
volume = {51},
type = {Journal Article},
year = {2010},
doi = {10.1093/comjnl/bxq024},
url = { https://publications.rwth-aachen.de/record/171721},
}×
[issue] 		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, Univ. Press, 2010.
2009
DOI [bibtex]
@inbook{TCACMPAS2009,
title = {The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri},
publisher = {Springer},
booktitle = {LNCS},
volume = {5775},
pages = {173-186},
type = {Book Chapter},
year = {2009},
doi = {10.1007/978-3-642-04468-7_15},
url = { https://publications.rwth-aachen.de/record/83788},
}×
[issue] 		Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems, Volume 5775 of LNCS, 173-186, Springer, 2009.
DOI [bibtex]
@conference{CDSACBML2009,
title = {Codesign of Dependable Systems: A Component-Based Modeling Language},
author = {Marco Bozzano and Alessandro Cimatti and Marco Roveri and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll},
publisher = {IEEE},
pages = {121-130},
type = {Conference Paper},
year = {2009},
doi = {10.1109/MEMCOD.2009.5185388},
url = { https://publications.rwth-aachen.de/record/100524},
}×
[issue] 		Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. Codesign of Dependable Systems: A Component-Based Modeling Language, 7. ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 121-130, IEEE, 2009.
fulltext PDF [bibtex]
@conference{MBCCES2009,
title = {Model-Based Codesign of Critical Embedded Systems},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {507},
pages = {87-91},
type = {Conference Paper},
year = {2009},
url = { https://publications.rwth-aachen.de/record/100526},
}×
[issue] 		Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Model-Based Codesign of Critical Embedded Systems, 2. International Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB 2009), Volume 507 of CEUR Workshop Proceedings, 87-91, RWTH Aachen, 2009.
[bibtex]
@conference{VPEAMTD2009,
title = {Verification and Performance Evaluation of AADL Models (Tool Demonstration)},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri},
publisher = {ACM},
pages = {285-286},
type = {Conference Paper},
year = {2009},
url = { https://publications.rwth-aachen.de/record/100527},
}×
[issue] 		Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Verification and Performance Evaluation of AADL Models (Tool Demonstration), Joint 12. European Software Engineering Conference and 17. ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC-FSE’09), 285-286, ACM, 2009.
2008
DOI [bibtex]
@inbook{D2008,
title = {Delayed nondeterminism in model checking embedded systems assembly code},
author = {Thomas Noll and Bastian Schlich},
publisher = {Springer},
booktitle = {LNCS},
volume = {4899},
pages = {185-201},
type = {Book Chapter},
year = {2008},
doi = {10.1007/978-3-540-77966-7_16},
url = { https://publications.rwth-aachen.de/record/83461},
}×
[issue] 		Thomas Noll, Bastian Schlich. Delayed nondeterminism in model checking embedded systems assembly code, Volume 4899 of LNCS, 185-201, Springer, 2008.
DOI [bibtex]
@inbook{VDPMT2008,
title = {Verifying Dynamic Pointer-Manipulating Threads},
author = {Thomas Noll and Stefan Rieger},
publisher = {Springer},
booktitle = {LNCS},
volume = {5014},
pages = {84-99},
type = {Book Chapter},
year = {2008},
doi = {10.1007/978-3-540-68237-0_8},
url = { https://publications.rwth-aachen.de/record/83800},
}×
[issue] 		Thomas Noll, Stefan Rieger. Verifying Dynamic Pointer-Manipulating Threads, Volume 5014 of LNCS, 84-99, Springer, 2008.
DOI [bibtex]
@conference{ACDSHR2008,
title = {Abstracting Complex Data Structures by Hyperedge Replacement},
author = {Stefan Rieger and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {5214},
pages = {69-83},
type = {Conference Paper},
year = {2008},
doi = {10.1007/978-3-540-87405-8_6},
url = { https://publications.rwth-aachen.de/record/83801},
}×
[issue] 		Stefan Rieger, Thomas Noll. Abstracting Complex Data Structures by Hyperedge Replacement, Graph transformations : 4. International Conference (ICGT 2008), Volume 5214 of LNCS, 69-83, Springer, 2008.
DOI [bibtex]
@article{P2008,
title = {Proving correctness of an efficient abstraction for interrupt handling},
author = {Gerlind Herberich and Bastian Schlich and Carsten Weise and Thomas Noll},
publisher = {Elsevier Science},
journal = {Electronic notes in theoretical computer science},
volume = {217},
pages = {pages 133-150},
type = {Journal Article},
year = {2008},
doi = {10.1016/j.entcs.2008.06.046},
url = { https://publications.rwth-aachen.de/record/130980},
}×
[issue] 		Gerlind Herberich, Bastian Schlich, Carsten Weise, 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]
@article{EARSSRT2008,
title = {Equational Abstractions for Reducing the State Space of Rewrite Theories},
author = {Lars Helge Haß and Thomas Noll},
publisher = {Elsevier},
journal = {Electronic notes in theoretical computer science},
volume = {238(3)},
pages = {pages 139-154},
type = {Journal Article},
year = {2008},
doi = {10.1016/j.entcs.2009.05.017},
url = { https://publications.rwth-aachen.de/record/134127},
}×
[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.
2007
DOI [bibtex]
@inbook{CTOLC2007,
title = {Composing Transformations to Optimize Linear Code},
author = {Thomas Noll and Stefan Rieger},
publisher = {Springer},
booktitle = {LNCS},
volume = {4711},
pages = {425-439},
type = {Book Chapter},
year = {2007},
doi = {10.1007/978-3-540-75292-9_29},
url = { https://publications.rwth-aachen.de/record/89820},
}×
[issue] 		Thomas Noll, Stefan Rieger. Composing Transformations to Optimize Linear Code, Volume 4711 of LNCS, 425-439, Springer, 2007.
fulltext PDF [bibtex]
@techreport{VL2007,
title = {Verifying concurrent list-manipulating programs by LTL model checking},
author = {Joost-Pieter Katoen and Thomas Noll and Stefan Rieger},
publisher = {RWTH, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2007,6},
pages = {26 Bl. : graph. Darst.},
type = {Tech Report},
year = {2007},
url = { https://publications.rwth-aachen.de/record/96680},
}×
[issue] 		Joost-Pieter Katoen, Thomas Noll, Stefan Rieger. 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.
fulltext PDF [bibtex]
@conference{VL2007,
title = {Verifying concurrent list-manipulating programs by LTL model checking},
author = {Joost-Pieter Katoen and Thomas Noll and Stefan Rieger},
pages = {94-113},
type = {Conference Paper},
year = {2007},
url = { https://publications.rwth-aachen.de/record/115549},
}×
[issue] 		Joost-Pieter Katoen, Thomas Noll, Stefan Rieger. Verifying concurrent list-manipulating programs by LTL model checking, Workshop on Heap Analysis and Verification (HAV 2007), 94-113, 2007.
DOI [bibtex]
@article{AEM2007,
title = {Abstraction and model checking of core Erlang programs in Maude},
author = {Martin R. Neuhäußer and Thomas Noll},
publisher = {Elsevier},
journal = {Electronic notes in theoretical computer science},
volume = {176(4)},
pages = {pages 147-163},
type = {Journal Article},
year = {2007},
doi = {10.1016/j.entcs.2007.06.013},
url = { https://publications.rwth-aachen.de/record/158140},
}×
[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
DOI [bibtex]
@conference{TE2006,
title = {Towards automatic verification of Erlang programs by pi-calculus translation},
author = {Thomas Noll and Chanchal Kumar Roy},
publisher = {ACM},
pages = {38-50},
type = {Conference Paper},
year = {2006},
doi = {10.1145/1159789.1159798},
url = { https://publications.rwth-aachen.de/record/111729},
}×
[issue] 		Thomas Noll, Chanchal Kumar Roy. Towards automatic verification of Erlang programs by pi-calculus translation, ACM SIGPLAN Workshop on Generic Programming 2006 (WGP 2006), 38-50, ACM, 2006.
DOI [bibtex]
@article{A2006,
title = {Algebraic correctness proofs for compiling recursive function definitions with strictness information},
author = {Klaus Indermark and Thomas Noll},
publisher = {Springer},
journal = {Acta informatica},
volume = {43(1)},
pages = {pages 1-43},
type = {Journal Article},
year = {2006},
doi = {10.1007/s00236-006-0013-0},
url = { https://publications.rwth-aachen.de/record/152839},
}×
[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.
fulltext PDF [bibtex]
@article{O2006,
title = {Optimization of straight-line code revisited},
author = {Thomas Noll and Stefan Rieger},
publisher = {GI},
journal = {Softwaretechnik-Trends},
volume = {26(2)},
type = {Journal Article},
year = {2006},
url = { https://publications.rwth-aachen.de/record/155968},
}×
[issue] 		Thomas Noll, Stefan Rieger. Optimization of straight-line code revisited, Softwaretechnik-Trends 26 (2), GI, 2006.
2005
[bibtex]
@conference{MEC2005,
title = {Modeling Erlang in the pi-Calculus},
author = {Thomas Noll and Chanchal Kumar Roy},
publisher = {ACM Press},
pages = {72-77},
type = {Conference Paper},
year = {2005},
url = { https://publications.rwth-aachen.de/record/113383},
}×
[issue] 		Thomas Noll, Chanchal Kumar Roy. Modeling Erlang in the pi-Calculus, ACM SIGPLAN 2005 Erlang Workshop (Erlang 05), 72-77, ACM Press, 2005.
[bibtex]
@conference{TE2005,
title = {Towards automatic verification of Erlang programs by pi-calculus translation},
author = {Thomas Noll and Chanchal Kumar Roy},
publisher = {ACM Press},
pages = {38-50},
type = {Conference Paper},
year = {2005},
url = { https://publications.rwth-aachen.de/record/113836},
}×
[issue] 		Thomas Noll, Chanchal Kumar Roy. Towards automatic verification of Erlang programs by pi-calculus translation, ACM SIGPLAN 2005 Erlang Workshop (Erlang 2005), 38-50, ACM Press, 2005.
DOI [bibtex]
@article{FMH2005,
title = {Functional programming languages for verification tools: a comparison of ML and Haskell},
author = {Martin Leucker and Thomas Noll and Perdita Stevens and Michael Weber},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {7(2)},
pages = {pages 184-194},
type = {Journal Article},
year = {2005},
doi = {10.1007/s10009-004-0184-3},
url = { https://publications.rwth-aachen.de/record/155632},
}×
[issue] 		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 7 (2), pages 184-194, Springer, 2005.
2002
DOI [bibtex]
@conference{GM2002,
title = {Generalised regular MSC languages},
author = {Benedikt Bollig and Martin Leucker and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {2303},
pages = {52-66},
type = {Conference Paper},
year = {2002},
doi = {10.1007/3-540-45931-6_5},
url = { https://publications.rwth-aachen.de/record/117694},
}×
[issue] 		Benedikt Bollig, Martin Leucker, Thomas Noll. Generalised regular MSC languages, Foundations of software science and computation structures : 5. international conference (FOSSACS 2002), Volume 2303 of LNCS, 52-66, Springer, 2002.
2001
fulltext PDF [bibtex]
@techreport{KGPSR2001,
title = {Kolloquium programmiersprachen und Grundlagen der Programmierung ; 11 (Simmerath-Rurberg): 2001.10.07-11},
author = {},
editor = {Klaus Indermark and Thomas Noll},
publisher = {RWTH, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2001,11},
pages = {128 Bl.. : graph. Darst.},
type = {Tech Report},
year = {2001},
url = { https://publications.rwth-aachen.de/record/47522},
}×
[issue] 		Klaus Indermark (ed), Thomas Noll (ed). Kolloquium programmiersprachen und Grundlagen der Programmierung ; 11 (Simmerath-Rurberg): 2001.10.07-11, Volume 2001,11 of Aachener Informatik-Berichte, 128 Bl.. : graph. Darst., RWTH, Department of Computer Science, 2001.
fulltext PDF [bibtex]
@techreport{RM2001,
title = {Regular MSC languages},
author = {Benedikt Bollig and Martin Leucker and Thomas Noll},
publisher = {RWTH},
booktitle = {Aachener Informatik-Berichte},
volume = {2001,5},
type = {Tech Report},
year = {2001},
url = { https://publications.rwth-aachen.de/record/47889},
}×
[issue] 		Benedikt Bollig, Martin Leucker, Thomas Noll. Regular MSC languages, Volume 2001,5 of Aachener Informatik-Berichte, RWTH, 2001.
[bibtex]
@conference{TS2001,
title = {Truth/SLC: a parallel verification platform for concurrent systems},
author = {Martin Leucker and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {2102},
pages = {255-259},
type = {Conference Paper},
year = {2001},
url = { https://publications.rwth-aachen.de/record/107394},
}×
[issue] 		Martin Leucker, Thomas Noll. Truth/SLC: a parallel verification platform for concurrent systems, Computer aided verification : 13. international conference (CAV 2001), Volume 2102 of LNCS, 255-259, Springer, 2001.
DOI [bibtex]
@conference{SE2001,
title = {Semi-automated verification of Erlang code},
author = {Lars-Åke Fredlund and Dilian Gurov and Thomas Noll},
publisher = {IEEE Computer Society},
pages = {319-323},
type = {Conference Paper},
year = {2001},
doi = {10.1109/ASE.2001.989820},
url = { https://publications.rwth-aachen.de/record/108418},
}×
[issue] 		Lars-Åke Fredlund, Dilian Gurov, Thomas Noll. Semi-automated verification of Erlang code, 16. Annual International Conference on Automated Software Engineering (ASE 2001), 319-323, IEEE Computer Society, 2001.
[bibtex]
@conference{VE2001,
title = {Verifying generic Erlang client-server implementations},
author = {Thomas Arts and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {2011},
pages = {37-52},
type = {Conference Paper},
year = {2001},
url = { https://publications.rwth-aachen.de/record/108933},
}×
[issue] 		Thomas Arts, Thomas Noll. Verifying generic Erlang client-server implementations, 12. international workshop Implementation of functional languages (IFL 2000), Volume 2011 of LNCS, 37-52, Springer, 2001.
[bibtex]
@conference{T2001,
title = {Transaction-based anomaly detection in communication networks},
author = {Roland Büschkes and Thomas Noll and Mark Borning},
type = {Conference Paper},
year = {2001},
url = { https://publications.rwth-aachen.de/record/108996},
}×
[issue] 		Roland Büschkes, Thomas Noll, Mark Borning. Transaction-based anomaly detection in communication networks, 9. International Conference on Telecommunication Systems - Modeling and Analysis, 2001.
[bibtex]
@conference{TE2001,
title = {The Erlang verification tool},
author = {L.-A. Fredlund and D. Gurov and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {2031},
pages = {582-585},
type = {Conference Paper},
year = {2001},
url = { https://publications.rwth-aachen.de/record/111451},
}×
[issue] 		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, 582-585, Springer, 2001.
DOI [bibtex]
@article{AE2001,
title = {A rewriting logic implementation of Erlang},
author = {Thomas Noll},
publisher = {Elsevier Science},
journal = {Electronic notes in theoretical computer science},
volume = {44(2)},
pages = {pages 206-224},
type = {Journal Article},
year = {2001},
doi = {10.1016/S1571-0661(04)80928-9},
url = { https://publications.rwth-aachen.de/record/146610},
}×
[issue] 		Thomas Noll. A rewriting logic implementation of Erlang, Electronic notes in theoretical computer science 44 (2), pages 206-224, Elsevier Science, 2001.
2000
[bibtex]
@techreport{VE2000,
title = {Verifying generic Erlang client-server implementations},
author = {Thomas Arts and Thomas Noll},
publisher = {RWTH, Fachgruppe Informatik},
booktitle = {Aachener Informatik-Berichte},
volume = {2000,08},
pages = {26 Bl.},
type = {Tech Report},
year = {2000},
url = { https://publications.rwth-aachen.de/record/47875},
}×
[issue] 		Thomas Arts, Thomas Noll. Verifying generic Erlang client-server implementations, Volume 2000,08 of Aachener Informatik-Berichte, 26 Bl., RWTH, Fachgruppe Informatik, 2000.
[bibtex]
@inbook{C2000,
title = {Context-representable processes},
author = {Mads Dam and Thomas Noll},
publisher = {Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI)},
booktitle = {Dagstuhl-Seminar-Report},
volume = {271},
pages = {19-22},
type = {Book Chapter},
year = {2000},
url = { https://publications.rwth-aachen.de/record/88115},
}×
[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]
@conference{VECS2000,
title = {Verifying generic Erlang Client-Server implementations},
author = {Thomas Arts and Thomas Noll},
publisher = {RWTH, Fachgruppe Informatik},
booktitle = {Aachener Informatik-Berichte},
volume = {2000,07},
pages = {387-402},
type = {Conference Paper},
year = {2000},
url = { https://publications.rwth-aachen.de/record/107335},
}×
[issue] 		Thomas Arts, Thomas Noll. Verifying generic Erlang Client-Server implementations, 12. International Workshop on Implementation of Functional Languages, Volume 2000,07 of Aachener Informatik-Berichte, 387-402, RWTH, Fachgruppe Informatik, 2000.
fulltext PDF [bibtex]
@conference{TH2000,
title = {Truth - a real-world application in Haskell},
author = {M. Leucker and Thomas Noll},
publisher = {RWTH Aachen},
booktitle = {Aachener Informatik-Berichte},
volume = {2000,07},
pages = {363-380},
type = {Conference Paper},
year = {2000},
url = { https://publications.rwth-aachen.de/record/111080},
}×
[issue] 		M. Leucker, Thomas Noll. Truth - a real-world application in Haskell, 12. International Workshop on Implementation of Functional Languages, Volume 2000,07 of Aachener Informatik-Berichte, 363-380, RWTH Aachen, 2000.
DOI [bibtex]
@article{T2000,
title = {The universality of higher-order attributed tree transducers},
author = {Thomas Noll and H. Vogler},
publisher = {Springer},
journal = {Theory of computing systems},
volume = {34},
pages = {pages 45-75},
type = {Journal Article},
year = {2000},
doi = {10.1007/s002240010018},
url = { https://publications.rwth-aachen.de/record/143815},
}×
[issue] 		Thomas Noll, H. Vogler. The universality of higher-order attributed tree transducers, Theory of computing systems 34, pages 45-75, Springer, 2000.
1999
[bibtex]
@techreport{O1999,
title = {On the universality of higher-order attributed tree transducers},
author = {Thomas Noll and Heiko Vogler},
publisher = {TU, Fak. Informatik},
booktitle = {Technische Berichte / Technische Universität Dresden, Fakultät Informatik},
volume = {99/05},
pages = {23 S. : graph. Darst.},
type = {Tech Report},
year = {1999},
url = { https://publications.rwth-aachen.de/record/95056},
}×
[issue] 		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, 23 S. : graph. Darst., TU, Fak. Informatik, 1999.
[bibtex]
@conference{KMS1999,
title = {Kohärenzeigenschaften in termersetzungsbasierten Modellen für verteilte Systeme},
author = {Thomas Noll},
publisher = {GhK},
booktitle = {Mathematische Schriften Kassel},
volume = {99,12},
pages = {52-52},
type = {Conference Paper},
year = {1999},
url = { https://publications.rwth-aachen.de/record/103936},
}×
[issue] 		Thomas Noll. Kohärenzeigenschaften in termersetzungsbasierten Modellen für verteilte Systeme, 9. Theorietag der GI-Fachgruppe 0.1.5 'Automaten und Formale Sprachen', Volume 99,12 of Mathematische Schriften Kassel, 52-52, GhK, 1999.
[bibtex]
@conference{O1999,
title = {On coherence properties in term rewriting models of concurrency},
author = {Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {1664},
pages = {478-493},
type = {Conference Paper},
year = {1999},
url = { https://publications.rwth-aachen.de/record/103937},
}×
[issue] 		Thomas Noll. On coherence properties in term rewriting models of concurrency, CONCUR '99 - Concurrency Theory : 10. International Conference, Volume 1664 of LNCS, 478-493, Springer, 1999.
[bibtex]
@conference{O1999,
title = {On the universality of higher-order attribute grammars},
author = {Thomas Noll and H. Vogler},
publisher = {Techn. Univ., Fakultät Informatik},
booktitle = {Technische Berichte / Technische Universität Dresden, Fakultät Informatik},
volume = {99/01},
type = {Conference Paper},
year = {1999},
url = { https://publications.rwth-aachen.de/record/103938},
}×
[issue] 		Thomas Noll, H. Vogler. On the universality of higher-order attribute grammars, International Workshop Grammers, Automata, and Logic on Graphs and Trees, Volume 99/01 of Technische Berichte / Technische Universität Dresden, Fakultät Informatik, Techn. Univ., Fakultät Informatik, 1999.
[bibtex]
@conference{T1999,
title = {Truth - a verification platform for concurrent systems, tool support for system specification, development and verification},
author = {M. Lange and M. Leucker and Thomas Noll and S. Tobies},
publisher = {Springer},
booktitle = {LNCS},
volume = {1742},
pages = {150-159},
type = {Conference Paper},
year = {1999},
url = { https://publications.rwth-aachen.de/record/103940},
}×
[issue] 		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), Volume 1742 of LNCS, 150-159, Springer, 1999.
DOI [bibtex]
@conference{R1999,
title = {Rapid prototyping of specification language implementations},
author = {Martin Leucker and Thomas Noll},
publisher = {IEEE Computer Soc.},
booktitle = {IEEE / IFIP International Symposium on Rapid System Prototyping. Proceedings},
pages = {60-65},
type = {Conference Paper},
year = {1999},
doi = {10.1109/IWRSP.1999.779032},
url = { https://publications.rwth-aachen.de/record/209176},
}×
[issue] 		Martin Leucker, Thomas Noll. Rapid prototyping of specification language implementations, IEEE International Workshop on Rapid Systems Prototyping, IEEE / IFIP International Symposium on Rapid System Prototyping. Proceedings, 60-65, IEEE Computer Soc., 1999.
1993
[bibtex]
@conference{H1993,
title = {Hierarchical parallelization of imperative programs},
author = {A. Kindler and Thomas Noll and B. Steffen},
pages = {178-184},
type = {Conference Paper},
year = {1993},
url = { https://publications.rwth-aachen.de/record/121747},
}×
[issue] 		A. Kindler, Thomas Noll, B. Steffen. Hierarchical parallelization of imperative programs, EuroMicro Workshop on Parallel and Distributed Process, 178-184, 1993.
[bibtex]
@conference{O1993,
title = {On the first-order equivalence of call-by-name and call-by-value},
author = {Thomas Noll},
publisher = {Univ. der Bundeswehr},
booktitle = {Bericht / Universität der Bundeswehr München, Fakultät für Informatik},
volume = {9309},
pages = {175-186},
type = {Conference Paper},
year = {1993},
url = { https://publications.rwth-aachen.de/record/121754},
}×
[issue] 		Thomas Noll. On the first-order equivalence of call-by-name and call-by-value, Workshop Programmiersprachen u. Grundl. d. Programmier, Volume 9309 of Bericht / Universität der Bundeswehr München, Fakultät für Informatik, 175-186, Univ. der Bundeswehr, 1993.
1992
[bibtex]
@book{T1992,
title = {Top-down parsing with simultaneous evaluation of noncircular attribute grammars},
author = {Thomas Noll and H. Vogler},
booktitle = {Aachener Informatik-Berichte},
volume = {92,14},
type = {Book},
year = {1992},
url = { https://publications.rwth-aachen.de/record/97055},
}×
[issue] 		Thomas Noll, H. Vogler. Top-down parsing with simultaneous evaluation of noncircular attribute grammars, Volume 92,14 of Aachener Informatik-Berichte, 1992.