Publications

2017

Preprint
Heap Abstraction Beyond Context-Freeness
Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll
PDF of Heap Abstraction Beyond Context-Freeness RWTH record for Heap Abstraction Beyond Context-Freeness BibTeX for Heap Abstraction Beyond Context-Freeness
Technical report
Analysis and Verification of Pointer Programs : October 2-5, 2017
Marieke Huisman, Thomas Noll, Makoto Tatsuta
RWTH record for Analysis and Verification of Pointer Programs : October 2-5, 2017 BibTeX for Analysis and Verification of Pointer Programs : October 2-5, 2017
Book chapter
Synthesis and Verification of Self-aware Computing Systems
Radu Calinescu, Marco Autili, Javier Ciamara, Antinisca Di Marco, Simos Gerasimou, Paola Inverardi, Alexander Perucci, Nils Jansen, Joost-Pieter Katoen, Marta Kwiatkowska, Ole J. Mengshoel, Romina Spalazzese, Massimo Tivoli
Self-Aware Computing Systems
RWTH record for Synthesis and Verification of Self-aware Computing Systems BibTeX for Synthesis and Verification of Self-aware Computing Systems
Conference paper
Formal Methods for Aerospace Systems : Achievements and Challenges
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta
Cyber-Physical System Design from an Architecture Analysis Viewpoint
RWTH record for Formal Methods for Aerospace Systems : Achievements and Challenges BibTeX for Formal Methods for Aerospace Systems : Achievements and Challenges
Book
ModelEd, TestEd, TrustEd : essays dedicated to Ed Brinksma on the occassion of his 60th birthday
Joost-Pieter Katoen, Rom Langerak, Arend Rensink
Springer
RWTH record for ModelEd, TestEd, TrustEd : essays dedicated to Ed Brinksma on the occassion of his 60th birthday BibTeX for ModelEd, TestEd, TrustEd : essays dedicated to Ed Brinksma on the occassion of his 60th birthday
Conference paper
Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract)
Joost-Pieter Katoen
Theoretical Aspects of Computing - ICTAC 2017
RWTH record for Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract)BibTeX for Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract)
Book chapter
Boosting Fault Tree Analysis by Formal Methods
Joost-Pieter Katoen, Marielle Stoelinga
ModelEd, TestEd, TrustEd
RWTH record for Boosting Fault Tree Analysis by Formal Methods BibTeX for Boosting Fault Tree Analysis by Formal Methods
Conference paper
Modal Stochastic Games : Abstraction-Refinement of Probabilistic Automata
Joost-Pieter Katoen, Falak Sher
Models, algorithms, logics and tools
RWTH record for Modal Stochastic Games : Abstraction-Refinement of Probabilistic Automata BibTeX for Modal Stochastic Games : Abstraction-Refinement of Probabilistic Automata
Conference paper
Motion planning under partial observability using game-based abstraction
Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker
2017 IEEE 56th Annual Conference on Decision and Control (CDC)
RWTH record for Motion planning under partial observability using game-based abstraction BibTeX for Motion planning under partial observability using game-based abstraction
Conference paper
Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms
Saba Aflaki, Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Arne Storjohann
2017 IEEE 36th International Symposium on Reliable Distributed Systems
RWTH record for Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms BibTeX for Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms
Conference paper
Model-based Safety Analysis for Vehicle Guidance Systems
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk
Computer safety, reliability, and security
RWTH record for Model-based Safety Analysis for Vehicle Guidance Systems BibTeX for Model-based Safety Analysis for Vehicle Guidance Systems
Conference paper
The COMPASS 3.0 Toolset
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta
RWTH record for The COMPASS 3.0 Toolset BibTeX for The COMPASS 3.0 Toolset
Conference paper
Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees
Sascha Müller, Andreas Gerndt, Thomas Noll
AIAA Space and Astronautics Forum and Exposition 2017
RWTH record for Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees BibTeX for Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees
Conference paper
Markov Automata with Multiple Objectives
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen
Computer aided verification
RWTH record for Markov Automata with Multiple Objectives BibTeX for Markov Automata with Multiple Objectives
Conference paper
JANI: Quantitative Model and Tool Interaction
Carlos E. Budde, Hans Christian Dehnert, E. Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini
Tools and algorithms for the construction and analysis of systems
RWTH record for JANI: Quantitative Model and Tool Interaction BibTeX for JANI: Quantitative Model and Tool Interaction
Conference paper
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, Ufuk Topcu
Tools and algorithms for the construction and analysis of systems
RWTH record for Sequential Convex Programming for the Efficient Verification of Parametric MDPs BibTeX for Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Conference paper
Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications
Louis Wachtmeister, Thomas Noll
[embeddedworld Exibition & Conference, 2017-03-14 - 2017-03-16, Nuremberg, Germany]
PDF of Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications RWTH record for Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications BibTeX for Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications
Conference paper
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger
Programming languages and systems
RWTH record for Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic BibTeX for Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
Conference paper
A Storm is Coming: A Modern Probabilistic Model Checker
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk
Computer aided verification
RWTH record for A Storm is Coming: A Modern Probabilistic Model Checker BibTeX for A Storm is Coming: A Modern Probabilistic Model Checker
Journal article
Missie: foutvrije software in de ruimte
Harold Yorick Bruintjes, Joost-Pieter Katoen
Bits en Chips
RWTH record for Missie: foutvrije software in de ruimte BibTeX for Missie: foutvrije software in de ruimte
Preprint
A storm is Coming: A Modern Probabilistic Model Checker
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk
PDF of A storm is Coming: A Modern Probabilistic Model Checker RWTH record for A storm is Coming: A Modern Probabilistic Model Checker BibTeX for A storm is Coming: A Modern Probabilistic Model Checker
Conference paper
A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations
Benjamin Lucien Kaminski, Joost-Pieter Katoen
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
RWTH record for A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations BibTeX for A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations
Journal article
Fault trees on a diet: automated reduction by graph rewriting
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga
Formal aspects of computing
RWTH record for Fault trees on a diet: automated reduction by graph rewriting BibTeX for Fault trees on a diet: automated reduction by graph rewriting
Journal article
Quantitative model-checking of controlled discrete-time Markov processes
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate
Information and Computation
RWTH record for Quantitative model-checking of controlled discrete-time Markov processes BibTeX for Quantitative model-checking of controlled discrete-time Markov processes

2016

Preprint
Satisfiability checking and symbolic computation
Erika Ábrahám, P. Fontaine, S. Forrest, A. Griggio, D. Kroening, W. M. Seiler, T. Sturm, J. Abbott, B. Becker, A. M. Bigatti, M. Brain, B. Buchberger, A. Cimatti, J. H. Davenport, M. England
PDF of Satisfiability checking and symbolic computation RWTH record for Satisfiability checking and symbolic computation BibTeX for Satisfiability checking and symbolic computation