Travelled to:1 × Denmark
1 × Estonia
1 × Norway
1 × Portugal
1 × Sweden
2 × Austria
2 × France
2 × Switzerland
2 × The Netherlands
2 × United Kingdom
3 × Spain
5 × Italy
5 × USA
6 × Germany
Collaborated with:H.Hermanns B.L.Kaminski C.Baier C.Dehnert ∅ T.Quatmann T.Han C.Matheja D.Latella T.Noll B.R.Haverkort S.Junges M.Leucker R.Wimmer N.Jansen E.Ábrahám H.C.Bohnenkamp D.N.Jansen H.Wu B.Becker V.Y.Nguyen D.Peled A.McIver J.Meyer-Kayser M.Siegle C.Jansen T.Chen A.Mereacre M.Massink T.C.Ruys K.Batz B.Bollig C.Kern T.N.0001 A.Wijs D.Bošnački L.Song L.Zhang D.Parker B.D.Theelen M.R.Neuhäußer M.Stoelinga M.Bozzano A.Cimatti M.Roveri J.Heinen L.Meinicke C.C.Morgan D.Klink V.Wolf T.Kemna I.S.Zapreev R.D.Nicola R.Klaren P.R.D'Argenio J.Tretmans A.Nymeyer Y.Westra H.Alblas F.Olmedo M.V.0001 C.Morgan M.Hark J.Giesl T.Brázdil S.Kiefer A.Kucera P.Novotný T.Santen D.Seifert M.Esteve B.Postma Y.Yushtein B.Barbot R.Langerak Y.Feng H.Li B.Xia N.Zhan H.Arndt D.Neider D.R.Piegdon B.Delahaye K.G.Larsen A.Legay M.L.Pedersen F.Sher A.Wasowski F.Corzilius M.Volk H.Bruintjes
Talks about:model (19) time (16) probabilist (11) markov (10) check (8) automata (6) program (6) analysi (6) continu (5) process (4)
Person: Joost-Pieter Katoen
DBLP: Katoen:Joost=Pieter
Facilitated 1 volumes:
EdContributed to:
2015
20152014
2014
2014
2013
2013
20132012
20122012
2011201120112010
20102010
2009
20092009200820072007
200620042004
200320012000
2000
2000200019981997
1996201620182017201720182018
201820192020Wrote 50 papers:
- CAV-2015-DehnertJJCVBKA #named #parametricity #probability #synthesis
- PROPhESY: A PRObabilistic ParamEter SYnthesis Tool (CD, SJ, NJ, FC, MV, HB, JPK, EÁ), pp. 214–231.
- FM-2015-QuatmannJDWAKB
- Counterexamples for Expected Rewards (TQ, NJ, CD, RW, EÁ, JPK, BB), pp. 435–452.
- CAV-2014-WijsKB #component #composition #graph
- GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (AW, JPK, DB), pp. 310–326.
- LICS-CSL-2014-BrazdilKKNK #automaton #multi #probability
- Zero-reachability in probabilistic multi-counter automata (TB, SK, AK, PN, JPK), p. 10.
- LICS-CSL-2014-KatoenSZ
- Probably safe or live (JPK, LS, LZ), p. 10.
- SFM-2014-AbrahamBDJKW #generative #markov #modelling #overview
- Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey (EÁ, BB, CD, NJ, JPK, RW), pp. 65–121.
- DATE-2013-KatoenNWSS #energy #modelling #optimisation
- Model-based energy optimization of automotive control systems (JPK, TN, HW, TS, DS), pp. 761–766.
- ESOP-2013-KatoenP #concurrent #implementation #modelling #probability
- Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems (JPK, DP), pp. 411–430.
- VMCAI-2013-DehnertKP #bisimulation #markov #modelling #smt
- SMT-Based Bisimulation Minimisation of Markov Models (CD, JPK, DP), pp. 28–47.
- DATE-2012-TheelenKW #data flow #model checking
- Model checking of Scenario-Aware Dataflow with CADP (BDT, JPK, HW), pp. 653–658.
- ICSE-2012-EsteveKNPY #analysis #correctness #dependence #performance #safety
- Formal correctness, safety, dependability, and performance analysis of a satellite (MAE, JPK, VYN, BP, YY), pp. 1022–1031.
- TACAS-2012-WimmerJABK #markov #modelling
- Minimal Critical Subsystems for Discrete-Time Markov Models (RW, NJ, EÁ, BB, JPK), pp. 299–314.
- LATA-2011-JansenHKN #normalisation
- A Local Greibach Normal Form for Hyperedge Replacement Grammars (CJ, JH, JPK, TN), pp. 323–335.
- TACAS-2011-BarbotCHKM #linear #model checking #performance #realtime
- Efficient CTMC Model Checking of Linear Real-Time Objectives (BB, TC, TH, JPK, AM), pp. 128–142.
- VMCAI-2011-DelahayeKLLPSW #automaton #probability
- Abstract Probabilistic Automata (BD, JPK, KGL, AL, MLP, FS, AW), pp. 324–339.
- CAV-2010-BolligKKLNP #automaton #framework #learning #named
- libalf: The Automata Learning Framework (BB, JPK, CK, ML, DN, DRP), pp. 360–364.
- CAV-2010-BozzanoCKNNRW #model checking
- A Model Checker for AADL (MB, AC, JPK, VYN, TN, MR, RW), pp. 562–565.
- SAS-2010-KatoenMMM #automation #generative #invariant #probability #source code
- Linear-Invariant Generation for Probabilistic Programs: — Automated Support for Proof-Based Methods (JPK, AM, LM, CCM), pp. 390–406.
- VMCAI-2010-Katoen #model checking #probability #roadmap
- Advances in Probabilistic Model Checking (JPK), p. 25.
- ESEC-FSE-2009-BozzanoCRKNN #evaluation #modelling #performance #verification
- Verification and performance evaluation of aadl models (MB, AC, MR, JPK, VYN, TN), pp. 285–286.
- FoSSaCS-2009-NeuhausserSK #markov #nondeterminism #process
- Delayed Nondeterminism in Continuous-Time Markov Decision Processes (MRN, MS, JPK), pp. 364–379.
- LICS-2009-ChenHKM #automaton #markov #model checking #specification
- Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications (TC, TH, JPK, AM), pp. 309–318.
- DATE-2008-Katoen #analysis #design #embedded #evaluation #modelling #roadmap
- Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques (JPK), pp. 86–87.
- CAV-2007-KatoenKLW #abstraction #markov
- Three-Valued Abstraction for Continuous-Time Markov Chains (JPK, DK, ML, VW), pp. 311–324.
- TACAS-2007-BohnenkampHK #named
- motor: The modestTool Environment (HCB, HH, JPK), pp. 500–504.
- TACAS-2007-BolligKKL #design #game studies #learning #modelling #synthesis
- Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning (BB, JPK, CK, ML), pp. 435–450.
- TACAS-2007-HanK #model checking #probability
- Counterexamples in Probabilistic Model Checking (TH, JPK), pp. 72–86.
- TACAS-2007-KatoenKZJ #bisimulation #model checking #probability
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking (JPK, TK, ISZ, DNJ), pp. 87–101.
- QAPL-2005-NicolaKLM06 #logic #performance #towards
- Towards a Logic for Performance and Mobility (RDN, JPK, DL, MM), pp. 161–175.
- SFM-2004-KatoenBKH #analysis #embedded
- Embedded Software Analysis with MOTOR (JPK, HCB, RK, HH), pp. 268–294.
- TACAS-2004-BaierHHK #bound #markov #performance #process #reachability
- Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes (CB, BRH, HH, JPK), pp. 61–76.
- UML-2003-JansenHK #uml
- A QoS-Oriented Extension of UML Statecharts (DNJ, HH, JPK), pp. 76–91.
- TACAS-2001-RuysLKLM #algebra #analysis #partial order #probability #process #using
- First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders (TCR, RL, JPK, DL, MM), pp. 220–235.
- CAV-2000-BaierHHK #analysis #markov #model checking
- Model Checking Continuous-Time Markov Chains by Transient Analysis (CB, BRH, HH, JPK), pp. 358–372.
- ICALP-2000-BaierHHK #logic #on the
- On the Logical Characterisation of Performability Properties (CB, BRH, HH, JPK), pp. 780–792.
- IFM-2000-HermannsKMS #algebra #model checking #probability #process #towards
- Towards Model Checking Stochastic Process Algebra (HH, JPK, JMK, MS), pp. 420–439.
- TACAS-2000-HermannsKMS #markov #model checking
- A Markov Chain Model Checker (HH, JPK, JMK, MS), pp. 347–362.
- ICALP-1998-BaierKL #concurrent #metric #realtime #semantics
- Metric Semantics for True Concurrent Real Time (CB, JPK, DL), pp. 568–579.
- TACAS-1997-DArgenioKRT #bound #exclamation #protocol
- The Bounded Retransmission Protocol Must Be on Time! (PRD, JPK, TCR, JT), pp. 416–431.
- CC-1996-NymeyerKWA #code generation
- Code Generation = A* + BURS (AN, JPK, YW, HA), pp. 160–176.
- ESOP-2016-KaminskiKMO #probability #reasoning #source code
- Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs (BLK, JPK, CM, FO), pp. 364–389.
- ESOP-2018-BatzKKM #how #network #program analysis
- How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times (KB, BLK, JPK, CM), pp. 186–213.
- CAV-2017-QuatmannJK #automaton #markov #multi
- Markov Automata with Multiple Objectives (TQ, SJ, JPK), pp. 140–159.
- CAV-2017-DehnertJK0 #model checking #probability
- A Storm is Coming: A Modern Probabilistic Model Checker (CD, SJ, JPK, MV0), pp. 592–600.
- CAV-2018-FengKLXZ #automaton #monitoring #multi
- Monitoring CTMCs by Multi-clock Timed Automata (YF, JPK, HL, BX, NZ), pp. 507–526.
- CAV-2018-QuatmannK
- Sound Value Iteration (TQ, JPK), pp. 643–661.
- CAV-2018-ArndtJKMN #exclamation #graph #java #pointer #source code #verification
- Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs (HA, CJ, JPK, CM, TN0), pp. 3–11.
- POPL-2018-McIverMKK #proving #termination
- A new proof rule for almost-sure termination (AM, CM, BLK, JPK), p. 28.
- POPL-2019-BatzKKMN #logic #pointer #probability #reasoning #source code
- Quantitative separation logic: a logic for reasoning about probabilistic pointer programs (KB, BLK, JPK, CM, TN0), p. 29.
- POPL-2020-HarkKGK #bound #induction #probability #verification
- Aiming low is harder: induction for lower bounds in probabilistic program verification (MH, BLK, JG, JPK), p. 28.