Publications

Publications

2018

[bibtex]
Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-based Conditioning of Probabilistic Data Integration. Proc. of the 12th International Conference on Scalable Uncertainty Management (SUM 2018), Volume of LNAI, Springer, 2018.

[bibtex]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Synthesis in pMDPs: A Tale of 1001 Parameters. Proc. of ATVA, Volume of LNCS, Springer, 2018.

[bibtex]
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, Mary Hayhoe. Model Checking For Safe Navigation Among Humans. Proc. of QEST, Volume of LNCS, , 2018.

[bibtex]
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs via Parameter Synthesis. Proc. of UAI, , 2018.

[bibtex]
Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan. Monitoring CTMCs By Multi-Clock Timed Automata. Proc. of CAV, Volume of LNCS, , 2018.

[bibtex]
Tim Quatmann, Joost-Pieter Katoen. Sound Value Iteration. Prof. of CAV, Volume of LNCS, Springer, 2018.

[bibtex]
Philipp Berger, Joost-Pieter Katoen, Erika Abraham, Thomas Rambow, Md Tawhid Bin Waez. Verifying Auto-Generated C Code from Simulink. Proc. of Formal Methods Symposium (FM 2018), Volume of LNCS, Springer, 2018.

[bibtex]
Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Abraham, Joost-Pieter Katoen. Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations. Proc. of Formal Methods Symposium (FM 2018), Volume of LNCS, Springer, 2018.

[bibtex]
Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk. One Net Fits All: A unifying semantics of DFTs using GSPNs. Proc. of Petri Nets, Volume of LNCS, Springer, 2018.

[bibtex]
Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin, Gaoang Liu, Hao Wu. Branching Bisimulation and Concurrent Object Verification. Proc. of the 48th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), IEEE, 2018.
Download
[bibtex]
Christel Baier, Holger Hermanns, Joost-Pieter Katoen. The 10,000 Facets of MDP Model Checking. In , Computing and Software Science, Volume 10000 of LNCS, 2018.
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, 2018.
Download
[bibtex]
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times.. Proc. of the 27th European Symposium on Programming (ESOP 2018), Volume 10801 of LNCS, pages 186-213, Springer, 2018.

[bibtex]
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-Cost Bounded Reachability in MDPs. Proc. of TACAS, Volume 10805 of LNCS, , 2018.
Link
[bibtex]
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic. Technical report at arxiv number 1802.10467, 2018.
DOI
[bibtex]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Fast Dynamic Fault Tree Analysis by Model Checking Techniques. IEEE Transactions on Industrial Informatics 14(1), pages 370-379, 2018.
DOI
[bibtex]
Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming. ACM Transactions on Programming Languages and Systems (TOPLAS) 40(1), pages 4:1-4:50, 2018.
DOI
[bibtex]
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen. A New Proof Rule for Almost-Sure Termination. Proc. of the 45th Symposium on Principles of Programming Languages (POPL 2018), pages 33:1-33:28, 2018.
Download
[bibtex]
Stefan Schupp, Erika Abraham. Efficient dynamic error reduction for hybrid systems reachability analysis. Proc. of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), Volume of LNCS, Springer, 2018.

[bibtex]
Stefan Schupp, Francesco Leofante, Erika Abraham, Armando Tacchella. Robot Swarms as Hybrid Systems. Proceedings 4th International Workshop on Symbolic and Numerical Methods for Reachability Analysis, SNR@ETAPS 2018, , 2018.
DOI
[bibtex]
Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs. Proc. CAV 2018, Part I/II, Volume 10980/10981 of LNCS, Springer, 2018.
DOI
[bibtex]
Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, Klaus Wehrle. Symbolic Liveness Analysis of Real-World Software. Proc. CAV 2018, Part I/II, Volume 10980/10981 of LNCS, Springer, 2018.
DOI
[bibtex]
Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Graph-Based Shape Analysis Beyond Context-Freeness. Proc. 16th Int. Conf. on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, pages 271–286, Springer, 2018.

[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. Journal of the ACM [to appear], 2018.
Download
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the Hardness of Analyzing Probabilistic Programs. Acta Informatica [to appear], 2018.
DOI
[bibtex]
Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen. Improving Generalization in Software IC3. SPIN 2018, Volume 10869 of LNCS, pages 85–102, Springer, 2018.

[bibtex]
Francesco Leofante. Guaranteed Plans for Multi-Robot Systems via Optimization Modulo Theories. Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, New Orleans, Louisiana, USA, February 2-7, 2018, , 2018.
DOI
[bibtex]
Stefan Schupp, Erika Abraham. Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems. Software Engineering and Formal Methods (SEFM'18), Volume 10886 of LNCS, pages 89–104, Springer, 2018.
Download
[bibtex]
Francesco Leofante, Nina Narodytska, Luca Pulina, Armando Tacchella. Automated Verification of Neural Networks: Advances, Challenges and Perspectives. Technical report at RWTH Aachen University number , 2018.

[bibtex]
Francesco Leofante, Erika Abraham, Armando Tacchella. Task Planning with OMT: an Application to Production Logistics. Proceedings of the 14th International Conference on integrated Formal Methods, Volume of LNCS, Springer, 2018.

[bibtex]
Erika Abraham, Borzoo Bonakdarpour. HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties. Proc. of the 15th International Conference on Quantitative Evaluation of SysTems (QEST 2018), Volume of LNCS, Springer, 2018.
DOI
[bibtex]
Francesco Leofante. Optimal Multi-robot Task Planning: from Synthesis to Execution (and Back). Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden., pages 5771–5772, , 2018.
2017
Download
[bibtex]
Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker. Motion Planning under Partial Observability using Game-Based Abstraction. IEEE 56th Annual Conference on Decision and Control (CDC), pages 2201-2208, IEEE, 2017.
Download
[bibtex]
Joost-Pieter Katoen, Marielle Stoelinga. Boosting Fault Tree Analysis by Formal Methods. ModelEd, TestEd, TrustEd (Festschrift Ed Brinksma), Volume 10500 of LNCS, pages 368-389, Springer, 2017.
DOI
[bibtex]
Joost-Pieter Katoen, Rom Langerak, Arend Rensink editors. ModelEd, TestEd, TrustEd (Festschrift Ed Brinksma). Springer, Volume 10500 of LNCS, 2017.
Download
[bibtex]
Joost-Pieter Katoen. Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract). Proc. of ICTAC, Volume of LNCS, pages 1-2, Springer, 2017.
DOI
[bibtex]
Christina Jansen. Static Analysis of Pointer Programs – Linking Graph Grammars and Separation Logic. Phd Thesis at RWTH Aachen University, 2017.
Download
[bibtex]
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems. Proc. of SAFECOMP, Volume 10488 of LNCS, pages 3–19, Springer, 2017.
Download
[bibtex]
Saba Aflaki, Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Arne Storjohann. Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms. Proc. of 36th IEEE Symposium on Reliable Distributed Systems (SRDS), pages 94–103, IEEE CS (Recipient of Best Paper Award), 2017.
Download
[bibtex]
Joost-Pieter Katoen, Falak Sher. Modal Stochastic Games: Abstraction-Refinement of Probabilistic Automata. Models, Algorithms, Logics and Tools (Festschrift Kim Larsen), Volume 10460 of LNCS, pages 426-448, Springer, 2017.
Link
[bibtex]
Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker. Proc. of CAV, Volume 10427 of LNCS, pages 592–600, Springer, 2017.
Link
[bibtex]
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives. Proc. of Computer Aided Verification (CAV), Volume 10426 of LNCS, pages 140–159, Springer, 2017.
DOI
[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), pages 1-12, IEEE, 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 10206 of LNCS, pages 133-150, Springer, 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 (2), Volume 10206 of LNCS, pages 151-168, Springer, 2017.
Link
[bibtex]
Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness. Technical report at arxiv number 1705.03754, 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.
Download
[bibtex]
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate. Quantitative Model Checking of Controlled Discrete-Time Markov Processes. Information and Computation 253, pages 1-35, 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 29(4), pages 651-703, 2017.
DOI
[bibtex]
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. Proc. ESOP 2017, Volume 10201 of LNCS, pages 611–638, Springer, 2017.
DOI
[bibtex]
Louis Wachtmeister, Thomas Noll. Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications. Proc. Int. Workshop on MILS: Architecture and Assurance for Secure Systems, Zenodo, 2017.
Download
[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 10227 of LNCS, pages 288–294, Springer International Publishing, 2017.
Download
[bibtex]
Stefan Schupp, Johanna Nellen, Erika Abraham. Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis. Proc. of the 15th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'17), Volume 250 of EPTCS, pages 1–14, Open Publishing Association, 2017.
DOI
[bibtex]
Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees. 2017 AIAA SPACE Forum, Volume AIAA 2017-5163, American Institute of Aeronautics and Astronautics, 2017.
Link
[bibtex]
Marco Bozzano, Harold Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. The COMPASS 3.0 Toolset (short paper). Proc. 5th Int. Symp. on Model-Based Safety and Assessment (IMBSA 2017), , 2017.
DOI
[bibtex]
Marco Bozzano, Harold Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. Formal Methods for Aerospace Systems: Achievements and Challenges. In Shin Nakajima, Jean-Pierre Talpin, Masumi Toyoshima, Huafeng Yu editors, Cyber-Physical System Design from an Architecture Analysis Viewpoint: Communications of NII Shonan Meetings, Springer Singapore, 2017.
Download
[bibtex]
Erika Abraham. Techniques and Tools for Hybrid Systems Reachability Analysis. Proc. Numerical Software Verification (NSV'17), , 2017.
Download
[bibtex]
Tarik Viehmann, Gereon Kremer, Erika Abraham. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving. Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, Volume 1974 of CEUR Workshop Proceedings, CEUR-WS.org, 2017.
Link
[bibtex]
Erika Abraham, Jasper Nalbach, Gereon Kremer. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, Volume 1974 of CEUR Workshop Proceedings, CEUR-WS.org, 2017.
DOI
[bibtex]
Erika Abraham, Hadas Kress-Gazit, Lorenzo Natale, Armando Tacchella editors. Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Volume 7/2 of Dagstuhl Reports, pages 48–63, 2017.
Download
[bibtex]
Tim Niemueller, Gerhard Lakemeyer, Francesco Leofante, Erika Abraham. Towards CLIPS-based Task Execution and Monitoring with SMT-based Planning and Optimization. 5th Workshop on Planning and Robotics at ICAPS, , 2017.
Download
[bibtex]
Hao Wu. Industrial Applications of Probabilistic Model Checking. Phd Thesis at RWTH Aachen University, 2017.
Link
[bibtex]
Marieke Huisman, Thomas Noll, Makoto Tatsuta. Analysis and Verification of Pointer Programs. Technical report at National Institute of Informatics number 2017-14, 2017.
Link
[bibtex]
Francesco Leofante, Erika Abraham, Tim Niemueller, Gerhard Lakemeyer, Armando Tacchella. On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories. 2017 IEEE International Conference on Information Reuse and Integration, IRI 2017, San Diego, CA, USA, August 4-6, 2017, pages 403–410, IEEE Computer Society, 2017.
DOI
[bibtex]
Radu Calinescu, Marco Autili, Javier Ciamara, Antinisca Di Marco, Simos Gerasimou, Paola Inverardi, Alexander Perucci, Nils Jansen, Joost-Pieter Katoen, Marta Kwiatkowska, Ole J. Mengshoel, Romina Spalazzese, Massimo Tivoli. Synthesis and Verification of Self-aware Computing Systems. In , Self-Aware Computing Systems, pages 337-373, 2017.
DOI
[bibtex]
Erika Abraham, James H. Davenport, Pascal Fontaine editors. Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation (SC2 2016), Timisoara, Romania, September 24, 2016.. CEUR-WS.org, Volume 1804 of CEUR Workshop Proceedings, 2017.
DOI
[bibtex]
Erika Abraham, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler. SC-square: when Satisfiability Checking and Symbolic Computation join forces. Proc. of the 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE'17), Volume 51 of EPiC Series in Computing, pages 6–10, EasyChair, 2017.
Link
[bibtex]
Erika Abraham, Sergiy Bogomolov editors. Proc. of the 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, SNR@ETAPS 2017. , Volume 247 of EPTCS, 2017.

[bibtex]
Erika Abraham, Tudor Jebelean. Adapting Cylindrical Algebraic Decomposition for Proof Specific Tasks. Proc. of the 10th International Conference on Applied Informatics (ICAI'17), , 2017.

[bibtex]
Jannik Hüls, Stefan Schupp, Anne Remke, Erika Abraham. Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro. Proc. of the 11th EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS'17), , 2017.
Show all