Publications

2017
DOI
[bibtex]
Erika Abraham, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm. Satisfiability Checking and Symbolic Computation. ACM Commun. Comput. Algebra 50(4), pages 145–147, 2017.
2016

[bibtex]
Erika Abraham, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm. Satisfiability Checking and Symbolic Computation. CoRR (Proc. of the 41th Int. Symposium on Symbolic and Algebraic Computation, ISSAC'16) abs/1607.06945, 2016.
DOI
[bibtex]
Erika Abraham, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm. SC$^ 2$: Satisfiability Checking meets Symbolic Computation. Proc. of the 9th Conf. on Intelligent Computer Mathematics (CICM'16), Volume 9791 of LNCS, pages 28-43, , 2016.
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.
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.
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.
Download
[bibtex]
Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Abraham, Bernd Becker. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition. Proc. of the 24th International Conference on Automated Deduction (CADE-24), Volume 7898 of LNCS, pages 193–207, Springer-Verlag, 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]
Erika Abraham, Tobias Schubert, Bernd Becker, Martin Fraenzle, Christian Herde. Parallel SAT Solving in Bounded Model Checking. Journal of Logic and Computation 21(1), pages 5–21, 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.
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.
2007
DOI
[bibtex]
Erika Abraham, Marc Herbstritt, Bernd Becker, Martin Steffen. Bounded Model Checking with Parametric Data Structures. Int. Workshop on Bounded Model Checking (BMC'06), Volume 174 of ENTCS, pages 3–16, Elsevier Science Publishers, 2007.
DOI
[bibtex]
Marc Herbstritt, Bernd Becker, Erika Abraham, Christian Herde. On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata. IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS'07), pages 1–6, IEEE Computer Society, 2007.
2006
DOI
[bibtex]
Erika Abraham, Tobias Schubert, Bernd Becker, Martin Fraenzle, Christian Herde. Parallel SAT Solving in Bounded Model Checking. Parallel and Distributed Methods in Verification (PDMC'06), Volume 4346 of LNCS, pages 301–315, Springer Berlin Heidelberg, 2006.

[bibtex]
Erika Abraham, Marc Herbstritt, Bernd Becker, Martin Steffen. Memory-Aware Bounded Model Checking for Linear Hybrid Systems. 9th. Workshop for Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'06), pages 153–162, , 2006.
2005
DOI
[bibtex]
Erika Abraham, Bernd Becker, Felix Klaedke, Martin Steffen. Optimizing Bounded Model Checking for Linear Hybrid Systems. Verification, Model Checking, and Abstract Interpretation (VMCAI'05), Volume 3385 of LNCS, pages 396–412, Springer Berlin Heidelberg, 2005.
2004

[bibtex]
Erika Abraham, Bernd Becker, Felix Klaedke, Martin Steffen. Optimizing Bounded Model Checking for Linear Hybrid Systems. Technical report at Albert-Ludwigs-Universität Freiburg, Fakultät für Angewandte Wissenschaften, Institut für Informatik number TR214, 2004.