The paper entitled “Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification” by Marcel Hark, Jürgen Giesl, Benjamin Kaminski and Joost-Pieter Katoen has been accepted for the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020). The paper tackles the problem of finding lower bounds of expected values / run-times […]
The paper entitled “The 10,000 Facets of MDP Model Checking” by Christel Baier, Holger Hermanns and Joost-Pieter Katoen just (finally) appeared in LNCS volume 10,000, Computing and Software Science: State of the Art and Perspectives.
The paper “Model Checking Revamped: On the Automated Synthesis of Markov Chains” by Milan Ceska, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen has been published in LNCS 11500, From Reactive Systems to Cyber-Physical Systems – Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday. The paper surveys a CEGAR and CEGIS approach towards the […]
The paper entitled “Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems” by Mingzhang Huang, Hongfei Fu (both from Shanghai Jiao Tong University), Joost-Pieter Katoen has been accepted to the journal Information and Computation. The paper shows that proving probabilistic similarity between a finite probabilistic transition system (specification) and a probabilistic pushdown automaton (implementationI is EXPTIME-complete.
The paper “Synergizing Reliability Modeling Languages: BDMPs Without Repairs and DFTs” by Shahid Khan, Joost-Pieter Katoen, Matthias Volk, and Marc Bouissou (EDF) has been accepted at the 24th IEEE Pacific Rim Int. Symp. on Dependable Computing, Kyoto, 2019. The paper discusses rules to transform the reliability formalism BDMPs into dynamic fault trees, applies this to […]
The paper “A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas” by Matthias Volk, Norman Weik, Joost-Pieter Katoen and Nils Nießen has been awarded the best paper award at the 24th International Conference on Formal Methods for Industrial-Critical Systems (FMICS 2019), Amsterdam, The Netherlands.
The paper “Formal Verification of Rewriting Rules for Dynamic Fault Trees” by Yassmeen Elderhalli (Concordia Univ.), Matthias Volk, Osman Hasan (Concordia), Joost-Pieter Katoen and Sofiene Tahar (Concordia) has been accepted at the 17th International Conference on Software Engineering andFormal Methods (SEFM 2019). The paper models a set of existing rewrite rules for DFTs in HOL4 […]
The paper “Are Parametric Markov Chains Monotonic?” by Jip Spel, Sebastian Junges and Joost-Pieter Katoen has been accepted at ATVA 2019. The paper presents a simple algorithm to check whether reachability probabilities in parametric Markov chains are monotonic in (some of) the parameters.
The paper “On the Complexity of Reachability in Parametric Markov Decision Processes” by Tobias Winkler, Sebastian Junges, Guillermo A. Pérez and Joost-Pieter Katoen has been accepted at CONCUR 2019. The paper addresses the complexity of various synthesis problems for parametric Markov decision processes.
The paper “Counterexample-Driven Synthesis for Probabilistic Program Sketches” by Milan Ceska, Christian Dehnert, Sebastian Junges and Joost-Pieter Katoen has been accepted for the FM 2019 World Congress. The paper presents a CEGIS-inspired technique to automatically synthesize probabilistic programs from sketches, i.e., programs with holes.