Publications

2016
DOI
[bibtex]
Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Joost-Pieter Katoen, Erika Abraham, Harold Bruintjes. Parameter Synthesis for Probabilistic Systems. Proc. of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'16), pages 72-74, Albert-Ludwigs-Universität Freiburg, 2016.
DOI
[bibtex]
Francesco Leofante, Simone Vuotto, Erika Abraham, Armando Tacchella, Nils Jansen. Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, Part I, Volume 9952 of LNCS, pages 496-514, Springer International Publishing, 2016.
2015
Download
[bibtex]
Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, Erika Abraham. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. Proc. of the 27th Int. Conf. on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, pages 214–231, Springer, 2015.
Download
[bibtex]
Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards. Proc. of the 20th Int. Symp. on Formal Methods (FM'15), Volume 9109 of LNCS, pages 435–452, Springer, 2015.
Link
[bibtex]
Shashank Pathak, Erika Abraham, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen. A Greedy Approach for the Efficient Repair of Stochastic Models. Proc. of the 7th NASA Formal Methods Symp. (NFM'15), Volume 9058 of LNCS, pages 295–309, Springer, 2015.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen. High-level Counterexamples for Probabilistic Automata. Logical Methods in Computer Science (LMCS) 11(1:15), pages 1–23, 2015.
Download
[bibtex]
Nils Jansen. Counterexamples in Probabilistic Verification. Phd Thesis at RWTH Aachen University, 2015.
2014
Download
[bibtex]
Erika Abraham, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer. Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey. Proc. of the 14th Int. School on Formal Methods for the Design of Computer, Communication and Software Systems: Executable Software Models (SFM-14:ESM), Volume 8483 of LNCS, pages 65–121, Springer, 2014.
Download
[bibtex]
Nils Jansen, Ralf Wimmer, Erika Abraham, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster. Symbolic Counterexample Generation for Large Discrete-Time Markov Chains. Science of Computer Programming 91 (Part A), pages 90–114, 2014.
Download
[bibtex]
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. 11th Int. Conf. on Quantitative Evaluation of Systems (QEST'14), Volume 8657 of LNCS, pages 404–420, Springer, 2014.
DOI
[bibtex]
Ralf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Linear-Time Probabilistic Verification. Theoretical Computer Science 549, pages 61–100, 2014.
Download
[bibtex]
Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen. Fast Debugging of PRISM Models. Int. Symp. on Automated Technology for Verification and Analysis (ATVA'14), Volume 8837 of LNCS, pages 146–162, Springer, 2014.
2013
Download
[bibtex]
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. Technical report at Cornell University number arXiv:1312.3979, 2013.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata. Proc. of the 10th Int. Conf. on Quantitative Evaluation of Systems (QEST'13), Volume 8054 of LNCS, pages 39–54, Springer-Verlag, 2013.
Download
[bibtex]
Daniel Neider, Nils Jansen. Regular Model Checking Using Solver Technologies and Automata Learning. 5th NASA Formal Methods Symposium (NFM'13), Volume 7871 of LNCS, pages 16–31, Springer Berlin Heidelberg, 2013.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata. Technical report at Cornell University number arXiv:1305.5055, 2013.
2012
Download
[bibtex]
Nils Jansen, Erika Abraham, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool - Computing Minimal Counterexamples for DTMCs. Proc. of the 10th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'12), Volume 7561 of LNCS, pages 349–353, Springer Berlin Heidelberg, 2012.
Download
[bibtex]
Nils Jansen, Erika Abraham, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker. Symbolic Counterexample Generation for Discrete-time Markov Chains. 9th Int. Symp. on Formal Aspects of Component Software (FACS'12), Volume 7684 of LNCS, pages 134–151, Springer Berlin Heidelberg, 2012.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes. Technical report at Reports of SFB/TR 14 AVACS number 88, 2012.
Download
[bibtex]
Nils Jansen, Erika Abraham, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains. Technical report at Cornell University number arXiv:1206.0603v1, 2012.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Erika Abraham, Bernd Becker, Joost-Pieter Katoen. Minimal Critical Subsystems for Discrete-Time Markov Models. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), Volume 7214 of LNCS, pages 299–314, Springer Berlin Heidelberg, 2012.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'12), pages 169–180, Verlag Dr. Kovac, 2012.
2011
Download
[bibtex]
Erika Abraham, Nadine Bergner, Philipp Brauner, Florian Corzilius, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Johanna Nellen, Ulrik Schroeder. On Collaboratively Conveying Computer Science to Pupils. Proc. of the 11th Koli Calling Int. Conf. on Computing Education Research (KOLI'11), pages 132–137, ACM, 2011.
Download
[bibtex]
Nils Jansen, Erika Abraham, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. Hierarchical Counterexamples for Discrete-Time Markov Chains. 9th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'11), Volume 6996 of LNCS, pages 443–452, Springer Berlin Heidelberg, 2011.
Download
[bibtex]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham. Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking. Formal Techniques for Distributed Systems (FMOODS/FORTE'11), Volume 6722 of LNCS, pages 75–89, Springer Berlin Heidelberg, 2011.
Download
[bibtex]
Nils Jansen, Erika Abraham, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. Hierarchical Counterexamples for Discrete-Time Markov Chains. Technical report at RWTH Aachen University number AIB-2011-11, 2011.
Download
[bibtex]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham. SMT-based Counterexample Generation for Markov Chains. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'11), pages 19–28, OFFIS-Institut für Informatik, 2011.
Download
[bibtex]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham. SMT-based Counterexample Generation for Discrete-Time Markov Chains. Workshop on Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems (ROCKS'11), , 2011.
2010
Download
[bibtex]
Erika Abraham, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. DTMC Model Checking by SCC Reduction. 7th Int. Conf. on Quantitative Evaluation of Systems (QEST'10), pages 37–46, IEEE, 2010.
Download
[bibtex]
Erika Abraham, Philipp Brauner, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Ulrik Schroeder. Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik. Interaktive Kulturen - Die 8. E-Learning Fachtagung Informatik (DeLFI'10), Volume 169 of LNI, pages 239–251, Gesellschaft für Informatik, 2010.