Joost-Pieter Katoen

According to our database1, Joost-Pieter Katoen
  • authored at least 272 papers between 1989 and 2017.
  • has a "Dijkstra number"2 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2017
Quantitative model-checking of controlled discrete-time Markov processes.
Inf. Comput., 2017

Fault trees on a diet: automated reduction by graph rewriting.
Formal Asp. Comput., 2017

Motion Planning under Partial Observability using Game-Based Abstraction.
CoRR, 2017

Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation.
CoRR, 2017

Markov Automata with Multiple Objectives.
CoRR, 2017

A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations.
CoRR, 2017

A storm is Coming: A Modern Probabilistic Model Checker.
CoRR, 2017

Sequential Convex Programming for the Efficient Verification of Parametric MDPs.
CoRR, 2017

Sequential Convex Programming for the Efficient Verification of Parametric MDPs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Model-Based Safety Analysis for Vehicle Guidance Systems.
Proceedings of the Computer Safety, Reliability, and Security, 2017

A weakest pre-expectation semantics for mixed-sign expectations.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Markov Automata with Multiple Objectives.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

A Storm is Coming: A Modern Probabilistic Model Checker.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Modal Stochastic Games - Abstraction-Refinement of Probabilistic Automata.
Proceedings of the Models, Algorithms, Logics and Tools, 2017

Synthesis and Verification of Self-aware Computing Systems.
Proceedings of the Self-Aware Computing Systems., 2017

2016
Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow.
ACM Trans. Design Autom. Electr. Syst., 2016

Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components.
Formal Methods in System Design, 2016

Viewpoints on "Logic activities in Europe", twenty years later.
Bulletin of the EATCS, 2016

Proving Linearizability via Branching Bisimulation.
CoRR, 2016

Parameter Synthesis for Markov Models: Faster Than Ever.
CoRR, 2016

Reasoning about Recursive Probabilistic Programs.
CoRR, 2016

Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs.
CoRR, 2016

Inferring Covariances for Probabilistic Programs.
CoRR, 2016

Probabilistic Model Checking for Complex Cognitive Tasks - A case study in human-robot interaction.
CoRR, 2016

The Probabilistic Model Checker Storm (Extended Abstract).
CoRR, 2016

Advancing Dynamic Fault Tree Analysis.
CoRR, 2016

Bounded Model Checking for Probabilistic Programs.
CoRR, 2016

Safety-Constrained Reinforcement Learning for MDPs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks.
Proceedings of the 35th IEEE Symposium on Reliable Distributed Systems, 2016

Performance Evaluation of Concurrent Data Structures.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2016

Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates.
Proceedings of the Computer Safety, Reliability, and Security, 2016

Inferring Covariances for Probabilistic Programs.
Proceedings of the Quantitative Evaluation of Systems - 13th International Conference, 2016

Parameter Synthesis for Probabilistic Systems.
Proceedings of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2016

Reasoning about Recursive Probabilistic Programs.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

The Probabilistic Model Checking Landscape.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

On the Satisfiability of Some Simple Probabilistic Logics.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs.
Proceedings of the Programming Languages and Systems, 2016

Uncovering Dynamic Fault Trees.
Proceedings of the 46th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2016

Parameter Synthesis for Markov Models: Faster Than Ever.
Proceedings of the Automated Technology for Verification and Analysis, 2016

Bounded Model Checking for Probabilistic Programs.
Proceedings of the Automated Technology for Verification and Analysis, 2016

2015
Modelling and statistical model checking of a microgrid.
STTT, 2015

Verifying pointer programs using graph grammars.
Sci. Comput. Program., 2015

Juggrnaut: using graph grammars for abstracting unbounded heap structures.
Formal Methods in System Design, 2015

Conditioning in Probabilistic Programming.
Electr. Notes Theor. Comput. Sci., 2015

Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181).
Dagstuhl Reports, 2015

High-level Counterexamples for Probabilistic Automata
Logical Methods in Computer Science, 2015

On the Hardness of Almost-Sure Termination.
CoRR, 2015

Safety-Constrained Reinforcement Learning for MDPs.
CoRR, 2015

Conditioning in Probabilistic Programming.
CoRR, 2015

Fault Trees on a Diet - - Automated Reduction by Graph Rewriting -.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2015

A Greedy Approach for the Efficient Repair of Stochastic Models.
Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

On the Hardness of Almost-Sure Termination.
Proceedings of the Mathematical Foundations of Computer Science 2015, 2015

Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2015

Counterexamples for Expected Rewards.
Proceedings of the FM 2015: Formal Methods, 2015

A Statistical Approach for Timed Reachability in AADL Models.
Proceedings of the 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2015

PROPhESY: A PRObabilistic ParamEter SYnthesis Tool.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Understanding Probabilistic Programs.
Proceedings of the Correct System Design, 2015

Probabilistic Programming: A True Verification Challenge.
Proceedings of the Automated Technology for Verification and Analysis, 2015

Model Checking of Open Interval Markov Chains.
Proceedings of the Analytical and Stochastic Modelling Techniques and Applications, 2015

2014
Formal validation methods in model-based spacecraft systems engineering.
Proceedings of the Modeling and Simulation-Based Systems Engineering Handbook., 2014

Minimal counterexamples for linear-time probabilistic verification.
Theor. Comput. Sci., 2014

Symbolic counterexample generation for large discrete-time Markov chains.
Sci. Comput. Program., 2014

Spacecraft early design validation using formal methods.
Rel. Eng. & Sys. Safety, 2014

Operational versus weakest pre-expectation semantics for the probabilistic guarded command language.
Perform. Eval., 2014

Quantitative model-checking of controlled discrete-time Markov processes.
CoRR, 2014

Probably Safe or Live.
CoRR, 2014

Analyzing Expected Outcomes and Almost-Sure Termination of Probabilistic Programs is Hard.
CoRR, 2014

Analysis of Timed and Long-Run Objectives for Markov Automata.
Logical Methods in Computer Science, 2014

Parametric LTL on Markov Chains.
CoRR, 2014

Zero-Reachability in Probabilistic Multi-Counter Automata.
CoRR, 2014

Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey.
Proceedings of the Formal Methods for Executable Software Models, 2014

Accelerating Parametric Probabilistic Verification.
Proceedings of the Quantitative Evaluation of Systems - 11th International Conference, 2014

Performance Analysis of Computing Servers - A Case Study Exploiting a New GSPN Semantics.
Proceedings of the Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, 2014

Parametric LTL on Markov Chains.
Proceedings of the Theoretical Computer Science, 2014

Compositional Analysis Using Component-Oriented Interpolation.
Proceedings of the Formal Aspects of Component Software - 11th International Symposium, 2014

Exponentially timed SADF: Compositional semantics, reductions, and analysis.
Proceedings of the 2014 International Conference on Embedded Software, 2014

Probably safe or live.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

Zero-reachability in probabilistic multi-counter automata.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

Tight Game Abstractions of Probabilistic Automata.
Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Fast Debugging of PRISM Models.
Proceedings of the Automated Technology for Verification and Analysis, 2014

Layered Reduction for Abstract Probabilistic Automata.
Proceedings of the 14th International Conference on Application of Concurrency to System Design, 2014

2013
Model Checking Meets Probability: A Gentle Introduction.
Proceedings of the Engineering Dependable Software Systems, 2013

Model checking for performability.
Mathematical Structures in Computer Science, 2013

Abstract Probabilistic Automata.
Inf. Comput., 2013

A compositional modelling and analysis framework for stochastic hybrid systems.
Formal Methods in System Design, 2013

Correct and Efficient Accelerator Programming (Dagstuhl Seminar 13142).
Dagstuhl Reports, 2013

Modelling, Reduction and Analysis of Markov Automata (extended version)
CoRR, 2013

Accelerating Parametric Probabilistic Verification.
CoRR, 2013

SMT-Based Bisimulation Minimisation of Markov Models.
Proceedings of the Verification, 2013

High-Level Counterexamples for Probabilistic Automata.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

Modelling, Reduction and Analysis of Markov Automata.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

Prinsys - On a Quest for Probabilistic Loop Invariants.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

Layered Reduction for Modal Specification Theories.
Proceedings of the Formal Aspects of Component Software - 10th International Symposium, 2013

Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems.
Proceedings of the Programming Languages and Systems, 2013

Model-based energy optimization of automotive control systems.
Proceedings of the Design, Automation and Test in Europe, 2013

Concurrency Meets Probability: Theory and Practice - (Abstract).
Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

A Semantics for Every GSPN.
Proceedings of the Application and Theory of Petri Nets and Concurrency, 2013

2012
A linear process-algebraic format with data for probabilistic automata.
Theor. Comput. Sci., 2012

Three-valued abstraction for probabilistic systems.
J. Log. Algebr. Program., 2012

Layered reasoning for randomized distributed algorithms.
Formal Asp. Comput., 2012

The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains
CoRR, 2012

Minimal Critical Subsystems for Discrete-Time Markov Models.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Operational Versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language.
Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012

Quantitative Timed Analysis of Interactive Markov Chains.
Proceedings of the NASA Formal Methods, 2012

Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2012

Quantitative Modelling and Analysis.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, 2012

Compositional Abstraction Techniques for Probabilistic Automata.
Proceedings of the Theoretical Computer Science, 2012

Formal correctness, safety, dependability, and performance analysis of a satellite.
Proceedings of the 34th International Conference on Software Engineering, 2012

Robust PCTL model checking.
Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012

Symbolic Counterexample Generation for Discrete-Time Markov Chains.
Proceedings of the Formal Aspects of Component Software, 9th International Symposium, 2012

Model checking of Scenario-Aware Dataflow with CADP.
Proceedings of the 2012 Design, Automation & Test in Europe Conference & Exhibition, 2012

Efficient Modelling and Generation of Markov Automata.
Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012

The COMICS Tool - Computing Minimal Counterexamples for DTMCs.
Proceedings of the Automated Technology for Verification and Analysis, 2012

GSPNs Revisited: Simple Semantics and New Analysis Algorithms.
Proceedings of the 12th International Conference on Application of Concurrency to System Design, 2012

2011
Time-bounded reachability in tree-structured QBDs by abstraction.
Perform. Eval., 2011

The ins and outs of the probabilistic model checker MRMC.
Perform. Eval., 2011

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Logical Methods in Computer Science, 2011

Safety, Dependability and Performance Analysis of Extended AADL Models.
Comput. J., 2011

Abstract Probabilistic Automata.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Efficient CTMC Model Checking of Linear Real-Time Objectives.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Observing Continuous-Time MDPs by 1-Clock Timed Automata.
Proceedings of the Reachability Problems - 5th International Workshop, 2011

Analysing and Improving Energy Efficiency of Distributed Slotted Aloha.
Proceedings of the Smart Spaces and Next Generation Wired/Wireless Networking, 2011

A Local Greibach Normal Form for Hyperedge Replacement Grammars.
Proceedings of the Language and Automata Theory and Applications, 2011

Quantitative automata model checking of autonomous stochastic hybrid systems.
Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, 2011

Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2011

Model Checking: One Can Do Much More Than You Think!
Proceedings of the Fundamentals of Software Engineering - 4th IPM International Conference, 2011

Towards Trustworthy Aerospace Systems: An Experience Report.
Proceedings of the Formal Methods for Industrial Critical Systems, 2011

Weighted Lumpability on Markov Chains.
Proceedings of the Perspectives of Systems Informatics, 2011

Reachability probabilities in Markovian Timed Automata.
Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, 2011

Hierarchical Counterexamples for Discrete-Time Markov Chains.
Proceedings of the Automated Technology for Verification and Analysis, 2011

New Results on Abstract Probabilistic Automata.
Proceedings of the 11th International Conference on Application of Concurrency to System Design, 2011

2010
Learning Communicating Automata from MSCs.
IEEE Trans. Software Eng., 2010

Computing Optimal Schedules for battery Usage in Embedded Systems.
IEEE Trans. Industrial Informatics, 2010

Performability assessment by model checking of Markov reward models.
Formal Methods in System Design, 2010

Approximate Model Checking of Stochastic Hybrid Systems.
Eur. J. Control, 2010

SMA - The Smyle Modeling Approach.
Computing and Informatics, 2010

Performance evaluation and model checking join forces.
Commun. ACM, 2010

Advances in Probabilistic Model Checking.
Proceedings of the Verification, 2010

Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based Methods.
Proceedings of the Static Analysis - 17th International Symposium, 2010

DTMC Model Checking by SCC Reduction.
Proceedings of the QEST 2010, 2010

Analyzing Energy Consumption in a Gossiping MAC Protocol.
Proceedings of the Measurement, 2010

Quantitative Verification in Practice.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

Model Checking Markov Chains Using Krylov Subspace Methods: An Experience Report.
Proceedings of the Computer Performance Engineering, 2010

A Model Checker for AADL.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

libalf: The Automata Learning Framework.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption.
Proceedings of the Analytical and Stochastic Modeling Techniques and Applications, 2010

A Linear Process-Algebraic Format for Probabilistic Systems with Data.
Proceedings of the 10th International Conference on Application of Concurrency to System Design, 2010

2009
Counterexample Generation in Probabilistic Model Checking.
IEEE Trans. Software Eng., 2009

Verification and performance evaluation of aadl models.
Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009

The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems.
Proceedings of the Computer Safety, 2009

Time-Bounded Reachability in Tree-Structured QBDs by Abstraction.
Proceedings of the QEST 2009, 2009

The Ins and Outs of the Probabilistic Model Checker MRMC.
Proceedings of the QEST 2009, 2009

Simulation-Based CTMC Model Checking: An Empirical Evaluation.
Proceedings of the QEST 2009, 2009

Codesign of dependable systems: A component-based modeling language.
Proceedings of the 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 2009

Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

Delayed Nondeterminism in Continuous-Time Markov Decision Processes.
Proceedings of the Foundations of Software Science and Computational Structures, 2009

Compositional Abstraction for Stochastic Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2009

The How and Why of Interactive Markov Chains.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

Maximizing system lifetime by battery scheduling.
Proceedings of the 2009 IEEE/IFIP International Conference on Dependable Systems and Networks, 2009

LTL Model Checking of Time-Inhomogeneous Markov Chains.
Proceedings of the Automated Technology for Verification and Analysis, 2009

2008
How to model and analyze gossiping protocols?
SIGMETRICS Performance Evaluation Review, 2008

Perspectives in Probabilistic Verification.
Proceedings of the Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, 2008

Time-Abstracting Bisimulation for Probabilistic Timed Automata.
Proceedings of the Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, 2008

Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability.
Proceedings of the 29th IEEE Real-Time Systems Symposium, 2008

Regular Expressions for PCTL Counterexamples.
Proceedings of the Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), 2008

The Surprising Robustness of (Closed) Timed Automata against Clock-Drift.
Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

SMA - The Smyle Modeling Approach.
Proceedings of the Software Engineering Techniques, 2008

Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains.
Proceedings of the Hybrid Systems: Computation and Control, 11th International Workshop, 2008

Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2008

Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques.
Proceedings of the Design, Automation and Test in Europe, 2008

Abstraction for Stochastic Systems by Erlang's Method of Stages.
Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

Smyle: A Tool for Synthesizing Distributed Models from Scenarios by Learning.
Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

Symmetry reduction for stochastic hybrid systems.
Proceedings of the 47th IEEE Conference on Decision and Control, 2008

Reachability in continuous-time Markov reward decision processes.
Proceedings of the Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]., 2008

Principles of model checking.
MIT Press, ISBN: 978-0-262-02649-9, 2008

2007
Model checking mobile stochastic logic.
Theor. Comput. Sci., 2007

Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Counterexamples in Probabilistic Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

motor: The modestTool Environment.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison.
Proceedings of the Hardware and Software: Verification and Testing, 2007

Abstraction of Probabilistic Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2007

07101 Abstracts Collection -- Quantitative Aspects of Embedded Systems.
Proceedings of the Quantitative Aspects of Embedded Systems, 04.03. - 09.03.2007, 2007

07101 Executive Summary -- Quantitative Aspects of Embedded Systems.
Proceedings of the Quantitative Aspects of Embedded Systems, 04.03. - 09.03.2007, 2007

Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes.
Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007

Three-Valued Abstraction for Continuous-Time Markov Chains.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2007

2006
Guest Editors' Introduction to the Special Section on the First International Conference on the Quantitative Evaluation of SysTems (QEST).
IEEE Trans. Software Eng., 2006

MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems.
IEEE Trans. Software Eng., 2006

Guest editors' introduction: quantitative analysis of real-time embedded systems.
STTT, 2006

Towards a Logic for Performance and Mobility.
Electr. Notes Theor. Comput. Sci., 2006

YMCA: - Why Markov Chain Algebra? - .
Electr. Notes Theor. Comput. Sci., 2006

Bisimulation and Simulation Relations for Markov Chains.
Electr. Notes Theor. Comput. Sci., 2006

Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability.
Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 2006

Probably on Time and within Budget: On Reachability in Priced Probabilistic Timed Automata.
Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 2006

2005
Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes.
Theor. Comput. Sci., 2005

Performance and verification.
SIGMETRICS Performance Evaluation Review, 2005

Model checking meets performance evaluation.
SIGMETRICS Performance Evaluation Review, 2005

A theory of Stochastic systems. Part II: Process algebra.
Inf. Comput., 2005

A theory of stochastic systems part I: Stochastic automata.
Inf. Comput., 2005

Comparative branching-time semantics for Markov chains.
Inf. Comput., 2005

A Markov Reward Model Checker.
Proceedings of the Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), 2005

Safety and Liveness in Concurrent Pointer Programs.
Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Model Checking Markov Reward Models with Impulse Rewards.
Proceedings of the 2005 International Conference on Dependable Systems and Networks (DSN 2005), 28 June, 2005

Are You Still There? - A Lightweight Algorithm to Monitor Node Presence in Self-Configuring Networks.
Proceedings of the 2005 International Conference on Dependable Systems and Networks (DSN 2005), 28 June, 2005

2004
Guest editors' introduction: Advancements and extensions of verification techniques.
STTT, 2004

Probabilistic weak simulation is decidable in polynomial time.
Inf. Process. Lett., 2004

Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Embedded Software Analysis with MOTOR.
Proceedings of the Formal Methods for the Design of Real-Time Systems, 2004

An industrial-strength formal method -- A Modest survey.
Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2004

Who is Pointing When to Whom?
Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

Model Checking Dependability Attributes of Wireless Group Communication.
Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN 2004), 28 June, 2004

Labelled Transition Systems.
Proceedings of the Model-Based Testing of Reactive Systems, 2004

2003
Model-Checking Algorithms for Continuous-Time Markov Chains.
IEEE Trans. Software Eng., 2003

A tool for model-checking Markov chains.
STTT, 2003

Model-checking large structured Markov chains.
J. Log. Algebr. Program., 2003

A QoS-Oriented Extension of UML Statecharts.
Proceedings of the «UML» 2003, 2003

Discrete-Time Rewards Model-Checked.
Proceedings of the Formal Modeling and Analysis of Timed Systems: First International Workshop, 2003

ETMCC: Model Checking Performability Properties of Markov Chains.
Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003), 2003

On Integrating the MÖBIUS and MODEST Modeling Tools.
Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003), 2003

The Modest Modeling Tool and Its Implementation.
Proceedings of the Computer Performance Evaluations, 2003

Comparative Branching-Time Semantics.
Proceedings of the CONCUR 2003, 2003

2002
Real-Time and Probabilistic Systems - Foreword.
Theor. Comput. Sci., 2002

Process algebra for performance evaluation.
Theor. Comput. Sci., 2002

Guest editors' introduction: Model checking in a nutshell.
J. Log. Algebr. Program., 2002

Automated Performance and Dependability Evaluation Using Model Checking.
Proceedings of the Performance Evaluation of Complex Systems: Techniques and Tools, 2002

Model Checking Birth and Death.
Proceedings of the Foundations of Information Technology in the Era of Networking and Mobile Computing, 2002

A Probabilistic Extension of UML Statecharts.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

Model Checking Performability Properties.
Proceedings of the 2002 International Conference on Dependable Systems and Networks (DSN 2002), 2002

Simulation for Continuous-Time Markov Chains.
Proceedings of the CONCUR 2002, 2002

2001
Metric semantics for true concurrent real time.
Theor. Comput. Sci., 2001

First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Beyond Memoryless Distributions: Model Checking Semi-Markov Chains.
Proceedings of the Process Algebra and Probabilistic Methods, 2001

Faster and Symbolic CTMC Model Checking.
Proceedings of the Process Algebra and Probabilistic Methods, 2001

MoDeST - A Modelling and Description Language for Stochastic Timed Systems.
Proceedings of the Process Algebra and Probabilistic Methods, 2001

Performance Evaluation : = (Process Algebra + Model Checking) × Markov Chains.
Proceedings of the CONCUR 2001, 2001

2000
Pattern-matching algorithms based on term rewrite systems.
Theor. Comput. Sci., 2000

Automated compositional Markov chain generation for a plain-old telephone system.
Sci. Comput. Program., 2000

A Markov Chain Model Checker.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

On the Use of Model Checking Techniques for Dependability Evaluation.
Proceedings of the 19th IEEE Symposium on Reliable Distributed Systems, 2000

Towards Model Checking Stochastic Process Algebra.
Proceedings of the Integrated Formal Methods, Second International Conference, 2000

On the Logical Characterisation of Performability Properties.
Proceedings of the Automata, Languages and Programming, 27th International Colloquium, 2000

On a Temporal Logic for Object-Based Systems.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems IV, 2000

General Distributions in Process Algebra.
Proceedings of the Lectures on Formal Methods and Performance Analysis, 2000

Model Checking Continuous-Time Markov Chains by Transient Analysis.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999
On Generative Parallel Composition.
Electr. Notes Theor. Comput. Sci., 1999

Specification and Analysis of Soft Real-Time Systems: Quantity and Quality.
Proceedings of the 20th IEEE Real-Time Systems Symposium, 1999

Approximate Symbolic Model Checking of Continuous-Time Markov Chains.
Proceedings of the CONCUR '99: Concurrency Theory, 1999

1998
A Consistent Causality-Based View on a Timed Process Algebra Including Urgent Interactions.
Formal Methods in System Design, 1998

Automatic Verification of a Lip-Synchronisation Protocol Using Uppaal.
Formal Asp. Comput., 1998

Partial Order Models for Quantitative Extensions of LOTOS.
Computer Networks, 1998

An algebraic approach to the specification of stochastic systems.
Proceedings of the Programming Concepts and Methods, 1998

Metric Semantics for True Concurrent Real Time.
Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Pomsets for MSC.
Proceedings of the Formale Beschreibungstechniken für verteilte Systeme, 1998

A True Concurrency Semantics for ET-LOTOS.
Proceedings of the 1st International Conference on Application of Concurrency to System Design (ACSD '98), 1998

1997
Code Generation Based on Formal BURS Therory and Heuristic Search.
Acta Inf., 1997

The Bounded Retransmission Protocol Must Be on Time!
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1997

Causal Ambiguity and Partial Orders in Event Structures.
Proceedings of the CONCUR '97: Concurrency Theory, 1997

1996
Systolic Arrays for the Recognition of Permutation-Invariant Segments.
Sci. Comput. Program., 1996

Design and Analysis of Dynamic Leader Election Protocols in Broadcast Networks.
Distributed Computing, 1996

On Specifying Real-Time Systems in a Causality-Based Setting.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1996

Code Generation = A* + BURS.
Proceedings of the Compiler Construction, 6th International Conference, 1996

1995
A Design Model for Open Distributed Processing Systems.
Computer Networks and ISDN Systems, 1995

A Stochastic Causality-Based Process Algebra.
Comput. J., 1995

Causal Behaviours and Nets.
Proceedings of the Application and Theory of Petri Nets 1995, 1995

1993
Recognizing k-Rotated Segments.
International Journal of High Speed Computing, 1993

A Semi-Markov Model of a Home Network Access Protocol.
Proceedings of the MASCOTS '93, 1993

Modeling Systems by Probabilistic Process Algebra: an Event Structures Approach.
Proceedings of the Formal Description Techniques, VI, Proceedings of the IFIP TC6/WG6.1 Sixth International Conference on Formal Description Techniques, 1993

1991
A Parallel program for the recognition of P-Invariant segments.
Proceedings of the Algorithms and Parallel VLSI Architectures II, 1991

1989
Bottom-Up Tree Acceptors.
Sci. Comput. Program., 1989


  Loading...