Publications

2018

• Preprint

  Automated Verification of Neural Networks: Advances, Challenges and Perspectives

  Francesco Leofante, Nina Narodytska, Luca Pulina, Armando Tacchella

  PDF of Automated Verification of Neural Networks: Advances, Challenges and PerspectivesRWTH record for Automated Verification of Neural Networks: Advances, Challenges and PerspectivesBibTeX for Automated Verification of Neural Networks: Advances, Challenges and Perspectives
• Journal article

  Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics

  Francesco Leofante, Erika Ábrahám, Tim Dieter Niemüller, Gerhard Lakemeyer, Armando Tacchella

  Information systems frontiers

  RWTH record for Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in LogisticsBibTeX for Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics
• Conference paper

  Improving Generalization in Software IC3

  Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen

  Model checking software

  RWTH record for Improving Generalization in Software IC3BibTeX for Improving Generalization in Software IC3
• Conference paper

  Optimal Multi-robot Task Planning: from Synthesis to Execution (and Back)

  Francesco Leofante

  Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

  RWTH record for Optimal Multi-robot Task Planning: from Synthesis to Execution (and Back)BibTeX for Optimal Multi-robot Task Planning: from Synthesis to Execution (and Back)
• Conference paper

  Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations

  Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Ábrahám, Joost-Pieter Katoen

  Formal Methods

  RWTH record for Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and RecommendationsBibTeX for Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
• Conference paper

  Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain

  Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow

  Formal Methods

  RWTH record for Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive DomainBibTeX for Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain
• Conference paper

  Sound Value Iteration

  Tim Quatmann, Joost-Pieter Katoen

  Computer Aided Verification

  PDF of Sound Value IterationRWTH record for Sound Value IterationBibTeX for Sound Value Iteration
• Conference paper

  Monitoring CTMCs by Multi-clock Timed Automata

  Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan

  Computer Aided Verification

  PDF of Monitoring CTMCs by Multi-clock Timed AutomataRWTH record for Monitoring CTMCs by Multi-clock Timed AutomataBibTeX for Monitoring CTMCs by Multi-clock Timed Automata
• Journal article

  Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms

  Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo

  Journal of the ACM

  RWTH record for Weakest Precondition Reasoning for Expected Runtimes of Randomized AlgorithmsBibTeX for Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
• Conference paper

  Symbolic Liveness Analysis of Real-World Software

  Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, Klaus Wehrle

  Computer Aided Verification

  PDF of Symbolic Liveness Analysis of Real-World SoftwareRWTH record for Symbolic Liveness Analysis of Real-World SoftwareBibTeX for Symbolic Liveness Analysis of Real-World Software
• Conference paper

  Let this Graph Be Your Witness! : An Attestor for Verifying Java Pointer Programs

  Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll

  Computer Aided Verification

  RWTH record for Let this Graph Be Your Witness! : An Attestor for Verifying Java Pointer ProgramsBibTeX for Let this Graph Be Your Witness! : An Attestor for Verifying Java Pointer Programs
• Conference paper

  Branching Bisimulation and Concurrent Object Verification

  Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin, Gaoang Liu, Hao Wu

  48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks

  RWTH record for Branching Bisimulation and Concurrent Object VerificationBibTeX for Branching Bisimulation and Concurrent Object Verification
• Preprint

  Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs

  Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll

  PDF of Quantitative Separation Logic : A Logic for Reasoning about Probabilistic ProgramsRWTH record for Quantitative Separation Logic : A Logic for Reasoning about Probabilistic ProgramsBibTeX for Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs
• Conference paper

  One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs

  Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk

  Application and theory of petri nets and concurrency

  RWTH record for One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNsBibTeX for One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs
• Conference paper

  How long, O Bayesian network, will I sample thee? : A program analysis perspective on expected sampling times

  Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

  Programming Languages and Systems

  PDF of How long, O Bayesian network, will I sample thee? : A program analysis perspective on expected sampling timesRWTH record for How long, O Bayesian network, will I sample thee? : A program analysis perspective on expected sampling timesBibTeX for How long, O Bayesian network, will I sample thee? : A program analysis perspective on expected sampling times
• Journal article

  A new proof rule for almost-sure termination

  Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen

  Proceedings of the ACM on Programming Languages

  RWTH record for A new proof rule for almost-sure terminationBibTeX for A new proof rule for almost-sure termination
• Conference paper

  Graph-Based Shape Analysis Beyond Context-Freeness

  Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll

  Software engineering and formal methods

  RWTH record for Graph-Based Shape Analysis Beyond Context-FreenessBibTeX for Graph-Based Shape Analysis Beyond Context-Freeness
• Conference paper

  Multi-cost Bounded Reachability in MDP

  Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann

  Tools and Algorithms for the Construction and Analysis of Systems

  PDF of Multi-cost Bounded Reachability in MDPRWTH record for Multi-cost Bounded Reachability in MDPBibTeX for Multi-cost Bounded Reachability in MDP
• Conference paper

  Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis

  Stefan Schupp, Erika Ábrahám

  Tools and Algorithms for the Construction and Analysis of Systems

  PDF of Efficient Dynamic Error Reduction for Hybrid Systems Reachability AnalysisRWTH record for Efficient Dynamic Error Reduction for Hybrid Systems Reachability AnalysisBibTeX for Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis
• Conference paper

  Spread the Work : Multi-threaded Safety Analysis for Hybrid Systems

  Stefan Schupp, Erika Ábrahám

  Software engineering and formal methods

  RWTH record for Spread the Work : Multi-threaded Safety Analysis for Hybrid SystemsBibTeX for Spread the Work : Multi-threaded Safety Analysis for Hybrid Systems
• Journal article

  Modular strategic SMT solving with SMT-RAT

  Gereon Kremer, Erika Ábrahám

  Acta Universitatis Sapientiae

  PDF of Modular strategic SMT solving with SMT-RATRWTH record for Modular strategic SMT solving with SMT-RATBibTeX for Modular strategic SMT solving with SMT-RAT
• Conference paper

  Context-Dependent Reachability Analysis for Hybrid Systems

  Stefan Schupp, Justin Winkens, Erika Ábrahám

  2018 IEEE 19th International Conference on Information Reuse and Integration for Data Science

  RWTH record for Context-Dependent Reachability Analysis for Hybrid SystemsBibTeX for Context-Dependent Reachability Analysis for Hybrid Systems
• Journal article

  Fast Dynamic Fault Tree Analysis by Model Checking Techniques

  Matthias Volk, Sebastian Junges, Joost-Pieter Katoen

  IEEE transactions on industrial informatics

  RWTH record for Fast Dynamic Fault Tree Analysis by Model Checking TechniquesBibTeX for Fast Dynamic Fault Tree Analysis by Model Checking Techniques
• Journal article

  Conditioning in Probabilistic Programming

  Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle Mciver

  ACM transactions on programming languages and systems

  RWTH record for Conditioning in Probabilistic ProgrammingBibTeX for Conditioning in Probabilistic Programming
• Journal article

  Positive root isolation for poly-powers by exclusion and differentiation

  Cheng-Chao Huang, Jing-Cao Li, Ming Xu, Zhi-Bin Li

  Journal of symbolic computation

  RWTH record for Positive root isolation for poly-powers by exclusion and differentiationBibTeX for Positive root isolation for poly-powers by exclusion and differentiation