Kim G. Larsen

Affiliations:
  • Aalborg University, Department of Computer Science, Denmark


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

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Algorithmic Minimization of Uncertain Continuous-Time Markov Chains.
IEEE Trans. Autom. Control., November, 2023

AllSynth: A BDD-based approach for network update synthesis.
Sci. Comput. Program., August, 2023

A toolchain for domestic heat-pump control using Uppaal Stratego.
Sci. Comput. Program., August, 2023

CGAAL: Distributed On-The-Fly ATL Model Checker with Heuristics.
Proceedings of the Fourteenth International Symposium on Games, 2023

Efficient Simulation of Quantum Circuits by Model Order Reduction.
CoRR, 2023

Energy Consumption Optimization in Radio Access Networks (ECO-RAN).
CoRR, 2023

MM Algorithms to Estimate Parameters in Continuous-time Markov Chains.
CoRR, 2023

Timed I/O Automata: It is never too late to complete your timed specification theory.
CoRR, 2023

Optimality-preserving Reduction of Chemical Reaction Networks.
CoRR, 2023

Welcome Remarks from AISoLA 2023/Track C2 Chairs.
Proceedings of the Bridging the Gap Between AI and Reality, 2023

Shielded Reinforcement Learning for Hybrid Systems.
Proceedings of the Bridging the Gap Between AI and Reality, 2023

Elimination of Detached Regions in Dependency Graph Verification.
Proceedings of the Model Checking Software - 29th International Symposium, 2023

An MM Algorithm to Estimate Parameters in Continuous-Time Markov Chains.
Proceedings of the Quantitative Evaluation of Systems - 20th International Conference, 2023

Safety Verification of Decision-Tree Policies in Continuous Time.
Proceedings of the Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, 2023

Learning Symbolic Timed Models from Concrete Timed Data.
Proceedings of the NASA Formal Methods - 15th International Symposium, 2023

Dual Balancing of SoC/SoT in Smart Batteries Using Reinforcement Learning in Uppaal Stratego.
Proceedings of the 49th Annual Conference of the IEEE Industrial Electronics Society, 2023

Dynamic Extrapolation in Extended Timed Automata.
Proceedings of the Formal Methods and Software Engineering, 2023

Usage-and Risk-Aware Falsification Testing for Cyber-Physical Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2023

Refinement of Systems with an Attacker Focus.
Proceedings of the Formal Methods for Industrial Critical Systems, 2023

Modelling of Hot Water Buffer Tank and Mixing Loop for an Intelligent Heat Pump Control.
Proceedings of the Formal Methods for Industrial Critical Systems, 2023

A Modeling Concept for Formal Verification of OS-Based Compositional Software.
Proceedings of the Fundamental Approaches to Software Engineering, 2023

Comparative Analysis of Uppaal SMC, ns-3 and MATLAB/Simulink.
Proceedings of the Engineering of Computer-Based Systems - 8th International Conference, 2023

Guaranteed safe controller synthesis for switched systems using analytical solutions<sup>*</sup>.
Proceedings of the IEEE Conference on Control Technology and Applications, 2023

Assume-Guarantee Reasoning for Additive Hybrid Behaviour.
Proceedings of the Theories of Programming and Formal Methods, 2023

2022
Randomized reachability analysis in UPPAAL: fast error detection in timed systems.
Int. J. Softw. Tools Technol. Transf., 2022

Extended abstract dependency graphs.
Int. J. Softw. Tools Technol. Transf., 2022

Formal methods and tools for industrial critical systems.
Int. J. Softw. Tools Technol. Transf., 2022

Hierarchical identification of nonlinear hybrid systems in a Bayesian framework.
Inf. Comput., 2022

A Sigfox Module for the Network Simulator 3.
Proceedings of the WNS3 2022: 2022 Workshop on ns-3, Virtual Event, USA, June 22, 2022

AllSynth: Transiently Correct Network Update Synthesis Accounting for Operator Preferences.
Proceedings of the Theoretical Aspects of Software Engineering, 2022

End-to-End Heat-Pump Control Using Continuous Time Stochastic Modelling and Uppaal Stratego.
Proceedings of the Theoretical Aspects of Software Engineering, 2022

Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals.
Proceedings of the Model Checking Software - 28th International Symposium, 2022

Monte Carlo Tree Search for Priced Timed Automata.
Proceedings of the Quantitative Evaluation of Systems - 19th International Conference, 2022

Balancing Flexible Production and Consumption of Energy using Resource Timed Automata.
Proceedings of the 11th Mediterranean Conference on Embedded Computing, 2022

Automata Learning Meets Shielding.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

Formal Methods Meet Machine Learning (F3ML).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning, 2022

Importance Splitting in Uppaal.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning, 2022

Monitoring Timed Properties (Revisited).
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2022

Simulation Relations and Applications in Formal Methods.
Proceedings of the Principles of Systems Design, 2022

Playing Wordle with Uppaal Stratego.
Proceedings of the A Journey from Process Algebra via Timed Automata to Model Learning, 2022

Convex Lattice Equation Systems.
Proceedings of the Principles of Systems Design, 2022

STOMPC: Stochastic Model-Predictive Control with Uppaal Stratego.
Proceedings of the Automated Technology for Verification and Analysis, 2022

Distributed Fleet Management in Noisy Environments via Model-Predictive Control.
Proceedings of the Thirty-Second International Conference on Automated Planning and Scheduling, 2022

2021
ADTLang: a programming language approach to attack defense trees.
Int. J. Softw. Tools Technol. Transf., 2021

Preface to the Special Issue on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2017).
Sci. Comput. Program., 2021

Stubborn Set Reduction for Two-Player Reachability Games.
Log. Methods Comput. Sci., 2021

Computing Probabilistic Bisimilarity Distances for Probabilistic Automata.
Log. Methods Comput. Sci., 2021

Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction.
Fundam. Informaticae, 2021

2018 CAV award.
Formal Methods Syst. Des., 2021

L<sup>*</sup>-based learning of Markov decision processes (extended version).
Formal Aspects Comput., 2021

Optimal and robust controller synthesis using energy timed automata with uncertainty.
Formal Aspects Comput., 2021

Active Learning of Markov Decision Processes using Baum-Welch algorithm (Extended).
CoRR, 2021

Lumpability for Uncertain Continuous-Time Markov Chains.
Proceedings of the Quantitative Evaluation of Systems - 18th International Conference, 2021

Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code.
Proceedings of the Secure IT Systems - 26th Nordic Conference, NordSec 2021, Virtual Event, 2021

Battery Aware Analysis of Sensor Networks in Uppaal SMC.
Proceedings of the 10th Mediterranean Conference on Embedded Computing, 2021

Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods.
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

A Model-Checking Static Analysis of Task-Based Energy Neutrality for Energy Harvesting IoT.
Proceedings of the IEEE Symposium on Computers and Communications, 2021

Active Learning of Markov Decision Processes using Baum-Welch algorithm.
Proceedings of the 20th IEEE International Conference on Machine Learning and Applications, 2021

An Integer Static Analysis for Better Extrapolation in Uppaal.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2021

Stubborn Set Reduction for Timed Reachability and Safety Games.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2021

Quantitative Analysis of Interval Markov Chains.
Proceedings of the Model Checking, Synthesis, and Learning, 2021

A Bayesian Framework for Large-Scale Identification of Nonlinear Hybrid Systems.
Proceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems, 2021

Learning Safe and Optimal Control Strategies for Storm Water Detention Ponds.
Proceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems, 2021

2020
Dependency graphs with applications to verification.
Int. J. Softw. Tools Technol. Transf., 2020

Mixed Nondeterministic-Probabilistic Interfaces.
CoRR, 2020

It's Time to Play Safe: Shield Synthesis for Timed Systems.
CoRR, 2020

A general framework for defining and optimizing robustness.
CoRR, 2020

A complete axiomatization of weighted branching bisimulation.
Acta Informatica, 2020

Randomized Refinement Checking of Timed I/O Automata.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2020

From Statistical Model Checking to Run-Time Monitoring Using a Bayesian Network Approach.
Proceedings of the Runtime Verification - 20th International Conference, 2020

Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2020

30 Years of Statistical Model Checking.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

Fluid Model-Checking in UPPAAL for Covid-19.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

Approximating Euclidean by Imprecise Markov Decision Processes.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

Urgent Partial Order Reduction for Extended Timed Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2020

Synthesis for Multi-weighted Games with Branching-Time Winning Conditions.
Proceedings of the Application and Theory of Petri Nets and Concurrency, 2020

On-the-Fly Synthesis for Strictly Alternating Games.
Proceedings of the Application and Theory of Petri Nets and Concurrency, 2020

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.
Math. Struct. Comput. Sci., 2019

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

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

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

A Faster-Than Relation for Semi-Markov Decision Processes.
Proceedings of the Proceedings 16th Workshop on Quantitative Aspects of Programming Languages and Systems, 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

SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes.
Proceedings of the Quantitative Evaluation of Systems, 16th International Conference, 2019

Model Checking Constrained Markov Reward Models with Uncertainties.
Proceedings of the Quantitative Evaluation of Systems, 16th International Conference, 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<sup>*</sup>-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

Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs.
Proceedings of the Automated Technology for Verification and Analysis, 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.
Int. J. Softw. Tools Technol. Transf., 2018

High-level frameworks for the specification and verification of scheduling problems.
Int. J. Softw. Tools Technol. Transf., 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.
Log. Methods Comput. Sci., 2018

A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains.
Log. Methods Comput. Sci., 2018

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

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

Contracts for System Design.
Found. Trends Electron. Des. Autom., 2018

Complete Axiomatization for the Total Variation Distance of Markov Chains.
Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, 2018

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

Learning Timed Automata via Genetic Programming.
CoRR, 2018

Average-energy games.
Acta Informatica, 2018

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

Analytical Solution for Long Battery Lifetime Prediction in Nonadaptive Systems.
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 31st 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

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.
Log. Methods Comput. Sci., 2017

Reasoning About Bounds in Weighted Transition Systems.
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 MTL<sub>0, ∞</sub>.
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

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.
Int. J. Softw. Tools Technol. Transf., 2016

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

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

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

Formal modelling and analysis of Bitflips in ARM assembly code.
Inf. Syst. Frontiers, 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.
Log. Methods Comput. Sci., 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, 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.
Int. J. Softw. Tools Technol. Transf., 2015

Statistical model checking for biological systems.
Int. J. Softw. Tools Technol. Transf., 2015

Uppaal SMC tutorial.
Int. J. Softw. Tools Technol. Transf., 2015

Schedulability of Herschel revisited using statistical model checking.
Int. J. Softw. Tools Technol. Transf., 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. Algebraic Methods Program., 2015

Alternation-Free Weighted Mu-Calculus: Decidability and Completeness.
Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics, 2015

The EATCS Award 2016 - Call for Nominations.
Bull. EATCS, 2015

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

Refinement checking on parametric modal transition systems.
Acta Informatica, 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

Flexible Framework for Statistical Schedulability Analysis of Probabilistic Sporadic Tasks.
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

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.
Int. J. Softw. Tools Technol. Transf., 2014

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

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

Stuttering for Abstract Probabilistic Automata.
J. Log. Algebraic Methods Program., 2014

Adequacy and Complete Axiomatization for Timed Modal Logic.
Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, 2014

Refinement and Difference for Probabilistic Automata
Log. Methods Comput. Sci., 2014

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

Efficient controller synthesis for a fragment of MTL<sub>0,∞</sub>.
Acta Informatica, 2014

Degree of Schedulability of Mixed-Criticality Real-Time Systems with Probabilistic Sporadic Tasks.
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

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

Verification and Performance Analysis of Embedded and Cyber-Physical Systems using UPPAAL.
Proceedings of the MODELSWARD 2014 - Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development, Lisbon, Portugal, 7, 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 Syst. Des., 2013

Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 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

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

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


2012
Compositional verification of real-time systems using Ecdar.
Int. J. Softw. Tools Technol. Transf., 2012

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

Extending modal transition systems with structured labels.
Math. Struct. Comput. Sci., 2012

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

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

Consistency and refinement for Interval Markov Chains.
J. Log. Algebraic Methods 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
Log. Methods Comput. Sci., 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

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

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.
Sci. China Inf. Sci., 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

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. Exp., 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

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


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

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.
Math. Struct. Comput. Sci., 2010

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

Scenario-based verification of real-time systems using Uppaal.
Formal Methods Syst. Des., 2010

Present and Absent Sets: Abstraction for Testing of Reactive Systems with Databases.
Proceedings of the Sixth Workshop on Model-Based Testing, 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.
Proceedings of Seventh Workshop on Quantitative Aspects of Programming Languages, 2009

Discount-Optimal Infinite Runs in Priced Timed Automata.
Proceedings of the Joint Proceedings of the 8th, 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.
Log. Methods Comput. Sci., 2008

Optimal infinite scheduling for multi-priced timed automata.
Formal Methods Syst. Des., 2008

Cooperative Testing of Timed Systems.
Proceedings of the Fourth Workshop on Model Based Testing, 2008

EXPTIME-complete Decision Problems for Modal and Mixed Specifications.
Proceedings of the 15th Workshop on Expressiveness in Concurrency, 2008

20 Years of Modal and Mixed Specifications.
Bull. EATCS, 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.
Int. J. Softw. Tools Technol. Transf., 2007

Complexity in Simplicity: Flexible Agent-Based State Space Exploration.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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.
Int. J. Softw. Tools Technol. Transf., 2006

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

On using priced timed automata to achieve optimal scheduling.
Formal Methods Syst. Des., 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 Perform. Evaluation Rev., 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
Synthesis of Optimal Strategies Using HyTech.
Proceedings of the Workshop on Games in Design and Verification, 2004

Resource-Optimal Scheduling Using Priced 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 Syst., 2003

Regular languages definable by Lindström quantifiers.
RAIRO Theor. Informatics Appl., 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

Adding Symmetry Reduction to Uppaal.
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. Algebraic Methods Program., 2002

Verification of Hierarchical State/Event Systems using Reusability and Compositionality.
Formal Methods Syst. Des., 2002

Exact Acceleration of Real-Time Model Checking.
Proceedings of the Theory and Practice of Timed Systems, 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 Syst. Des., 2001

Efficient Guiding Towards Cost-Optimality in UPPAAL.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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

UPPAAL - present and future.
Proceedings of the 40th IEEE Conference on Decision and Control, 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.
Computer, 2000

UPPAAL - Now, Next, and Future.
Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 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) Mindstorms<sup>TM</sup> 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

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
Model Checking via Reachability Testing for Timed Automata.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 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.
Int. J. Softw. Tools Technol. Transf., 1997

UPPAAL in a Nutshell.
Int. J. Softw. Tools Technol. Transf., 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 Syst. Des., 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

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 NAPAW 92, 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

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

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

1989
Compositional Theories Based on an Operational Semantics of Contexts.
Proceedings of the Stepwise Refinement of Distributed Systems, 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
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


  Loading...