Christel Baier

Clemens Dubslaff

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

Probabilistic Model Checking for Energy-Utility Analysis.

[BibT_eX]

[DOI]

Proceedings of the Horizons of the Mind. A Tribute to Prakash Panangaden, 2014

Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Application and Theory of Petri Nets and Concurrency, 2014

Probabilistic model checking for energy analysis in software product lines.

[BibT_eX]

[DOI]

Clemens Dubslaff

Proceedings of the 13th International Conference on Modularity, 2014

2013

Model checking for performability.

[BibT_eX]

[DOI]

Ernst Moritz Hahn

Math. Struct. Comput. Sci., 2013

Preface to the special issue on Probabilistic Model Checking.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

Distributed wait state tracking for runtime MPI deadlock detection.

[BibT_eX]

[DOI]

Tobias Hilbrich

Bronis R. de Supinski

Proceedings of the International Conference for High Performance Computing, 2013

A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Select.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2013

Computing Quantiles in Markov Reward Models.

[BibT_eX]

[DOI]

Michael Ummels

Proceedings of the Foundations of Software Science and Computation Structures, 2013

Quantitative Analysis of Randomized Distributed Systems and Probabilistic Automata.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Informatics - 5th International Conference, 2013

2012

Probabilistic ω-automata.

[BibT_eX]

[DOI]

J. ACM, 2012

Model checking probabilistic systems against pushdown specifications.

[BibT_eX]

[DOI]

Clemens Dubslaff

Manuela Berg

Inf. Process. Lett., 2012

Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code

[BibT_eX]

[DOI]

Proceedings of the Proceedings Seventh Conference on Systems Software Verification, 2012

Stochastic game logic.

[BibT_eX]

[DOI]

Acta Informatica, 2012

Static Partial Order Reduction for Probabilistic Concurrent Systems.

[BibT_eX]

[DOI]

Álvaro Fernández Díaz

Clara Benac Earle

Lars-Åke Fredlund

Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012

Rare-event verification for stochastic hybrid systems.

[BibT_eX]

[DOI]

Paolo Zuliani

Edmund M. Clarke

Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012

Waiting for Locks: How Long Does It Usually Take?

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2012

2011

Synthesis of Reo circuits from scenario-based interaction specifications.

[BibT_eX]

[DOI]

Sun Meng

Sci. Comput. Program., 2011

Modeling and Verification of Components and Connectors.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Eternal Networked Software Systems, 2011

Hierarchical Modeling and Formal Verification. An Industrial Case Study Using Reo and Vereofy.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2011

A Compositional Framework for Controller Synthesis.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

2010

Alternating-time stream logic for multi-agent systems.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2010

Partially-shared zero-suppressed multi-terminal BDDs: concept, algorithms and applications.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2010

Performability assessment by model checking of Markov reward models.

[BibT_eX]

[DOI]

Lucia Cloth

Formal Methods Syst. Des., 2010

Performance evaluation and model checking join forces.

[BibT_eX]

[DOI]

Commun. ACM, 2010

Design and Verification of Systems with Exogenous Coordination Using Vereofy.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

On Model Checking Techniques for Randomized Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 8th International Conference, 2010

10031 Executive Summary - Quantitative Models: Expressiveness and Analysis.

[BibT_eX]

[DOI]

Manfred Droste

Paul Gastin

Kim Guldstrand Larsen

Proceedings of the Quantitative Models: Expressiveness and Analysis, 17.01. - 22.01.2010, 2010

10031 Abstracts Collection - Quantitative Models: Expressiveness and Analysis.

[BibT_eX]

[DOI]

Manfred Droste

Paul Gastin

Kim Guldstrand Larsen

Proceedings of the Quantitative Models: Expressiveness and Analysis, 17.01. - 22.01.2010, 2010

2009

Symbolic model checking for channel-based component connectors.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2009

Credo Methodology: Modeling and Analyzing A Peer-to-Peer System in Credo.

[BibT_eX]

[DOI]

Immo Grabe

Mohammad Mahdi Jaghoori

Bernhard K. Aichernig

Proceedings of the 3rd International Workshop on Harnessing Theories for Tool Support in Software, 2009

Preface.

[BibT_eX]

[DOI]

Alessandra Di Pierro

Proceedings of Seventh Workshop on Quantitative Aspects of Programming Languages, 2009

Probabilistic Automata over Infinite Words: Expressiveness, Efficiency, and Decidability

[BibT_eX]

[DOI]

Proceedings of the Proceedings Eleventh International Workshop on Descriptional Complexity of Formal Systems, 2009

Probabilistic Acceptors for Languages over Infinite Words.

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2009: Theory and Practice of Computer Science, 2009

When Are Timed Automata Determinizable?

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 36th Internatilonal Colloquium, 2009

Recurrence and Transience for Probabilistic Automata.

[BibT_eX]

[DOI]

Mathieu Tracol

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2009

The Credo Methodology - (Extended Version).

[BibT_eX]

[DOI]

Immo Grabe

Mohammad Mahdi Jaghoori

Bernhard K. Aichernig

Frank S. de Boer

Andreas Griesmayer

Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

A Uniform Framework for Modeling and Verifying Components and Connectors.

[BibT_eX]

[DOI]

Proceedings of the Coordination Models and Languages, 11th International Conference, 2009

The Effect of Tossing Coins in Omega-Automata.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009

Quantitative Analysis under Fairness Constraints.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2009

2008

A uniform framework for weighted decision diagrams and its implementation.

[BibT_eX]

[DOI]

Jörn Ossowski

Int. J. Softw. Tools Technol. Transf., 2008

Special issue: CONCUR 2006.

[BibT_eX]

[DOI]

Inf. Comput., 2008

Synthesis of Reo Circuits from Scenario-based Specifications.

[BibT_eX]

[DOI]

Sun Meng

Proceedings of the 7th International Workshop on the Foundations of Coordination Languages and Software Architectures, 2008

Preface.

[BibT_eX]

[DOI]

Alessandro Aldini

Proceedings of the Sixth Workshop on Quantitative Aspects of Programming Languages, 2008

Generating Compact MTBDD-Representations from ProbmelaSpecifications.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2008

Reduction Techniques for Model Checking Markov Decision Processes.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), 2008

Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

On Decision Problems for Probabilistic Büchi Automata.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2008

Formal Verification for Components and Connectors.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 7th International Symposium, 2008

Reachability in continuous-time Markov reward decision processes.

[BibT_eX]

Proceedings of the Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]., 2008

Principles of model checking.

[BibT_eX]

MIT Press, ISBN: 978-0-262-02649-9, 2008

2007

Model Checking Markov Chains with Actions and State Labels.

[BibT_eX]

[DOI]

Lucia Cloth

Matthias Kuntz

Markus Siegle

IEEE Trans. Software Eng., 2007

Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2007

Models and temporal logical specifications for timed component connectors.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2007

Checking Equivalence for Reo Networks.

[BibT_eX]

[DOI]

Tobias Blechmann

Proceedings of the 4th International Workshop on Formal Aspects of Component Software, 2007

On-the-Fly Stuttering in the Construction of Deterministic <i>omega</i> -Automata.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Automata, 2007

Syanco 2007: international workshop on synthesis and analysis of component connectors.

[BibT_eX]

[DOI]

Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007

Probabilistic and Topological Semantics for Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 2007

2006

Experiments with deterministic <i>omega</i>-automata for formulas of linear temporal logic.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

Modeling component connectors in Reo by constraint automata.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2006

A note on the attractor-property of infinite-state Markov chains.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2006

Trace Semantics for Stochastic Systems with Nondeterminism.

[BibT_eX]

[DOI]

Verena Wolf

Proceedings of the 4th International Workshop on Quantitative Aspects of Programming Languages, 2006

LiQuor: A tool for Qualitative and Quantitative Linear Time analysis of Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 2006

On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

On Reduction Criteria for Probabilistic Reward Models.

[BibT_eX]

[DOI]

Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006

Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2006

Compositional Semantics of an Actor-Based Language Using Constraint Automata.

[BibT_eX]

[DOI]

Marjan Sirjani

Mohammad Mahdi Jaghoori

Proceedings of the Coordination Models and Languages, 8th International Conference, 2006

Stochastic Reasoning About Channel-Based Component Connectors.

[BibT_eX]

[DOI]

Verena Wolf

Proceedings of the Coordination Models and Languages, 8th International Conference, 2006

2005

Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Model checking meets performance evaluation.

[BibT_eX]

[DOI]

SIGMETRICS Perform. Evaluation Rev., 2005

ProbMela and verification of Markov decision processes.

[BibT_eX]

[DOI]

SIGMETRICS Perform. Evaluation Rev., 2005

Probabilistic Models for Reo Connector Circuits.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2005

Comparative branching-time semantics for Markov chains.

[BibT_eX]

[DOI]

Inf. Comput., 2005

Simulating perfect channels with probabilistic lossy channels.

[BibT_eX]

[DOI]

Parosh Aziz Abdulla

S. Purushothaman Iyer

Bengt Jonsson

Inf. Comput., 2005

Trace Machines for Observing Continuous-Time Markov Chains.

[BibT_eX]

[DOI]

Verena Wolf

Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, 2005

Symbolic Reasoning with Weighted and Normalized Decision Diagrams.

[BibT_eX]

[DOI]

Jörn Ossowski

Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, 2005

Bisimulation and Simulation Relations for Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the Workshop "Essays on Algebraic Process Calculi", 2005

Partial Order Reduction for Probabilistic Branching Time.

[BibT_eX]

[DOI]

Pedro R. D'Argenio

Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, 2005

Verifying nondeterministic probabilistic channel systems against $\omega$-regular linear-time properties

[BibT_eX]

[DOI]

CoRR, 2005

Experiments with Deterministic omega-Automata for Formulas of Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Automata, 2005

Recognizing omega-regular Languages with Probabilistic Automata.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Genetic Algorithms for the Variable Ordering Problem of Binary Decision Diagrams.

[BibT_eX]

[DOI]

Wolfgang Lenders

Proceedings of the Foundations of Genetic Algorithms, 8th International Workshop, 2005

Quantitative analysis of distributed randomized protocols.

[BibT_eX]

[DOI]

Proceedings of the 10th international workshop on Formal methods for industrial critical systems, 2005

Partial Order Reduction for Markov Decision Processes: A Survey.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Synthesis of Reo Circuits for Implementation of Component-Connector Automata Specifications.

[BibT_eX]

[DOI]

Proceedings of the Coordination Models and Languages, 7th International Conference, 2005

2004

Probabilistic weak simulation is decidable in polynomial time.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2004

Models and Temporal Logics for Timed Component Connectors.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

Partial Order Reduction for Probabilistic Systems.

[BibT_eX]

[DOI]

Proceedings of the 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), 2004

PROBMELA: a modeling language for communicating probabilistic processes.

[BibT_eX]

[DOI]

Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

Controller Synthesis for Probabilistic Systems.

[BibT_eX]

[DOI]

Proceedings of the Exploring New Frontiers of Theoretical Informatics, 2004

Model Checking Action- and State-Labelled Markov Chains.

[BibT_eX]

[DOI]

Lucia Cloth

Matthias Kuntz

Markus Siegle

Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN 2004), 28 June, 2004

2003

Model-Checking Algorithms for Continuous-Time Markov Chains.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2003

Modeling Component Connectors in Reo by Constraint Automata: (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of FOCLASA 2003, 2003

Comparative Branching-Time Semantics.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2003, 2003

2002

Automated Performance and Dependability Evaluation Using Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Performance Evaluation of Complex Systems: Techniques and Tools, 2002

Model Checking Performability Properties.

[BibT_eX]

[DOI]

Proceedings of the 2002 International Conference on Dependable Systems and Networks (DSN 2002), 2002

Simulation for Continuous-Time Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2002, 2002

Theoretische Informatik - eine Einführung in Berechenbarkeit, Komplexität und formale Sprachen mit 101 Beispielen.

[BibT_eX]

[DOI]

Alexander Asteroth

Pearson Studium, ISBN: 978-3-8273-7033-4, 2002

2001

Metric semantics for true concurrent real time.

[BibT_eX]

[DOI]

Diego Latella

Theor. Comput. Sci., 2001

Model Checking with Formula-Dependent Abstract Models.

[BibT_eX]

[DOI]

Alexander Asteroth

Ulrich Aßmann

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Deciding Bisimilarity and Similarity for Probabilistic Processes.

[BibT_eX]

[DOI]

Bettina Engelen

J. Comput. Syst. Sci., 2000

On Topological Hierarchies of Temporal Properties.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2000

On the Logical Characterisation of Performability Properties.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 27th International Colloquium, 2000

Norm Functions for Probabilistic Bisimulations with Delays.

[BibT_eX]

[DOI]

Mariëlle Stoelinga

Proceedings of the Foundations of Software Science and Computation Structures, 2000

Reasoning about Probabilistic Lossy Channel Systems.

[BibT_eX]

[DOI]

Parosh Aziz Abdulla

S. Purushothaman Iyer

Bengt Jonsson

Proceedings of the CONCUR 2000, 2000

Model Checking Continuous-Time Markov Chains by Transient Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Approximate Symbolic Model Checking of Continuous-Time Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '99: Concurrency Theory, 1999

Establishing Qualitative Properties for Probabilistic Lossy Channel Systems: An Algorithmic Approach.

[BibT_eX]

[DOI]

Bettina Engelen

Proceedings of the Formal Methods for Real-Time and Probabilistic Systems, 1999

1998

On the Verification of Qualitative Properties of Probabilistic Processes under Fairness Constraints.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1998

Computing Probability Bounds for Linear Time Formulas over Concurrent Probabilistic Systems.

[BibT_eX]

[DOI]

Gethin Norman

Proceedings of the First International Workshop on Probabilistic Methods in Verification, 1998

Preface.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Probabilistic Methods in Verification, 1998

On the Semantic Foundations of Probabilistic Synchronous Reactive Programs.

[BibT_eX]

[DOI]

Vasiliki Hartonas-Garmhausen

Edmund M. Clarke

Proceedings of the First International Workshop on Probabilistic Methods in Verification, 1998

Model Checking for a Probabilistic Branching Time Logic with Fairness.

[BibT_eX]

[DOI]

Distributed Comput., 1998

1997

Trees and Semantics.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1997

How to Interpret and Establish Consistency Results for Semantics of Concurrent Programming Languages.

[BibT_eX]

[DOI]

Fundam. Informaticae, 1997

The Connection Between Initial and Unique Solutions of Domain Equations in the Partial Order and Metric Approach.

[BibT_eX]

[DOI]

Formal Aspects Comput., 1997

Domain equations for probabilistic processes.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Expressiveness in Concurrency, 1997

Metric Semantics from Partial Order Semantics.

[BibT_eX]

[DOI]

Acta Informatica, 1997

Automatic Verification of Liveness Properties of Randomized Systems.

[BibT_eX]

[DOI]

Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing, 1997

Symbolic Model Checking for Probabilistic Processes.

[BibT_eX]

[DOI]

Vasiliki Hartonas-Garmhausen

Edmund M. Clarke

Mark Ryan

Proceedings of the Automata, Languages and Programming, 24th International Colloquium, 1997

Weak Bisimulation for Fully Probabilistic Processes.

[BibT_eX]

Proceedings of the Formale Beschreibungstechniken für verteilte Systeme, 1997

1996

Metric Completion versus Ideal Completion.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1996

Denotational Linear Time Semantics and Sequential Composition.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1996

Polynomial Time Algorithms for Testing Probabilistic Bisimulation and Simulation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

A Categorical Characterization of Consistency Results.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Methodology and Software Technology, 1996

1994

Denotational Semantics in the CPO and Metric Approach.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1994

The Connection between an Event Structure Semantics and an Operational Semantics for TCSP.

[BibT_eX]

[DOI]

Acta Informatica, 1994

1991

The Consistency of a Noninterleaving and an Interleaving Model for Full TCSP.

[BibT_eX]

[DOI]