Publications

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.
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.
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.
Link
[bibtex]
Ralf Wimmer, Erika Abraham. Maybe or Maybe Not: Contributions to Stochastic Verification. Aspekte der Technischen Informatik: Festschrift zum 60. Geburtstag von Bernd Becker, Monsenstein und Vannerdat, 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]
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.

[bibtex]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Abraham. Stochastic Bounded Model Checking: Bounded Rewards and Compositionality. Proc. of Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'13), pages 243–254, , 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]
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.

[bibtex]
Natalia Kalinnik, Erika Abraham, Tobias Schubert, Ralf Wimmer, Bernd Becker. Exploiting Different Strategies for the Parallelization of an SMT Solver. 13. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'10), pages 97–106, Fraunhofer Verlag, 2010.
Download
[bibtex]
Erika Abraham, Ulrich Loup, Ralf Wimmer, Joost-Pieter Katoen. On the Minimization of Hybrid Automata. Nordic Workshop on Programming Theory (NWPT'10), , 2010.
2009
Download
[bibtex]
Natalia Kalinnik, Tobias Schubert, Erika Abraham, Ralf Wimmer, Bernd Becker. Picoso - A Parallel Interval Constraint Solver. Int. Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA'09), pages 473–479, CSREA Press, 2009.