Kim G. Larsen

According to our database1, Kim G. Larsen authored at least 436 papers between 1984 and 2019.

Collaborative distances:

Book
In proceedings
Article
PhD thesis
Other

Bibliography

2019
Continuous-Time Models for System Design and Analysis.
Proceedings of the Computing and Software Science - State of the Art and Perspectives, 2019

Converging from branching to linear metrics on Markov chains.
Mathematical Structures in Computer Science, 2019

Model checking and synthesis for branching multi-weighted logics.
J. Log. Algebr. Meth. Program., 2019

Selected papers from the 28th Nordic Workshop on Programming Theory (NWPT'16).
J. Log. Algebr. Meth. Program., 2019

Computing Probabilistic Bisimilarity Distances for Probabilistic Automata.
CoRR, 2019

L*-Based Learning of Markov Decision Processes (Extended Version).
CoRR, 2019

SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes.
CoRR, 2019

Abstract Dependency Graphs and Their Application to Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Model Verification Through Dependency Graphs.
Proceedings of the Model Checking Software - 26th International Symposium, 2019

Safe and Time-Optimal Control for Railway Games.
Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2019

Symbolic Model Checking of Weighted PCTL Using Dependency Graphs.
Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

Time to Learn - Learning Timed Automata from Tests.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2019

L*-Based Learning of Markov Decision Processes.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Synthesis of Safe, Optimal and Compact Strategies for Stochastic Hybrid Games (Invited Paper).
Proceedings of the 30th International Conference on Concurrency Theory, 2019

Partial Order Reduction for Reachability Games.
Proceedings of the 30th International Conference on Concurrency Theory, 2019

Computing Probabilistic Bisimilarity Distances for Probabilistic Automata.
Proceedings of the 30th International Conference on Concurrency Theory, 2019

2018
Model Checking Real-Time Systems.
Proceedings of the Handbook of Model Checking., 2018

Reachability problems: Special issue.
Theor. Comput. Sci., 2018

Discrete and continuous strategies for timed-arc Petri net games.
STTT, 2018

High-level frameworks for the specification and verification of scheduling problems.
STTT, 2018

On decidability of recursive weighted logics.
Soft Comput., 2018

Preface: Dedicated to the memory of Zoltán Ésik (1951-2016).
Soft Comput., 2018

Reasoning About Bounds in Weighted Transition Systems.
Logical Methods in Computer Science, 2018

A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains.
Logical Methods in Computer Science, 2018

On the metric-based approximate minimization of Markov Chains.
J. Log. Algebr. Meth. Program., 2018

A Distributed Fixed-Point Algorithm for Extended Dependency Graphs.
Fundam. Inform., 2018

Contracts for System Design.
Foundations and Trends in Electronic Design Automation, 2018

Complete Axiomatization for the Total Variation Distance of Markov Chains.
Electr. Notes Theor. Comput. Sci., 2018

A Faster-Than Relation for Semi-Markov Decision Processes.
CoRR, 2018

Parameter Synthesis Problems for one parametric clock Timed Automata.
CoRR, 2018

Learning Timed Automata via Genetic Programming.
CoRR, 2018

On the Metric-based Approximate Minimization of Markov Chains.
CoRR, 2018

Optimal and Robust Controller Synthesis: using Energy Timed Automata with Uncertainty.
CoRR, 2018

Average-energy games.
Acta Inf., 2018

A Hemimetric Extension of Simulation for Semi-Markov Decision Processes.
Proceedings of the Quantitative Evaluation of Systems - 15th International Conference, 2018

Proceedings of the Quantitative Evaluation of Systems - 15th International Conference, 2018

On the Verification of Weighted Kripke Structures Under Uncertainty.
Proceedings of the Quantitative Evaluation of Systems - 15th International Conference, 2018

Energiautomater, energifunktioner og Kleene-algebra.
Proceedings of the 31th Norsk Informatikkonferanse, 2018

Timed Comparisons of Semi-Markov Processes.
Proceedings of the Language and Automata Theory and Applications, 2018

Generic Formal Framework for Compositional Analysis of Hierarchical Scheduling Systems.
Proceedings of the 21st IEEE International Symposium on Real-Time Distributed Computing, 2018

20 Years of UPPAAL Enabled Industrial Model-Based Validation and Beyond.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, 2018

Statistical Model Checking the 2018 Edition!
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018

Model-Based Mutation Testing of Real-Time Systems via Model Checking.
Proceedings of the 2018 IEEE International Conference on Software Testing, 2018

Weighted Branching Systems: Behavioural Equivalence, Behavioural Distance, and Their Logical Characterisations.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2018

20 Years of Real Real Time Model Validation.
Proceedings of the Formal Methods - 22nd International Symposium, 2018

Optimal and Robust Controller Synthesis - Using Energy Timed Automata with Uncertainty.
Proceedings of the Formal Methods - 22nd International Symposium, 2018

Guaranteed Control Synthesis for Continuous Systems in Uppaal Tiga.
Proceedings of the Cyber Physical Systems. Model-Based Design - 8th International Workshop, 2018

Time Optimal Robust Fleet Management of Micro UAV Through Timed Games Formulation.
Proceedings of the IEEE Conference on Control Technology and Applications, 2018

Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Models, Mindsets, Meta: The What, the How, and the Why Not?
Proceedings of the Models, Mindsets, 2018

Analyzing Spreadsheets for Parallel Execution via Model Checking.
Proceedings of the Models, Mindsets, 2018

2017
From Timed Automata to Stochastic Hybrid Games Model Checking, Synthesis, Performance Analysis and Machine Learning.
Proceedings of the Dependable Software Systems Engineering, 2017

On-the-Fly Computation of Bisimilarity Distances.
Logical Methods in Computer Science, 2017

Timed Comparisons of Semi-Markov Processes.
CoRR, 2017

Reasoning About Bounds in Weighted Transition Systems.
CoRR, 2017

On-the-Fly Computation of Bisimilarity Distances.
CoRR, 2017

A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains.
CoRR, 2017

Timed and Untimed Energy Games.
Proceedings of the Implementation and Application of Automata, 2017

Memory-Efficient Tactics for Randomized LTL Model Checking.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

Validation, Synthesis and Optimization for Cyber-Physical Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Practical controller synthesis for MTL0, ∞.
Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

Dependable and Optimal Cyber-Physical Systems.
Proceedings of the SOFSEM 2017: Theory and Practice of Computer Science, 2017

Refinement of Trace Abstraction for Real-Time Programs.
Proceedings of the Reachability Problems - 11th International Workshop, 2017

Unrestricted stone duality for Markov processes.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Formal validation of supervisory energy management systems for microgrids.
Proceedings of the IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society, Beijing, China, October 29, 2017

PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2017, 2017

Mutation-Based Test-Case Generation with Ecdar.
Proceedings of the 2017 IEEE International Conference on Software Testing, 2017

Pareto Optimal Reachability Analysis for Simple Priced Timed Automata.
Proceedings of the Formal Methods and Software Engineering, 2017

Integrating Tools: Co-simulation in UPPAAL Using FMI-FMU.
Proceedings of the 22nd International Conference on Engineering of Complex Computer Systems, 2017

On the Metric-Based Approximate Minimization of Markov Chains.
Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

Symbolic Dependency Graphs for $$\text {PCTL}^{>}_{\le }$$ Model-Checking.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2017

Quantitative Evaluation of Attack Defense Trees Using Stochastic Timed Automata.
Proceedings of the Graphical Models for Security - 4th International Workshop, 2017

Compositional Testing of Real-Time Systems.
Proceedings of the ModelEd, TestEd, TrustEd, 2017

Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation.
Proceedings of the Application and Theory of Petri Nets and Concurrency, 2017

2016
Efficient model-checking of weighted CTL with upper-bound constraints.
STTT, 2016

Optimizing the resource requirements of hierarchical scheduling systems.
SIGBED Review, 2016

Statistical and exact schedulability analysis of hierarchical scheduling systems.
Sci. Comput. Program., 2016

Learning deterministic probabilistic automata from a model checking perspective.
Machine Learning, 2016

Formal modelling and analysis of Bitflips in ARM assembly code.
Information Systems Frontiers, 2016

WNetKAT: A Weighted SDN Programming and Verification Language.
CoRR, 2016

Limit Your Consumption! Finding Bounds in Average-energy Games.
Proceedings of the Proceedings 14th International Workshop Quantitative Aspects of Programming Languages and Systems, 2016

Compositional bisimulation metric reasoning with Probabilistic Process Calculi.
Logical Methods in Computer Science, 2016

Weighted Branching Simulation Distance for Parametric Weighted Kripke Structures.
Proceedings of the Proceedings Cassting Workshop on Games for the Synthesis of Complex Systems and 3rd International Workshop on Synthesis of Complex Parameters and 3rd International Workshop on Synthesis of Complex Parameters, 2016

Automatic Verification, Performance Analysis, Synthesis and Optimization of Timed Systems.
Proceedings of the 23rd International Symposium on Temporal Representation and Reasoning, 2016

Online and Compositional Learning of Controllers with Application to Floor Heating.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization.
Proceedings of the Model Checking Software - 23rd International Symposium, 2016

Importance Sampling for Stochastic Timed Automata.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2016

A Complete Approximation Theory for Weighted Transition Systems.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2016

Distributed Computation of Fixed Points on Dependency Graphs.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2016

Time optimal reachability analysis using swarm verification.
Proceedings of the 31st Annual ACM Symposium on Applied Computing, 2016

WNetKAT: A Weighted SDN Programming and Verification Language.
Proceedings of the 20th International Conference on Principles of Distributed Systems, 2016

On the Power of Statistical Model Checking.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Statistical Model Checking: Past, Present, and Future.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

Toolchain for user-centered intelligent floor heating control.
Proceedings of the IECON 2016, 2016

Probabilistic Mu-Calculus: Decidability and Complete Axiomatization.
Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

Distributed Algorithms for Time Optimal Reachability Analysis.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2016

Modelling Attack-defense Trees Using Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2016

A Model-Based Framework for the Specification and Analysis of Hierarchical Scheduling Systems.
Proceedings of the Critical Systems: Formal Methods and Automated Verification, 2016

Energy-aware scheduling of FIR filter structures using a timed automata model.
Proceedings of the 2016 IEEE 19th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS), 2016

Complete Axiomatization for the Bisimilarity Distance on Markov Chains.
Proceedings of the 27th International Conference on Concurrency Theory, 2016

An Automata-Based Approach to Trace Partitioned Abstract Interpretation.
Proceedings of the Semantics, Logics, and Calculi, 2016

2015
Real-time specifications.
STTT, 2015

Statistical model checking for biological systems.
STTT, 2015

Uppaal SMC tutorial.
STTT, 2015

Schedulability of Herschel revisited using statistical model checking.
STTT, 2015

A reconfigurable framework for compositional schedulability and power analysis of hierarchical scheduling systems with frequency scaling.
Sci. Comput. Program., 2015

Concurrent weighted logic.
J. Log. Algebr. Meth. Program., 2015

Alternation-Free Weighted Mu-Calculus: Decidability and Completeness.
Electr. Notes Theor. Comput. Sci., 2015

The EATCS Award 2016 - Call for Nominations.
Bulletin of the EATCS, 2015

Average-energy games (full version).
CoRR, 2015

Average-energy games.
Proceedings of the Proceedings Sixth International Symposium on Games, 2015

Language Emptiness of Continuous-Time Parametric Timed Automata.
CoRR, 2015

Refinement checking on parametric modal transition systems.
Acta Inf., 2015

Uppaal Stratego.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Parametric Verification of Weighted Systems.
Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters, 2015

Model checking of finite-state machine-based scenario-aware dataflow using timed automata.
Proceedings of the 10th IEEE International Symposium on Industrial Embedded Systems, 2015

Proceedings of the IEEE 18th International Symposium on Real-Time Distributed Computing, 2015

Formal Methods for Modelling and Analysis of Single-Event Upsets.
Proceedings of the 2015 IEEE International Conference on Information Reuse and Integration, 2015

Converging from Branching to Linear Metrics on Markov Chains.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2015, 2015

CAAL: Concurrency Workbench, Aalborg Edition.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2015, 2015

Language Emptiness of Continuous-Time Parametric Timed Automata.
Proceedings of the Automata, Languages, and Programming - 42nd International Colloquium, 2015

Resource-Parameterized Timing Analysis of Real-Time Systems.
Proceedings of the Hardware and Software: Verification and Testing, 2015

Compositional Metric Reasoning with Probabilistic Process Calculi.
Proceedings of the Foundations of Software Science and Computation Structures, 2015

On the Total Variation Distance of Semi-Markov Chains.
Proceedings of the Foundations of Software Science and Computation Structures, 2015

A Score Function for Optimizing the Cycle-Life of Battery-Powered Embedded Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2015

Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools.
Proceedings of the Formal Methods for Industrial Critical Systems, 2015

A Cost/Reward Method for Optimal Infinite Scheduling in Mobile Cloud Computing.
Proceedings of the Formal Aspects of Component Software - 12th International Conference, 2015

Polynomial Time Decidability of Weighted Synchronization under Partial Observability.
Proceedings of the 26th International Conference on Concurrency Theory, 2015

Modelling Social-Technical Attacks with Timed Automata.
Proceedings of the 7th ACM CCS International Workshop on Managing Insider Security Threats, 2015

Quantitative Schedulability Analysis of Continuous Probability Tasks in a Hierarchical Context.
Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering, 2015

Safe and Optimal Adaptive Cruise Control.
Proceedings of the Correct System Design, 2015

2014
Complete proof systems for weighted modal logic.
Theor. Comput. Sci., 2014

Robust synthesis for real-time systems.
Theor. Comput. Sci., 2014

Formal verification and simulation for platform screen doors and collision avoidance in subway control systems.
STTT, 2014

A modal specification theory for components with data.
Sci. Comput. Program., 2014

Lower-bound-constrained runs in weighted timed automata.
Perform. Eval., 2014

Stuttering for Abstract Probabilistic Automata.
J. Log. Algebr. Program., 2014

Adequacy and Complete Axiomatization for Timed Modal Logic.
Electr. Notes Theor. Comput. Sci., 2014

Refinement and Difference for Probabilistic Automata
Logical Methods in Computer Science, 2014

Topologies of Stochastic Markov Models: Computational Aspects.
CoRR, 2014

Efficient controller synthesis for a fragment of MTL0,∞.
Acta Inf., 2014

Proceedings of the 2014 Theoretical Aspects of Software Engineering Conference, 2014

Continuity Properties of Distances for Markov Processes.
Proceedings of the Quantitative Evaluation of Systems - 11th International Conference, 2014

Verification and Performance Analysis of Embedded and Cyber-Physical Systems using UPPAAL.
Proceedings of the PECCS 2014, 2014

Memory Efficient Data Structures for Explicit Verification of Timed Systems.
Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

Battery-Aware Scheduling of Mixed Criticality Systems.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014

Statistical Model Checking Past, Present, and Future - (Track Introduction).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014

A Decidable Recursive Logic for Weighted Transition Systems.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014

Compositional Schedulability Analysis of An Avionics System Using UPPAAL.
Proceedings of the 1st International Conference on Advanced Aspects of Software Engineering, 2014

Synchronizing Words for Weighted and Timed Automata.
Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014

Verification and Performance Evaluation of Timed Game Strategies.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2014

Widening the Schedulability of Hierarchical Scheduling Systems.
Proceedings of the Formal Aspects of Component Software - 11th International Symposium, 2014

Parametric and Quantitative Extensions of Modal Transition Systems.
Proceedings of the From Programs to Systems. The Systems perspective in Computing, 2014

Decidability and Expressiveness of Recursive Weighted Logic.
Proceedings of the Perspectives of System Informatics, 2014

Model Checking Process Algebra of Communicating Resources for Real-Time Systems.
Proceedings of the 26th Euromicro Conference on Real-Time Systems, 2014

Synchronizing Strategies under Partial Observability.
Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

Bisimulation on Markov Processes over Arbitrary Measurable Spaces.
Proceedings of the Horizons of the Mind. A Tribute to Prakash Panangaden, 2014

On Time with Minimal Expected Cost!
Proceedings of the Automated Technology for Verification and Analysis, 2014

Quantified Dynamic Metric Temporal Logic for Dynamic Networks of Stochastic Hybrid Automata.
Proceedings of the 14th International Conference on Application of Concurrency to System Design, 2014

2013
Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems.
Proceedings of the Engineering Dependable Software Systems, 2013

Abstract Probabilistic Automata.
Inf. Comput., 2013

Weighted modal transition systems.
Formal Methods in System Design, 2013

Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata.
ECEASST, 2013

On-the-Fly Exact Computation of Bisimilarity Distances.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Local Model Checking of Weighted CTL with Upper-Bound Constraints.
Proceedings of the Model Checking Software - 20th International Symposium, 2013

Refinement and Difference for Probabilistic Automata.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

The BisimDist Library: Efficient Computation of Bisimilarity Distances for Markovian Models.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

Remote Testing of Timed Specifications.
Proceedings of the Testing Software and Systems, 2013

Optimizing Control Strategy Using Statistical Model Checking.
Proceedings of the NASA Formal Methods, 2013

Computing Behavioral Distances, Compositionally.
Proceedings of the Mathematical Foundations of Computer Science 2013, 2013

Stone Duality for Markov Processes.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Stuttering for Abstract Probabilistic Automata.
Proceedings of the Logical Foundations of Computer Science, International Symposium, 2013

TetaSARTS: a tool for modular timing analysis of safety critical Java systems.
Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems, 2013

Priced Timed Automata and Statistical Model Checking.
Proceedings of the Integrated Formal Methods, 10th International Conference, 2013

Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems.
Proceedings of the Unifying Theories of Programming and Formal Engineering Methods, 2013

Probabilistic Modal Specifications (Invited Extended Abstract).
Proceedings of the Formal Aspects of Component Software - 10th International Symposium, 2013

Hierarchical Scheduling Framework Based on Compositional Analysis Using Uppaal.
Proceedings of the Formal Aspects of Component Software - 10th International Symposium, 2013

Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

On the Relationship between LTL Normal Forms and Büchi Automata.
Proceedings of the Theories of Programming and Formal Methods, 2013

Optimal Bounds for Multiweighted and Parametrised Energy Games.
Proceedings of the Theories of Programming and Formal Methods, 2013

Tools for Model-Checking Timed Systems.
Proceedings of the Communicating Embedded Systems, 2013

2012
Compositional verification of real-time systems using Ecdar.
STTT, 2012

New results for Constraint Markov Chains.
Perform. Eval., 2012

Extending modal transition systems with structured labels.
Mathematical Structures in Computer Science, 2012

Reachability analysis for timed automata using max-plus algebra.
J. Log. Algebr. Program., 2012

Modal transition systems with weight intervals.
J. Log. Algebr. Program., 2012

Consistency and refinement for Interval Markov Chains.
J. Log. Algebr. Program., 2012

EXPTIME-completeness of thorough refinement on modal transition systems.
Inf. Comput., 2012

MDM: A Mode Diagram Modeling Framework
Proceedings of the Proceedings First International Workshop on Formal Techniques for Safety-Critical Systems, 2012

Learning Markov Decision Processes for Model Checking
Proceedings of the Proceedings Quantities in Formal Methods, 2012

Parameterized Metatheory for Continuous Markovian Logic
Proceedings of the Proceedings Quantities in Formal Methods, 2012

Time-Darts: A Data Structure for Verification of Closed Timed Automata
Proceedings of the Proceedings Seventh Conference on Systems Software Verification, 2012

Continuous Markovian Logics - Axiomatization and Quantified Metatheory
Logical Methods in Computer Science, 2012

Weighted Modal Transition Systems
CoRR, 2012

Statistical Model Checking for Stochastic Hybrid Systems
Proceedings of the Proceedings First International Workshop on Hybrid Systems and Biology, 2012

On the Relationship between LTL Normal Forms and Buechi Automata
CoRR, 2012

Controllers with Minimal Observation Power (Application to Timed Systems)
CoRR, 2012

UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
Proceedings of the Proceedings 10th Workshop on Quantitative Aspects of Programming Languages and Systems, 2012

MDM: A Mode Diagram Modeling Framework for Periodic Control Systems
CoRR, 2012

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example
CoRR, 2012

Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach
Proceedings of the Proceedings Second International Workshop on Interactions, 2012

An evaluation framework for energy aware buildings using statistical model checking.
SCIENCE CHINA Information Sciences, 2012

Quantitative Modal Transition Systems.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2012

A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata.
Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012

Rewrite-Based Statistical Model Checking of WMTL.
Proceedings of the Runtime Verification, Third International Conference, 2012

Lower-Bound Constrained Runs in Weighted Timed Automata.
Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012

Learning Markov Models for Stationary System Behaviors.
Proceedings of the NASA Formal Methods, 2012

Checking and Distributing Statistical Model Checking.
Proceedings of the NASA Formal Methods, 2012

Taking It to the Limit: Approximate Reasoning for Markov Processes.
Proceedings of the Mathematical Foundations of Computer Science 2012, 2012

Action Investment Energy Games.
Proceedings of the Mathematical and Engineering Methods in Computer Science, 2012

Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Dual-Priced Modal Transition Systems with Time Durations.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Nash Equilibria in Concurrent Priced Games.
Proceedings of the Language and Automata Theory and Applications, 2012

Schedulability Analysis Abstractions for Safety Critical Java.
Proceedings of the 15th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, 2012

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

Runtime Verification of Biological Systems.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, 2012

Schedulability of Herschel-Planck Revisited Using Statistical Model Checking.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, 2012

Statistical Model Checking, Refinement Checking, Optimization, ... for Stochastic Hybrid Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2012

Multi-core Reachability for Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2012

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example.
Proceedings of the FM 2012: Formal Methods, 2012

Moving from Specifications to Contracts in Component-Based Design.
Proceedings of the Fundamental Approaches to Software Engineering, 2012

Code-level timing analysis of embedded software: emsoft'12 invited talk session outline.
Proceedings of the 12th International Conference on Embedded Software, 2012

State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems.
Proceedings of the 2012 Design, Automation & Test in Europe Conference & Exhibition, 2012

Controllers with Minimal Observation Power (Application to Timed Systems).
Proceedings of the Automated Technology for Verification and Analysis, 2012

2011
Model-Based Verification and Analysis for Real-Time Systems.
Proceedings of the Software and Systems Safety - Specification and Verification, 2011

Metrics for weighted transition systems: Axiomatization and complexity.
Theor. Comput. Sci., 2011

Constraint Markov Chains.
Theor. Comput. Sci., 2011

Developing UPPAAL over 15 years.
Softw., Pract. Exper., 2011

Distributed Parametric and Statistical Model Checking
Proceedings of the Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, 2011

Distances for Weighted Transition Systems: Games and Properties
Proceedings of the Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages, 2011

Stochastic Semantics and Statistical Model Checking for Networks of Priced Timed Automata
CoRR, 2011

Quantitative analysis of real-time systems using priced timed automata.
Commun. ACM, 2011

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

Adaptable Value-Set Analysis for Low-Level Code.
Proceedings of the 6th International Workshop on Systems Software Verification, 2011

Learning Probabilistic Automata for Model Checking.
Proceedings of the Eighth International Conference on Quantitative Evaluation of Systems, 2011

APAC: A Tool for Reasoning about Abstract Probabilistic Automata.
Proceedings of the Eighth International Conference on Quantitative Evaluation of Systems, 2011

Monitoring Dynamical Signals While Testing Timed Aspects of a System.
Proceedings of the Testing Software and Systems, 2011

opaal: A Lattice Model Checker.
Proceedings of the NASA Formal Methods, 2011

Quantitative Refinement for Weighted Modal Transition Systems.
Proceedings of the Mathematical Foundations of Computer Science 2011, 2011

Decision Problems for Interval Markov Chains.
Proceedings of the Language and Automata Theory and Applications, 2011

Energy Games in Multiweighted Automata.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2011 - 8th International Colloquium, Johannesburg, South Africa, August 31, 2011

Modular Markovian Logic.
Proceedings of the Automata, Languages and Programming - 38th International Colloquium, 2011

Robust Specification of Real Time Components.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2011

Statistical Model Checking for Networks of Priced Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2011

A Modal Specification Theory for Components with Data.
Proceedings of the Formal Aspects of Component Software - 8th International Symposium, 2011

Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas.
Proceedings of the Computer Science Logic, 2011

Timed Automata Can Always Be Made Implementable.
Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Time for Statistical Model Checking of Real-Time Systems.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Parametric Modal Transition Systems.
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
Modal and mixed specifications: key decision problems and their complexities.
Mathematical Structures in Computer Science, 2010

Quantitative analysis of weighted transition systems.
J. Log. Algebr. Program., 2010

Scenario-based verification of real-time systems using Uppaal.
Formal Methods in System Design, 2010

Present and Absent Sets: Abstraction for Testing of Reactive Systems with Databases.
Electr. Notes Theor. Comput. Sci., 2010

On Zone-Based Analysis of Duration Probabilistic Automata
Proceedings of the Proceedings 12th International Workshop on Verification of Infinite-State Systems, 2010

METAMOC: Modular Execution Time Analysis using Model Checking.
Proceedings of the 10th International Workshop on Worst-Case Execution Time Analysis, 2010

New Results on Timed Specifications.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2010

Symbolic and Compositional Reachability for Timed Automata.
Proceedings of the Reachability Problems, 4th International Workshop, 2010

Compositional Design Methodology with Constraint Markov Chains.
Proceedings of the QEST 2010, 2010

Schedulability Analysis Using Uppaal: Herschel-Planck Case Study.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

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

Timed I/O automata: a complete specification theory for real-time systems.
Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, 2010

Timed automata with observers under energy constraints.
Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, 2010

Testing Real-Time Systems under Uncertainty.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

Application of Model-Checking Technology to Controller Synthesis.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

Quantitative system validation in model driven design.
Proceedings of the 10th International conference on Embedded software, 2010

Scenario-based analysis and synthesis of real-time systems using uppaal.
Proceedings of the Design, Automation and Test in Europe, 2010

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

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

ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2010

2009
On determinism in modal transition systems.
Theor. Comput. Sci., 2009

Discounting in Time.
Electr. Notes Theor. Comput. Sci., 2009

Discount-Optimal Infinite Runs in Priced Timed Automata.
Electr. Notes Theor. Comput. Sci., 2009

EXPTIME-complete Decision Problems for Modal and Mixed Specifications.
Electr. Notes Theor. Comput. Sci., 2009

Teaching Concurrency: Theory in Practice.
Proceedings of the Teaching Formal Methods, Second International Conference, 2009

Verification and Performance Analysis for Embedded Systems.
Proceedings of the TASE 2009, 2009

A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic.
Proceedings of the Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2009

Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete.
Proceedings of the Theoretical Aspects of Computing, 2009

Timed Testing under Partial Observability.
Proceedings of the Second International Conference on Software Testing Verification and Validation, 2009

Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study.
Proceedings of the Hybrid Systems: Computation and Control, 12th International Conference, 2009

Priced Timed Automata: Theory and Tools.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2009

Verification, Performance Analysis and Controller Synthesis for Real-Time Systems.
Proceedings of the Fundamentals of Software Engineering, 2009

Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2009

Methodologies for Specification of Real-Time Systems Using Timed I/O Automata.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

Verifying Real-Time Systems against Scenario-Based Requirements.
Proceedings of the FM 2009: Formal Methods, 2009

Model-Based GUI Testing Using Uppaal at Novo Nordisk.
Proceedings of the FM 2009: Formal Methods, 2009

Compositional and Quantitative Model Checking (Extended Abstract).
Proceedings of the Perspectives of Systems Informatics, 2009

Playing Games with Timed Games.
Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems, 2009

2008
Optimal reachability for multi-priced timed automata.
Theor. Comput. Sci., 2008

Model Checking One-Clock Priced Timed Automata.
Logical Methods in Computer Science, 2008

Optimal infinite scheduling for multi-priced timed automata.
Formal Methods in System Design, 2008

Cooperative Testing of Timed Systems.
Electr. Notes Theor. Comput. Sci., 2008

20 Years of Modal and Mixed Specifications.
Bulletin of the EATCS, 2008

Model Checking One-clock Priced Timed Automata
CoRR, 2008

Fast Directed Model Checking Via Russian Doll Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Model-based schedulability analysis of safety critical hard real-time Java programs.
Proceedings of the 6th International Workshop on Java Technologies for Real-time and Embedded Systems, 2008

Complexity of Decision Problems for Mixed and Modal Specifications.
Proceedings of the Foundations of Software Science and Computational Structures, 2008

Testing Real-Time Systems Using UPPAAL.
Proceedings of the Formal Methods and Testing, 2008

Infinite Runs in Weighted Timed Automata with Energy Constraints.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2008

A Game-Theoretic Approach to Real-Time System Testing.
Proceedings of the Design, Automation and Test in Europe, 2008

2007
Modeling software product lines using color-blind transition systems.
STTT, 2007

Complexity in Simplicity: Flexible Agent-Based State Space Exploration.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Model-Checking One-Clock Priced Timed Automata.
Proceedings of the Foundations of Software Science and Computational Structures, 2007

Guided Controller Synthesis for Climate Controller Using Uppaal Tiga.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2007

Automatic Abstraction Refinement for Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2007

Modal I/O Automata for Interface and Product Line Theories.
Proceedings of the Programming Languages and Systems, 2007

On Modal Refinement and Consistency.
Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007

UPPAAL-Tiga: Time for Playing Games!
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Timed Control with Observation Based and Stuttering Invariant Strategies.
Proceedings of the Automated Technology for Verification and Analysis, 2007

2006
Lower and upper bounds in zone-based abstractions of timed automata.
STTT, 2006

CyNC: A method for real time analysis of systems with cyclic data flows.
J. Embedded Computing, 2006

On using priced timed automata to achieve optimal scheduling.
Formal Methods in System Design, 2006

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

Almost Optimal Strategies in One Clock Priced Timed Games.
Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006

Model Checking Timed Automata with Priorities Using DBM Subtraction.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2006

Interface Input/Output Automata.
Proceedings of the FM 2006: Formal Methods, 2006

Introducing synchronisation in deterministic network models.
Proceedings of the ISCA 19th International Conference on Computer Applications in Industry and Engineering, 2006

2005
Optimal scheduling using priced timed automata.
SIGMETRICS Performance Evaluation Review, 2005

Synthesis of Optimal Strategies Using HyTech.
Electr. Notes Theor. Comput. Sci., 2005

An approach to handle real time and probabilistic behaviors in e-commerce: validating the SET protocol.
Proceedings of the 2005 ACM Symposium on Applied Computing (SAC), 2005

Optimal Conditional Reachability for Multi-priced Timed Automata.
Proceedings of the Foundations of Software Science and Computational Structures, 2005

Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2005

Color-Blind Specifications for Transformations of Reactive Synchronous Programs.
Proceedings of the Fundamental Approaches to Software Engineering, 2005

Testing real-time embedded software using UPPAAL-TRON: an industrial case study.
Proceedings of the EMSOFT 2005, 2005

Efficient On-the-Fly Algorithms for the Analysis of Timed Games.
Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005

Network Calculus for Real Time Analysis of Embedded Systems with Cyclic Task Dependencies.
Proceedings of the 20th International Conference on Computers and Their Applications, 2005

2004
Resource-Optimal Scheduling Using Priced Timed Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Lower and Upper Bounds in Zone Based Abstractions of Timed Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

A Tutorial on Uppaal.
Proceedings of the Formal Methods for the Design of Real-Time Systems, 2004

T-UPPAAL: Online Model-based Testing of Real-Time Systems.
Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 2004

Staying Alive as Cheaply as Possible.
Proceedings of the Hybrid Systems: Computation and Control, 7th International Workshop, 2004

Optimal Strategies in Priced Timed Game Automata.
Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

Priced Timed Automata: Algorithms and Applications.
Proceedings of the Formal Methods for Components and Objects, 2004

Online Testing of Real-time Systems Using Uppaal.
Proceedings of the Formal Approaches to Software Testing, 4th International Workshop, 2004

Online Testing of Real-Time Systems Using UPPAAL: Status and Future Work.
Proceedings of the Perspectives of Model-Based Testing, 5.-10. September 2004, 2004

2003
The power of reachability testing for timed automata.
Theor. Comput. Sci., 2003

Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems.
Real-Time Systems, 2003

Regular languages definable by Lindström quantifiers.
ITA, 2003

Static Guard Analysis in Timed Automata Verification.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Unification & Sharing in Timed Automata Verification.
Proceedings of the Model Checking Software, 2003

Time-Optimal Test Cases for Real-Time Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems: First International Workshop, 2003

Proceedings of the Formal Modeling and Analysis of Timed Systems: First International Workshop, 2003

Time-Optimal Real-Time Test Case Generation Using Uppaal.
Proceedings of the Formal Approaches to Software Testing, 2003

Resource-Efficient Scheduling for Real Time Systems.
Proceedings of the Embedded Software, Third International Conference, 2003

To Store or Not to Store.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002
Automated verification of an audio-control protocol using UPPAAL.
J. Log. Algebr. Program., 2002

Verification of Hierarchical State/Event Systems using Reusability and Compositionality.
Formal Methods in System Design, 2002

Exact Acceleration of Real-Time Model Checking.
Electr. Notes Theor. Comput. Sci., 2002

A Tool Architecture for the Next Generation of Uppaal.
Proceedings of the Formal Methods at the Crossroads. From Panacea to Foundational Support, 2002

Reduction and Refinement Strategies for Probabilistic Analysis.
Proceedings of the Process Algebra and Probabilistic Methods, 2002

UPPAAL Implementation Secrets.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

2001
Guided Synthesis of Control Programs Using UPPAAL.
Nord. J. Comput., 2001

Verification of Large State/Event Systems Using Compositionality and Dependency Analysis.
Formal Methods in System Design, 2001

Reachability Analysis of Probabilistic Systems by Successive Refinements.
Proceedings of the Process Algebra and Probabilistic Methods, 2001

Minimum-Cost Reachability for Priced Timed Automata.
Proceedings of the Hybrid Systems: Computation and Control, 4th International Workshop, 2001

As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

Probabilistic Extensions of Process Algebras.
Proceedings of the Handbook of Process Algebra, 2001

2000
Practical Verification of Embedded Software.
IEEE Computer, 2000

UPPAAL - Now, Next, and Future.
Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 2000

Guided Synthesis of Control Programs Using UPPAAL.
Proceedings of the 2000 ICDCS Workshops, April 10, 2000, Taipei, Taiwan, ROC, 2000

Scaling up Uppaal Automatic Verification of Real-Time Systems Using Compositionality and Abstraction.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2000

Model-checking real-time control programs: verifying Lego(R) MindstormsTM systems using UPPAAL.
Proceedings of the 12th Euromicro Conference on Real-Time Systems (ECRTS 2000), 2000

The Impressive Power of Stopwatches.
Proceedings of the CONCUR 2000, 2000

Verification of Timed and Hybrid Systems.
Proceedings of the Application and Theory of Petri Nets 2000, 2000

1999
Clock Difference Diagrams.
Nord. J. Comput., 1999

Verification of Hierarchical State/Event Systems Using Reusability and Compositionality.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1999

Efficient Timed Reachability Analysis Using Clock Difference Diagrams.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL.
Proceedings of the Formal Methods for Real-Time and Probabilistic Systems, 1999

1998
Verification of Large State/Event Systems Using Compositionality and Dependency Analysis.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

Model Checking via Reachability Testing for Timed Automata.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

The Power of Reachability Testing for Timed Automata.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1998

CMC: A Tool for Compositional Model-Checking of Real-Time Systems.
Proceedings of the Formal Description Techniques and Protocol Specification, 1998

1997
Continuous Modeling of Real-Time and Hybrid Systems: From Concepts to Tools.
STTT, 1997

UPPAAL in a Nutshell.
STTT, 1997

Time-abstracted Bisimulation: Implicit Specifications and Decidability.
Inf. Comput., 1997

A Compositional Proof of a Real-Time Mutual Exclusion Protocol.
Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

Efficient verification of real-time systems: compact data structure and state-space reduction.
Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS '97), 1997

Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL.
Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS '97), 1997

UPPAAL: Status & Developments.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1996
UPPAAL in 1995.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1996

Modelling and analysis of a collision avoidance protocol using Spin and Uppaal.
Proceedings of the Spin Verification System, 1996

Verification of an Audio Protocol with Bus Collision Using UPPAAL.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995
Synthesizing Distinguishing Formulae for Real Time Systems.
Nord. J. Comput., 1995

Generality in Design and Compositional Verification Using TAV.
Formal Methods in System Design, 1995

A Constraint Oriented Proof Methodology Based on Modal Transition Systems.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1995

Compositional and Symbolic Model-Checking of Real-Time Systems.
Proceedings of the 16th IEEE Real-Time Systems Symposium, 1995

From Timed Automata to Logic - and Back.
Proceedings of the Mathematical Foundations of Computer Science 1995, 1995

Synthesizing Distinguishing Formulae for Real Time Systems (Extended Abstract).
Proceedings of the Mathematical Foundations of Computer Science 1995, 1995

Automatic Synthesis of Real Time Systems.
Proceedings of the Automata, Languages and Programming, 22nd International Colloquium, 1995

Fischer's Protocol Revisited: A Simple Proof Using Modal Constraints.
Proceedings of the Hybrid Systems III: Verification and Control, 1995

Diagnostic Model-Checking for Real-Time Systems.
Proceedings of the Hybrid Systems III: Verification and Control, 1995

UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems.
Proceedings of the Hybrid Systems III: Verification and Control, 1995

Model-Checking for Real-Time Systems.
Proceedings of the Fundamentals of Computation Theory, 10th International Symposium, 1995

Compositional Model Checking of Real Time Systems.
Proceedings of the CONCUR '95: Concurrency Theory, 1995

1994
The Fork Calculus.
Nord. J. Comput., 1994

A refinement logic for the fork calculus.
Proceedings of the Protocol Specification, 1994

Automatic verification of real-tim systems using epsilon.
Proceedings of the Protocol Specification, 1994

The Methodology of Modal Constraints.
Proceedings of the Formal Systems Specification, 1994

1993
The Expressive Power of Implicit Specifications.
Theor. Comput. Sci., 1993

Time Abstracted Bisimiulation: Implicit Specifications and Decidability.
Proceedings of the Mathematical Foundations of Programming Semantics, 1993

The Fork Calculus.
Proceedings of the Automata, Languages and Programming, 20nd International Colloquium, 1993

Model Construction for Implicit Specifications in Model Logic.
Proceedings of the CONCUR '93, 1993

Timed Modal Specification - Theory and Tools.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992
A Compositional Protocol Verification Using Relativized Bisimulation
Inf. Comput., July, 1992

Graphical Versus Logical Specifications.
Theor. Comput. Sci., 1992

Testing Probabilistic and Nondeterministic Processes.
Proceedings of the Protocol Specification, 1992

Real-Time Calculi and Expansion Theorems.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1992

Generality in design and compositional verification using TAV.
Proceedings of the Formal Description Techniques, 1992

Compositional Verification of Probabilistic Processes.
Proceedings of the CONCUR '92, 1992

Efficient Local Correctness Checking.
Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

1991
Bisimulation through Probabilistic Testing
Inf. Comput., September, 1991

Using Information Systems to Solve Recursive Domain Equations
Inf. Comput., April, 1991

Partial Specifications and Compositional Verification.
Theor. Comput. Sci., 1991

Compositionality through an Operational Semantics of Contexts.
J. Log. Comput., 1991

On the Complexity of Equation Solving in Process Algebra.
Proceedings of the TAPSOFT'91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1991

Specification and Refinement of Probabilistic Processes
Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

The Expressive Power of Implicit Specifications.
Proceedings of the Automata, Languages and Programming, 18th International Colloquium, 1991

Deciding Properties of Regular Real Time Processes.
Proceedings of the Computer Aided Verification, 3rd International Workshop, 1991

1990
Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion.
Theor. Comput. Sci., 1990

Equation Solving Using Modal Transition Systems
Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

Compositionality Through an Operational Semantics of Contexts.
Proceedings of the Automata, Languages and Programming, 17th International Colloquium, 1990

Ideal Specification Formalism + Expressivity + Compositionality + Decidability + Testability + ...
Proceedings of the CONCUR '90, 1990

Graphical versus Logical Specifications.
Proceedings of the CAAP '90, 1990

1989
Compositional Theories Based on an Operational Semantics of Contexts.
Proceedings of the Stepwise Refinement of Distributed Systems, 1989

Bisimulation Through Probabilistic Testing.
Proceedings of the Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989

The Use of Static Constructs in A Modal Process Logic.
Proceedings of the Logic at Botik '89, 1989

Modal Specifications.
Proceedings of the Automatic Verification Methods for Finite State Systems, 1989

1988
Compositional Proofs by Partial Specification of Processes.
Proceedings of the Mathematical Foundations of Computer Science 1988, 1988

A Modal Process Logic
Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

Proof System for Hennessy-Milner Logic with Recursion.
Proceedings of the CAAP '88, 1988

1987
A Context Dependent Equivalence Between Processes.
Theor. Comput. Sci., 1987

Recursively Defined Doains and their Induction Principles.
Theor. Comput. Sci., 1987

Verifying a Protocol Using Relativized Bisimulation.
Proceedings of the Automata, Languages and Programming, 14th International Colloquium, 1987

1985
A Context Dependent Equivalence between Processes.
Proceedings of the Automata, 1985

Recursively Defined Domains and Their Induction Principles.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1985

1984
Using Information Systems to Solve Recursive Domain Equations Effectively.
Proceedings of the Semantics of Data Types, International Symposium, 1984