Publications

Publications

2018

[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), [to appear], Volume of PACM, , 2018.
2017

[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. Proc. of CDC, IEEE, 2017.
DOI
[bibtex]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Fast Dynamic Fault Tree Analysis by Model Checking Techniques. IEEE Transactions on Industrial Informatics, 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, Springer, 2017.

[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). Prof. of ICTAC, Volume of LNCS, pages 1-2, Springer, 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), 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 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, 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.

[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.

[bibtex]
Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees. 2017 AIAA SPACE Forum, to be published, 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 of CEUR-WS, , 2017.

[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, CEUR-WS, 2017.

[bibtex]
Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming. In , ACM Transactions on Programming Languages and Systems (TOPLAS), [to appear], 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.
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'16). 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.
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.
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]
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]
Francesco Leofante, 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.
DOI
[bibtex]
Francesco Leofante, Armando Tacchella. Learning in Physical Domains: Mating Safety Requirements and Costly Sampling. AI*IA 2016: Advances in Artificial Intelligence - XVth International Conference of the Italian Association for Artificial Intelligence, Genova, Italy, November 29 - December 1, 2016, Proceedings, Volume 10037 of LNCS, pages 539–552, Springer, 2016.

[bibtex]
Francesco Leofante, Luca Pulina, Armando Tacchella. Learning with Safety Requirements: State of the Art and Open Questions. Proceedings of the 23rd RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2016 (RCRA 2016) A workshop of the XV International Conference of the Italian Association for Artificial, Volume 1745 of CEUR Workshop Proceedings, pages 11–25, CEUR-WS.org, 2016.

[bibtex]
Nicolò Arnaldi, Chiara Barone, Franco Fusco, Francesco Leofante, Armando Tacchella. Autonomous Driving and Undergraduates: an Affordable Setup for Teaching Robotics. Proceedings of the 3rd Italian Workshop on Artificial Intelligence and Robotics - A workshop of the XV International Conference of the Italian Association for Artificial Intelligence, AIRO@AI*IA 2016, Genova, Italy, November 28, 2016., Volume 1834 of CEUR Workshop Proceedings, pages 5–9, CEUR-WS.org, 2016.
Show all