Publications

Publications

2020

[bibtex]
Marcel Hark, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Jürgen Giesl. Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification. Proceedings of the ACM on Programming Languages [to appear], 2020.
DownloadLink
[bibtex]
Erika Abraham, James H. Davenport, Matthew England, Gereon Kremer. Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings. Journal of Logical and Algebraic Methods in Programming, 2020.
2019
DownloadLink
[bibtex]
Christel Baier, Holger Hermanns, Joost-Pieter Katoen. The 10,000 Facets of MDP Model Checking. In , Computing and Software Science, pages 420-451, Volume 10000 of LNCS, 2019.

[bibtex]
Milan Ceska, Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen. Counterexample-Driven Synthesis for Probabilistic Program Sketches. Proc. of FM, , 2019.
DOIDownloadLink
[bibtex]
Mingzhang Huang, Hongfei Fu, Joost-Pieter Katoen. Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems. Information and Computation 268, 2019.
DOI
[bibtex]
Yassmeen Elderhalli, Matthias Volk, Osman Hasan, Joost-Pieter Katoen, Sofiène Tahar. Formal Verification of Rewriting Rules for Dynamic Fault Trees. Proc. of SEFM, Volume 11724 of LNCS, pages 513–531, Springer, 2019.

[bibtex]
Tobias Winkler, Sebastian Junges, Guillermo A Perez, Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes. Proc. of CONCUR, , 2019.
DOI
[bibtex]
Matthias Volk, Norman Weik, Joost-Pieter Katoen, Nils Nießen. A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas. Proc. of FMICS, Volume 11687 of LNCS, pages 40–58, Springer, 2019.
DOI
[bibtex]
Gereon Kremer, Erika Abraham. Fully Incremental Cylindrical Algebraic Decomposition. Journal of Symbolic Computation (Available online 29 July 2019), 2019.
DOILink
[bibtex]
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Safety Analysis for Vehicle Guidance Systems with Dynamic Fault Trees. Reliability Engineering and System Safety 186, pages 37–50, 2019.
DownloadLink
[bibtex]
Souymodip Chakraborty. New Results on Probabilistic Verification: Automata, Logic and Satisfiability. Phd Thesis at RWTH Aachen University, 2019.

[bibtex]
Milan Ceska, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Shepherding Hordes of Markov Chains. Proc. of TACAS, Volume of LNCS, , 2019.
DOIDownloadLink
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the Hardness of Analyzing Probabilistic Programs. Acta Informatica 56(3), pages 255-285, 2019.
DownloadLink
[bibtex]
Harold Bruintjes. Model-Based Reliability Analysis of Aerospace Systems. Phd Thesis at RWTH Aachen University, 2019.
DownloadLink
[bibtex]
Benjamin Lucien Kaminski. Advanced Weakest Precondition Calculi for Probabilistic Programs. Phd Thesis at RWTH Aachen University, 2019.
DownloadLink
[bibtex]
Tim Lange. IC3 Software Model Checking. Phd Thesis at RWTH Aachen University, 2019.
DOI
[bibtex]
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic. Proceedings of the ACM on Programming Languages 3(POPL), pages 34:1-34:29, 2019.
DownloadLink
[bibtex]
Francesco Leofante, Nina Narodytska, Luca Pulina, Armando Tacchella. Automated Verification of Neural Networks: Advances, Challenges and Perspectives. Verification of Neural Networks (VNN19), AAAI Spring Symposia, , 2019.
DOI
[bibtex]
Liana Mikaelyan, Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing and Optimizing FDIR Recovery Strategies From Fault Trees. FTSCS 2018, Volume 1008 of CCIS, pages 37–54, Springer, 2019.
DOI
[bibtex]
Dario Guidotti, Francesco Leofante, Armando Tacchella, Claudio Castellini. Improving Reliability of Myocontrol Using Formal Verification. IEEE Transactions on Neural Systems and Rehabilitation Engineering, 2019.
DOI
[bibtex]
Marco Bozzano, Harold Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. COMPASS 3.0 (Tool paper). TACAS 2019, Volume 11427 of LNCS, pages 379–385, Springer, 2019.
DOI
[bibtex]
Dario Guidotti, Francesco Leofante, Armando Tacchella, Claudio Castellini. Repairing Learned Controllers with Convex Optimization: a Case Study. Proceedings of Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR), , 2019.
DOI
[bibtex]
Arthur Bit-Monnot, Francesco Leofante, Luca Pulina, Armando Tacchella. SMT-based Planning for Robots in Smart Factories. International Conference on Industrial Engineering and Other Applications of Applied Intelligent Systems (IEA/AIE), , 2019.
DOI
[bibtex]
Francesco Leofante, Stefan Schupp, Erika Abraham, Armando Tacchella. Engineeering Controllers for Swarm Robotics via Reachability Analysis in Hybrid Systems. 33rd International ECMS European Conference on Modelling and Simulation (ECMS'19), pages 407–413, European Council for Modeling and Simulation, 2019.
DOI
[bibtex]
Francesco Leofante, Erika Abraham, Tim Niemueller, Gerhard Lakemeyer, Armando Tacchella. Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics. Information Systems Frontiers 21(1), pages 87–107, 2019.
DOI
[bibtex]
Jens Katelaan, Christoph Matheja, Florian Zuleger. Effective Entailment Checking for Separation Logic with Inductive Definitions. TACAS, Volume 11428 of LNCS, pages 319-336, Springer, 2019.
DOI
[bibtex]
E. Moritz Hahn, Arnd Hartmanns, Christian Dehnert, Michaela Klauck, Joachim Klein, Jan Kretínský, David Parker, Tim Quatmann, Enno Ruijters, Marcel Steinmetz. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). TACAS 2019, Volume 11429 of LNCS, pages 69–92, Springer, 2019.
DOI
[bibtex]
Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, Enno Ruijters. The Quantitative Verification Benchmark Set. TACAS 2019, Volume 11427 of LNCS, pages 344–350, Springer, 2019.

[bibtex]
Jasper Nalbach, Gereon Kremer, Erika Abraham. On Variable Orderings in MCSAT for Non-linear Real Arithmetic. Proceedings of the 4th International Workshop on Satisfiability Checking and Symbolic Computation, , 2019.

[bibtex]
Gereon Kremer, Erika Abraham, Vijay Ganesh. On the Proof Complexity of MCSAT. Proceedings of the 4th International Workshop on Satisfiability Checking and Symbolic Computation, , 2019.
DOI
[bibtex]
Tim Lange, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen. IC3 Software Model Checking. Software Tools for Technology Transfer, 2019.
DOILink
[bibtex]
Stefan Schupp. State Set Representations and their Usage in the Reachability Analysis of Hybrid Systems. Phd Thesis at RWTH Aachen University, 2019.
DOI
[bibtex]
Mihaela Sighireanu, Juan A. Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomas Vojnar, Constantin Enea, Ondrej Lengal, Chong Gao, Zhilin Wu. SL-COMP: Competition of Solvers for Separation Logic. TACAS 2019, Volume 11429 of LNCS, pages 116–132, Springer, 2019.
DOI
[bibtex]
Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika Abraham, Md Tawhid Bin Waez, Thomas Rambow. Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development. Proc. of the 24th Int. Conf. on Formal Methods for Industrial Critical Systems (FMICS'19), Volume 11687 of LNCS, pages 59–75, Springer, 2019.
Show all