Publications

Publications

2017

[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations. Proc. of the 32nd Annual Symposium on Logic in Computer Science (LICS 2017), [to appear], 2017.
Link
[bibtex]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, Ufuk Topcu. Sequential Convex Programming for the Efficient Verification of Parametric MDPs. Proc. of TACAS, Volume of LNCS, , 2017.
Download
[bibtex]
Carlos E. Budde, Christian Dehnert, E. Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini. “JANI: Quantitative Model and Tool Interaction. Proc. of TACAS, Volume of LNCS, , 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.
Download
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations. Collected Abstracts of the 2nd Workshop on Probabilistic Programming Semantics (PPS 2017), 2017.
DOI
[bibtex]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Marielle Stoelinga. Fault Trees on a Diet: Automated Reduction by Graph Rewriting. Formal Aspects of Computing, pages 1–53, 2017.

[bibtex]
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. Proc. ESOP 2017, To be published, 2017.

[bibtex]
Louis Wachtmeister, Thomas Noll. Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications. Proc. MILS Workshop at embedded world Conference 2017, To be published, 2017.

[bibtex]
Stefan Schupp, Erika Abraham, Ibtissem Ben Makhlouf, Stefan Kowalewski. HyPro: A C++ Library for State Set Representations for Hybrid Systems Reachability Analysis. Proc. of the 9th NASA Formal Methods Symposium (NFM'17), Volume of LNCS, Springer International Publishing, 2017.
2016
Download
[bibtex]
Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga. Confluence Reduction for Markov Automata. Theoretical Computer Science 655(Part B), pages 193–219, 2016.
Download
[bibtex]
Joost-Pieter Katoen, Hao Wu. Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow. ACM Transactions on Embedded Computing Systems 22(1), pages 28, 2016.
Download
[bibtex]
Johanna Nellen. Analysis and Synthesis of Hybrid Systems in Control Engineering. Phd Thesis at RWTH Aachen University, 2016.
DOI
[bibtex]
Erika Abraham, Thi Mai Thuong Tran, Martin Steffen. Observable Interface Behavior and Inheritance. Mathematical Structures in Computer Science 26(3), pages 561–605, 2016.
Download
[bibtex]
Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen. Bounded Model Checking for Probabilistic Programs. Proc. of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, Springer, 2016.
DOI
[bibtex]
Johanna Nellen, Kai Driessen, Martin R. Neuhäußer, Erika Abraham, Benedikt Wolters. Two CEGAR-Based Approaches for the Safety Verification of PLC-Controlled Plants. Information Systems Frontiers 18(5), pages 927–952, 2016.
DOI
[bibtex]
Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever. Proc. of ATVA, Volume 9938 of LNCS, pages 50–67, Springer, 2016.
Download
[bibtex]
Victor Bos, Harold Bruintjes, Stefano Tonetta. Catalogue of System and Software Properties. Proc. of the 35th Int. Conf. on Computer Safety, Reliability and Security (SAFECOMP), Volume 9922 of LNCS, pages 88–101, Springer, 2016.
Link
[bibtex]
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu. Probabilistic Verification for Cognitive Models. Proc. of Cross-Disciplinary Challenges for Autonomous Systems (CDCAS), Volume of AAAI Technical Reports, AAAI Press, 2016.
Link
[bibtex]
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. Technical report at arXiv number 1610.07041, 2016.
DOI
[bibtex]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Advancing Dynamic Fault Tree Analysis. Proc. of the 35th Int. Conf. on Computer Safety, Reliability and Security (SAFECOMP), Volume 9922 of LNCS, pages 253–265, Springer, 2016.
Download
[bibtex]
Gereon Kremer, Florian Corzilius, Erika Abraham. A Generalised Branch-and-Bound Approach and its Application in SAT Modulo Nonlinear Integer Arithmetic. 18th International Workshop on Computer Algebra in Scientific Computing (CASC'16), Volume 9890 of LNCS, pages 315-335, Springer, 2016.
Download
[bibtex]
Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, James Gross. Model-Checking Assisted Protocol Design for Ultra-Reliable Low-Latency Wireless Networks. Proc. of the 35th Symp. on Reliable Distributed Systems (SRDS), pages 307–316, IEEE CS, 2016.
Download
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Inferring Covariances for Probabilistic Programs. Proc. of the 13th International Conference on Quantitative Evaluation of SysTems (QEST 2016), Volume 9826 of LNCS, pages 191-206, Springer, 2016.
DOI
[bibtex]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga. Uncovering Dynamic Fault Trees. Proc. of IEEE/IFIP Symposium on Dependable Systems and Networks (DSN), pages 299-310, IEEE CS, 2016.
Download
[bibtex]
Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs. Proc. of the 31st Annual Symposium on Logic in Computer Science (LICS 2016), pages 672-681, ACM, 2016.
Download
[bibtex]
Joost-Pieter Katoen. The Probabilistic Model Checking Landscape. Proc. of Logic in Computer Science (LICS), pages 31-46, ACM, 2016.
DOI
[bibtex]
Mohamed Amin Ben Sassi, Sriram Sankaranarayanan, Xin Chen, Erika Abraham. Linear Relaxations of Polynomial Positivity for Polynomial Lyapunov Function Synthesis. IMA Journal of Mathematical Control and Information 33(3), pages 723–756, 2016.
DOI
[bibtex]
Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs. Proc. of TACAS, Volume 9636 of LNCS, pages 130-146, Springer, 2016.
DOI
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs (EATCS Best Paper Award). Proc. of the 25th European Symposium on Programming (ESOP 2016), Volume 9632 of LNCS, pages 364 - 389, Springer, 2016.

[bibtex]
Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo. On the Semantic Intricacies of Conditioning. Collected Abstracts of the 1st Workshop on Probabilistic Programming Semantics (PPS 2016), 2016.
Download
[bibtex]
Anton J. Wijs, Joost-Pieter Katoen, Dragan Bosnacki. Efficient GPU Algorithms for Parallel Decomposition of Graphs into Strongly Connected and Maximal End Components. Formal Methods in System Design 48(3), pages 274-300, 2016.
DOI
[bibtex]
Erika Abraham, Marcello M. Bonsangue, Einar Broch Johnsen editors. Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. Springer International Publishing, Volume 9660 of LNCS, 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]
Erika Abraham, Pascal Fontaine, Thomas Sturm, Dongming Wang. Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471). Dagstuhl Reports 5(11), pages 71–89, 2016.
Download
[bibtex]
Souymodip Chakraborty, Joost-Pieter Katoen. On the Satisfiability of Some Simple Probabilistic Logics. Proc. of Logic in Computer Science (LICS), pages 56-66, ACM, 2016.
DOI
[bibtex]
Erika Abraham, Marieke Huisman editors. Proceedings of the 12th International Conference on Integrated Formal Methods (iFM'16). Springer International Publishing, Volume 9681 of LNCS, 2016.

[bibtex]
Erika Abraham, Sergiy Bogomolov editors. Proceedings of the 2016 International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR). IEEE, 2016.
DOI
[bibtex]
Erika Abraham, Gereon Kremer. Satisfiability Checking: Theory and Applications. Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM'16), Volume 9763 of LNCS, pages 9–23, Springer International Publishing, 2016.

[bibtex]
Luca Aceto, Tom Henzinger, Joost-Pieter Katoen, Wolfgang Thomas, Moshe Vardi. Viewpoints on "Logic activities in Europe", twenty years later. Bulletin of the EATCS 118, 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.

[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 meets Symbolic Computation. CoRR (Proc. of the 9th Conf. on Intelligent Computer Mathematics, CICM'16) abs/1607.08028, 2016.
DOI
[bibtex]
Erika Abraham, Klaus Havelund. Some Recent Advances in Automated Analysis. Software Tools for Technology Transfer 18(2), pages 121–128, 2016.
Download
[bibtex]
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate. Quantitative Model Checking of Controlled Discrete-Time Markov Processes. Information and Computation, 2016.
Download
[bibtex]
Hao Wu, Xiaoxiao Yang, Joost-Pieter Katoen. Performance Evaluation of Concurrent Data Structures. Prof. of Dependable Software Engineering: Theories, Tools, and Applications (SETTA), Volume 9984 of LNCS, pages 38–49, Springer, 2016.

[bibtex]
Florian Corzilius. Integrating Virtual Substitution into Strategic SMT Solving. Phd Thesis at RWTH Aachen University, 2016.

[bibtex]
Pascal Richter, David Laukamp, Levin Gerdes, Martin Frank, Erika Abraham. Heliostat Field Layout Optimization with Evolutionary Algorithms. Proc. of the 2nd Global Conference on Artificial Intelligence (GCAI'16), Volume 41 of EPiC Series in Computing, pages 240–252, EasyChair, 2016.
DOI
[bibtex]
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.
Download
[bibtex]
Erika Abraham, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro. Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies. Dependable Software Engineering: Theories, Tools, and Applications (SETTA'16), Volume 9984 of LNCS, pages 229–245, Springer, 2016.

[bibtex]
Erika Abraham. Symbolic Computation Techniques in Satisfiability Checking. Proc. of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16), pages 3–10, IEEE Computer Society, 2016.
Show all