Using Information Systems to Solve Recursive Domain Equations Effectively. - Glynn Winskel; Kim Guldstrand Larsen (Semantics of Data Types, 1984)

Recursively Defined Domains and Their Induction Principles. - Finn Verner Jensen; Kim Guldstrand Larsen (FSTTCS, 1985)

A Context Dependent Equivalence between Processes. - Kim Guldstrand Larsen (ICALP, 1985)

Verifying a Protocol Using Relativized Bisimulation. - Kim Guldstrand Larsen; Robin Milner (ICALP, 1987)

Recursively Defined Doains and their Induction Principles. - Finn Verner Jensen; Kim Guldstrand Larsen (Theor. Comput. Sci., 1987)

Proof System for Hennessy-Milner Logic with Recursion. - Kim Guldstrand Larsen (CAAP, 1988)

A Modal Process Logic - Kim Guldstrand Larsen; Bent Thomsen (LICS, 1988)

Compositional Proofs by Partial Specification of Processes. - Kim Guldstrand Larsen; Bent Thomsen (MFCS, 1988)

Modal Specifications. - Kim Guldstrand Larsen (Automatic Verification Methods for Finite State Systems, 1989)

The Use of Static Constructs in A Modal Process Logic. - Hans Hüttel; Kim Guldstrand Larsen (Logic at Botik, 1989)

Bisimulation Through Probabilistic Testing. - Kim Guldstrand Larsen; Arne Skou (POPL, 1989)

Compositional Theories Based on an Operational Semantics of Contexts. - Kim Guldstrand Larsen (REX Workshop, 1989)

Graphical versus Logical Specifications. - Gérard Boudol; Kim Guldstrand Larsen (CAAP, 1990)

Ideal Specification Formalism + Expressivity + Compositionality + Decidability + Testability + ... - Kim Guldstrand Larsen (CONCUR, 1990)

Compositionality Through an Operational Semantics of Contexts. - Kim Guldstrand Larsen; Xinxin Liu (ICALP, 1990)

Equation Solving Using Modal Transition Systems - Kim Guldstrand Larsen; Xinxin Liu (LICS, 1990)

Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion. - Kim Guldstrand Larsen (Theor. Comput. Sci., 1990)

Deciding Properties of Regular Real Time Processes. - Uno Holmer; Kim Guldstrand Larsen; Wang Yi 001 (CAV, 1991)

The Expressive Power of Implicit Specifications. - Kim Guldstrand Larsen (ICALP, 1991)

Specification and Refinement of Probabilistic Processes - Bengt Jonsson 001; Kim Guldstrand Larsen (LICS, 1991)

On the Complexity of Equation Solving in Process Algebra. - Bengt Jonsson 001; Kim Guldstrand Larsen (TAPSOFT, Vol.1, 1991)

Partial Specifications and Compositional Verification. - Kim Guldstrand Larsen; Bent Thomsen (Theor. Comput. Sci., 1991)

Using Information Systems to Solve Recursive Domain Equations - Kim Guldstrand Larsen; Glynn Winskel (Inf. Comput., 1991)

Efficient Local Correctness Checking. - Kim Guldstrand Larsen (CAV, 1992)

Compositional Verification of Probabilistic Processes. - Kim Guldstrand Larsen; Arne Skou (CONCUR, 1992)

Generality in design and compositional verification using TAV. - Anders Børjesson; Kim Guldstrand Larsen; Arne Skou (FORTE, 1992)

Real-Time Calculi and Expansion Theorems. - Jens Chr. Godskesen; Kim Guldstrand Larsen (FSTTCS, 1992)

Testing Probabilistic and Nondeterministic Processes. - Wang Yi 001; Kim Guldstrand Larsen (PSTV, 1992)

A Compositional Protocol Verification Using Relativized Bisimulation - Kim Guldstrand Larsen; Robin Milner (Inf. Comput., 1992)

Timed Modal Specification - Theory and Tools. - Karlis Cerans; Jens Chr. Godskesen; Kim Guldstrand Larsen (CAV, 1993)

Model Construction for Implicit Specifications in Model Logic. - Ole Høgh Jensen; Jarl Tuxen Lang; Christian Jeppesen; Kim Guldstrand Larsen (CONCUR, 1993)

The Fork Calculus. - Klaus Havelund; Kim Guldstrand Larsen (ICALP, 1993)

Time Abstracted Bisimiulation: Implicit Specifications and Decidability. - Kim Guldstrand Larsen; Wang Yi 001 (MFPS, 1993)

The Methodology of Modal Constraints. - Kim Guldstrand Larsen; Bernhard Steffen; Carsten Weise (Formal Systems Specification, 1994)

Automatic verification of real-tim systems using epsilon. - Jens Chr. Godskesen; Kim Guldstrand Larsen; Arne Skou (PSTV, 1994)

A refinement logic for the fork calculus. - Klaus Havelund; Kim Guldstrand Larsen (PSTV, 1994)

Compositional Model Checking of Real Time Systems. - François Laroussinie; Kim Guldstrand Larsen (CONCUR, 1995)

Model-Checking for Real-Time Systems. - Kim Guldstrand Larsen; Paul Pettersson; Wang Yi 001 (FCT, 1995)

UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems. - Johan Bengtsson; Kim Guldstrand Larsen; Fredrik Larsson; Paul Pettersson; Wang Yi 001 (Hybrid Systems, 1995)

Diagnostic Model-Checking for Real-Time Systems. - Kim Guldstrand Larsen; Paul Pettersson; Wang Yi 001 (Hybrid Systems, 1995)

Fischer's Protocol Revisited: A Simple Proof Using Modal Constraints. - Kim Guldstrand Larsen; Bernhard Steffen; Carsten Weise (Hybrid Systems, 1995)

Automatic Synthesis of Real Time Systems. - Jørgen H. Andersen; Kåre J. Kristoffersen; Kim Guldstrand Larsen; Jesper Niedermann (ICALP, 1995)

Synthesizing Distinguishing Formulae for Real Time Systems (Extended Abstract). - Jens Chr. Godskesen; Kim Guldstrand Larsen (MFCS, 1995)

From Timed Automata to Logic - and Back. - François Laroussinie; Kim Guldstrand Larsen; Carsten Weise (MFCS, 1995)

Compositional and Symbolic Model-Checking of Real-Time Systems. - Kim Guldstrand Larsen; Paul Pettersson; Wang Yi 001 (RTSS, 1995)

A Constraint Oriented Proof Methodology Based on Modal Transition Systems. - Kim Guldstrand Larsen; Bernhard Steffen; Carsten Weise (TACAS, 1995)

Synthesizing Distinguishing Formulae for Real Time Systems. - Jens Chr. Godskesen; Kim Guldstrand Larsen (Nord. J. Comput., 1995)

Verification of an Audio Protocol with Bus Collision Using UPPAAL. - Johan Bengtsson; W. O. David Griffioen; Kåre J. Kristoffersen; Kim Guldstrand Larsen; Fredrik Larsson; Paul Pettersson; Wang Yi 001 (CAV, 1996)

Modelling and analysis of a collision avoidance protocol using Spin and Uppaal. - Henrik Ejersbo Jensen; Kim G. Larsen; Arne Skou (The Spin Verification System, 1996)

UPPAAL in 1995. - Johan Bengtsson; Kim Guldstrand Larsen; Fredrik Larsson; Paul Pettersson; Wang Yi 001 (TACAS, 1996)

UPPAAL: Status & Developments. - Kim Guldstrand Larsen; Paul Pettersson; Wang Yi 001 (CAV, 1997)

Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL. - Klaus Havelund; Arne Skou; Kim Guldstrand Larsen; Kristian Lund (RTSS, 1997)

Efficient verification of real-time systems: compact data structure and state-space reduction. - Kim Guldstrand Larsen; Fredrik Larsson; Paul Pettersson; Wang Yi 001 (RTSS, 1997)

A Compositional Proof of a Real-Time Mutual Exclusion Protocol. - Kåre J. Kristoffersen; François Laroussinie; Kim Guldstrand Larsen; Paul Pettersson; Wang Yi 001 (TAPSOFT, 1997)

Time-abstracted Bisimulation: Implicit Specifications and Decidability. - Kim Guldstrand Larsen; Wang Yi 001 (Inf. Comput., 1997)

UPPAAL in a Nutshell. - Kim Guldstrand Larsen; Paul Pettersson; Wang Yi 001 (Int. J. Softw. Tools Technol. Transf., 1997)

Continuous Modeling of Real-Time and Hybrid Systems: From Concepts to Tools. - Kim Guldstrand Larsen; Bernhard Steffen; Carsten Weise (Int. J. Softw. Tools Technol. Transf., 1997)

CMC: A Tool for Compositional Model-Checking of Real-Time Systems. - François Laroussinie; Kim Guldstrand Larsen (FORTE, 1998)

The Power of Reachability Testing for Timed Automata. - Luca Aceto; Patricia Bouyer; Augusto Burgueño; Kim Guldstrand Larsen (FSTTCS, 1998)

Model Checking via Reachability Testing for Timed Automata. - Luca Aceto; Augusto Burgueño; Kim Guldstrand Larsen (TACAS, 1998)

Verification of Large State/Event Systems Using Compositionality and Dependency Analysis. - Jørn Lind-Nielsen; Henrik Reif Andersen; Gerd Behrmann; Henrik Hulgaard; Kåre J. Kristoffersen; Kim Guldstrand Larsen (TACAS, 1998)

Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL. - Klaus Havelund; Kim Guldstrand Larsen; Arne Skou (ARTS, 1999)

Efficient Timed Reachability Analysis Using Clock Difference Diagrams. - Gerd Behrmann; Kim Guldstrand Larsen; Justin Pearson; Carsten Weise; Wang Yi 001 (CAV, 1999)

Verification of Hierarchical State/Event Systems Using Reusability and Compositionality. - Gerd Behrmann; Kim Guldstrand Larsen; Henrik Reif Andersen; Henrik Hulgaard; Jørn Lind-Nielsen (TACAS, 1999)

Clock Difference Diagrams. - Kim Guldstrand Larsen; Justin Pearson; Carsten Weise; Wang Yi 001 (Nord. J. Comput., 1999)

Verification of Timed and Hybrid Systems. - Kim Guldstrand Larsen (ICATPN, 2000)

The Impressive Power of Stopwatches. - Franck Cassez; Kim Guldstrand Larsen (CONCUR, 2000)

Model-checking real-time control programs: verifying Lego(R) MindstormsTM systems using UPPAAL. - Torsten K. Iversen; Kåre J. Kristoffersen; Kim Guldstrand Larsen; Morten Laursen; Rune G. Madsen; Steffen K. Mortensen; Paul Pettersson; Chris B. Thomasen (ECRTS, 2000)

Scaling up Uppaal Automatic Verification of Real-Time Systems Using Compositionality and Abstraction. - Henrik Ejersbo Jensen; Kim Guldstrand Larsen; Arne Skou (FTRTFT, 2000)

Guided Synthesis of Control Programs Using UPPAAL. - Thomas Hune; Kim Guldstrand Larsen; Paul Pettersson (ICDCS Workshop on Distributed System Validation and Verification, 2000)

UPPAAL - Now, Next, and Future. - Tobias Amnell; Gerd Behrmann; Johan Bengtsson; Pedro R. D'Argenio; Alexandre David; Ansgar Fehnker; Thomas Hune; Bertrand Jeannet; Kim Guldstrand Larsen; M. Oliver Möller; Paul Pettersson; Carsten Weise; et al. (MOVEP, 2000)

Practical Verification of Embedded Software. - Jørgen Staunstrup; Henrik Reif Andersen; Henrik Hulgaard; Jørn Lind-Nielsen; Kim Guldstrand Larsen; Gerd Behrmann; Kåre J. Kristoffersen; Arne Skou; Henrik Leerberg; Niels Bo Theilgaard (Computer, 2000)

Probabilistic Extensions of Process Algebras. - Bengt Jonsson 001; Wang Yi 001; Kim G. Larsen (Handbook of Process Algebra, 2001)

As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. - Kim Guldstrand Larsen; Gerd Behrmann; Ed Brinksma; Ansgar Fehnker; Thomas Hune; Paul Pettersson; Judi Romijn (CAV, 2001)

UPPAAL - present and future. - Gerd Behrmann; Kim G. Larsen; Oliver Möller; Alexandre David; Paul Pettersson; Wang Yi 001 (CDC, 2001)

Minimum-Cost Reachability for Priced Timed Automata. - Gerd Behrmann; Ansgar Fehnker; Thomas Hune; Kim Guldstrand Larsen; Paul Pettersson; Judi Romijn; Frits W. Vaandrager (HSCC, 2001)

Reachability Analysis of Probabilistic Systems by Successive Refinements. - Pedro R. D'Argenio; Bertrand Jeannet; Henrik Ejersbo Jensen; Kim Guldstrand Larsen (PAPM-PROBMIV, 2001)

Efficient Guiding Towards Cost-Optimality in UPPAAL. - Gerd Behrmann; Ansgar Fehnker; Thomas Hune; Kim G. Larsen; Paul Pettersson; Judi Romijn (TACAS, 2001)

UPPAAL Implementation Secrets. - Gerd Behrmann; Johan Bengtsson; Alexandre David; Kim Guldstrand Larsen; Paul Pettersson; Wang Yi 001 (FTRTFT, 2002)

Reduction and Refinement Strategies for Probabilistic Analysis. - Pedro R. D'Argenio; Bertrand Jeannet; Henrik Ejersbo Jensen; Kim Guldstrand Larsen (PAPM-PROBMIV, 2002)

A Tool Architecture for the Next Generation of Uppaal. - Alexandre David; Gerd Behrmann; Kim Guldstrand Larsen; Wang Yi 001 (10th Anniversary Colloquium of UNU/IIST, 2002)

Exact Acceleration of Real-Time Model Checking. - Martijn Hendriks; Kim Guldstrand Larsen (Theory and Practice of Timed Systems @ ETAPS, 2002)

Automated verification of an audio-control protocol using UPPAAL. - Johan Bengtsson; W. O. David Griffioen; Kåre J. Kristoffersen; Kim Guldstrand Larsen; Fredrik Larsson; Paul Pettersson; Wang Yi 001 (J. Log. Algebraic Methods Program., 2002)

To Store or Not to Store. - Gerd Behrmann; Kim Guldstrand Larsen; Radek Pelánek (CAV, 2003)

Resource-Efficient Scheduling for Real Time Systems. - Kim Guldstrand Larsen (EMSOFT, 2003)

Time-Optimal Real-Time Test Case Generation Using Uppaal. - Anders Hessel; Kim Guldstrand Larsen; Brian Nielsen; Paul Pettersson; Arne Skou (FATES, 2003)

Adding Symmetry Reduction to Uppaal. - Martijn Hendriks; Gerd Behrmann; Kim Guldstrand Larsen; Peter Niebert; Frits W. Vaandrager (FORMATS, 2003)

Time-Optimal Test Cases for Real-Time Systems. - Anders Hessel; Kim Guldstrand Larsen; Brian Nielsen; Paul Pettersson; Arne Skou (FORMATS, 2003)

Unification & Sharing in Timed Automata Verification. - Alexandre David; Gerd Behrmann; Kim Guldstrand Larsen; Wang Yi 001 (SPIN, 2003)

Static Guard Analysis in Timed Automata Verification. - Gerd Behrmann; Patricia Bouyer; Emmanuel Fleury; Kim Guldstrand Larsen (TACAS, 2003)

Regular languages definable by Lindström quantifiers. - Zoltán Ésik; Kim Guldstrand Larsen (RAIRO Theor. Informatics Appl., 2003)

Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems. - Kim Guldstrand Larsen; Fredrik Larsson; Paul Pettersson; Wang Yi 001 (Real Time Syst., 2003)

Online Testing of Real-Time Systems Using UPPAAL: Status and Future Work. - Kim Guldstrand Larsen; Marius Mikucionis; Brian Nielsen (Perspectives of Model-Based Testing, 2004)

Online Testing of Real-time Systems Using Uppaal. - Kim Guldstrand Larsen; Marius Mikucionis; Brian Nielsen (FATES, 2004)

Priced Timed Automata: Algorithms and Applications. - Gerd Behrmann; Kim Guldstrand Larsen; Jacob Illum Rasmussen (FMCO, 2004)

Optimal Strategies in Priced Timed Game Automata. - Patricia Bouyer; Franck Cassez; Emmanuel Fleury; Kim Guldstrand Larsen (FSTTCS, 2004)

Staying Alive as Cheaply as Possible. - Patricia Bouyer; Ed Brinksma; Kim Guldstrand Larsen (HSCC, 2004)

T-UPPAAL: Online Model-based Testing of Real-Time Systems. - Marius Mikucionis; Kim Guldstrand Larsen; Brian Nielsen (ASE, 2004)

A Tutorial on Uppaal. - Gerd Behrmann; Alexandre David; Kim Guldstrand Larsen (SFM, 2004)

Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. - Gerd Behrmann; Patricia Bouyer; Kim Guldstrand Larsen; Radek Pelánek (TACAS, 2004)

Resource-Optimal Scheduling Using Priced Timed Automata. - Jacob Illum Rasmussen; Kim Guldstrand Larsen; K. Subramani 001 (TACAS, 2004)

Synthesis of Optimal Strategies Using HyTech. - Patricia Bouyer; Franck Cassez; Emmanuel Fleury; Kim Guldstrand Larsen (GDV@CAV, 2004)

Network Calculus for Real Time Analysis of Embedded Systems with Cyclic Task Dependencies. - Henrik Schiøler; Jan Jakob Jessen; Jens Dalsgaard Nielsen; Kim Guldstrand Larsen (CATA, 2005)

Efficient On-the-Fly Algorithms for the Analysis of Timed Games. - Franck Cassez; Alexandre David; Emmanuel Fleury; Kim Guldstrand Larsen; Didier Lime (CONCUR, 2005)

Testing real-time embedded software using UPPAAL-TRON: an industrial case study. - Kim Guldstrand Larsen; Marius Mikucionis; Brian Nielsen; Arne Skou (EMSOFT, 2005)

Color-Blind Specifications for Transformations of Reactive Synchronous Programs. - Kim Guldstrand Larsen; Ulrik Larsen; Andrzej Wasowski (FASE, 2005)

Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness. - Gerd Behrmann; Kim Guldstrand Larsen; Jacob Illum Rasmussen (FORMATS, 2005)

Optimal Conditional Reachability for Multi-priced Timed Automata. - Kim Guldstrand Larsen; Jacob Illum Rasmussen (FoSSaCS, 2005)

An approach to handle real time and probabilistic behaviors in e-commerce: validating the SET protocol. - Gregorio Díaz 001; Kim Guldstrand Larsen; Juan José Pardo; Fernando Cuartero; Valentín Valero (SAC, 2005)

Optimal scheduling using priced timed automata. - Gerd Behrmann; Kim Guldstrand Larsen; Jacob Illum Rasmussen (SIGMETRICS Perform. Evaluation Rev., 2005)

Introducing synchronisation in deterministic network models. - Henrik Schiøler; Jan Jakob Jessen; Jens Dalsgaard Nielsen; Kim Guldstrand Larsen (CAINE, 2006)

Interface Input/Output Automata. - Kim Guldstrand Larsen; Ulrik Nyman; Andrzej Wasowski (FM, 2006)

Model Checking Timed Automata with Priorities Using DBM Subtraction. - Alexandre David; John Håkansson; Kim Guldstrand Larsen; Paul Pettersson (FORMATS, 2006)

Almost Optimal Strategies in One Clock Priced Timed Games. - Patricia Bouyer; Kim Guldstrand Larsen; Nicolas Markey; Jacob Illum Rasmussen (FSTTCS, 2006)

UPPAAL 4.0. - Gerd Behrmann; Alexandre David; Kim Guldstrand Larsen; John Håkansson; Paul Pettersson; Wang Yi 001; Martijn Hendriks (QEST, 2006)

On using priced timed automata to achieve optimal scheduling. - Jacob Illum Rasmussen; Kim Guldstrand Larsen; K. Subramani 001 (Formal Methods Syst. Des., 2006)

CyNC: A method for real time analysis of systems with cyclic data flows. - Henrik Schiøler; Jens Dalsgaard Nielsen; Kim Guldstrand Larsen; Jan Jakob Jessen (J. Embed. Comput., 2006)

Timed Control with Observation Based and Stuttering Invariant Strategies. - Franck Cassez; Alexandre David; Kim Guldstrand Larsen; Didier Lime; Jean-François Raskin (ATVA, 2007)

UPPAAL-Tiga: Time for Playing Games! - Gerd Behrmann; Agnès Cougnard; Alexandre David; Emmanuel Fleury; Kim Guldstrand Larsen; Didier Lime (CAV, 2007)

On Modal Refinement and Consistency. - Kim Guldstrand Larsen; Ulrik Nyman; Andrzej Wasowski (CONCUR, 2007)

Modal I/O Automata for Interface and Product Line Theories. - Kim Guldstrand Larsen; Ulrik Nyman; Andrzej Wasowski (ESOP, 2007)

Automatic Abstraction Refinement for Timed Automata. - Henning Dierks; Sebastian Kupferschmid; Kim Guldstrand Larsen (FORMATS, 2007)

Guided Controller Synthesis for Climate Controller Using Uppaal Tiga. - Jan Jakob Jessen; Jacob Illum Rasmussen; Kim Guldstrand Larsen; Alexandre David (FORMATS, 2007)

Model-Checking One-Clock Priced Timed Automata. - Patricia Bouyer; Kim Guldstrand Larsen; Nicolas Markey (FoSSaCS, 2007)

Complexity in Simplicity: Flexible Agent-Based State Space Exploration. - Jacob Illum Rasmussen; Gerd Behrmann; Kim Guldstrand Larsen (TACAS, 2007)

Modeling software product lines using color-blind transition systems. - Kim Guldstrand Larsen; Ulrik Nyman; Andrzej Wasowski (Int. J. Softw. Tools Technol. Transf., 2007)

A Game-Theoretic Approach to Real-Time System Testing. - Alexandre David; Kim Guldstrand Larsen; Shuhao Li; Brian Nielsen (DATE, 2008)

Infinite Runs in Weighted Timed Automata with Energy Constraints. - Patricia Bouyer; Ulrich Fahrenberg; Kim Guldstrand Larsen; Nicolas Markey; Jirí Srba (FORMATS, 2008)

Testing Real-Time Systems Using UPPAAL. - Anders Hessel; Kim Guldstrand Larsen; Marius Mikucionis; Brian Nielsen; Paul Pettersson; Arne Skou (Formal Methods and Testing, 2008)

Complexity of Decision Problems for Mixed and Modal Specifications. - Adam Antonik; Michael Huth 001; Kim Guldstrand Larsen; Ulrik Nyman; Andrzej Wasowski (FoSSaCS, 2008)

Model-based schedulability analysis of safety critical hard real-time Java programs. - Thomas Bøgholm; Henrik Kragh-Hansen; Petur Olsen; Bent Thomsen; Kim Guldstrand Larsen (JTRES, 2008)

Fast Directed Model Checking Via Russian Doll Abstraction. - Sebastian Kupferschmid; Jörg Hoffmann 001; Kim Guldstrand Larsen (TACAS, 2008)

20 Years of Modal and Mixed Specifications. - Adam Antonik; Michael Huth 001; Kim G. Larsen; Ulrik Nyman; Andrzej Wasowski (Bull. EATCS, 2008)

EXPTIME-complete Decision Problems for Modal and Mixed Specifications. - Adam Antonik; Michael Huth 001; Kim Guldstrand Larsen; Ulrik Nyman; Andrzej Wasowski (EXPRESS, 2008)

Cooperative Testing of Timed Systems. - Alexandre David; Kim Guldstrand Larsen; Shuhao Li; Brian Nielsen (MBT@ETAPS, 2008)

Optimal infinite scheduling for multi-priced timed automata. - Patricia Bouyer; Ed Brinksma; Kim Guldstrand Larsen (Formal Methods Syst. Des., 2008)

Optimal reachability for multi-priced timed automata. - Kim Guldstrand Larsen; Jacob Illum Rasmussen (Theor. Comput. Sci., 2008)

Playing Games with Timed Games. - Thomas Chatain; Alexandre David; Kim G. Larsen (ADHS, 2009)

Compositional and Quantitative Model Checking (Extended Abstract). - Kim G. Larsen (Ershov Memorial Conference, 2009)

Model-Based GUI Testing Using Uppaal at Novo Nordisk. - Ulrik H. Hjort; Jacob Illum Rasmussen; Kim Guldstrand Larsen; Michael A. Petersen; Arne Skou (FM, 2009)

Verifying Real-Time Systems against Scenario-Based Requirements. - Kim Guldstrand Larsen; Shuhao Li; Brian Nielsen; Saulius Pusinskas (FM, 2009)

Methodologies for Specification of Real-Time Systems Using Timed I/O Automata. - Alexandre David; Kim G. Larsen; Axel Legay; Ulrik Nyman; Andrzej Wasowski (FMCO, 2009)

Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation. - Peter E. Bulychev; Thomas Chatain; Alexandre David; Kim Guldstrand Larsen (FORMATS, 2009)

Verification, Performance Analysis and Controller Synthesis for Real-Time Systems. - Uli Fahrenberg; Kim G. Larsen; Claus R. Thrane (FSEN, 2009)

Priced Timed Automata: Theory and Tools. - Kim G. Larsen (FSTTCS, 2009)

Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study. - Franck Cassez; Jan Jakob Jessen; Kim Guldstrand Larsen; Jean-François Raskin; Pierre-Alain Reynier (HSCC, 2009)

Timed Testing under Partial Observability. - Alexandre David; Kim Guldstrand Larsen; Shuhao Li; Brian Nielsen (ICST, 2009)

Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete. - Nikola Benes; Jan Kretínský; Kim Guldstrand Larsen; Jirí Srba (ICTAC, 2009)

A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic. - Kim G. Larsen; Uli Fahrenberg; Claus R. Thrane (MEMICS, 2009)

Verification and Performance Analysis for Embedded Systems. - Kim Guldstrand Larsen (TASE, 2009)

Teaching Concurrency: Theory in Practice. - Luca Aceto; Anna Ingólfsdóttir; Kim Guldstrand Larsen; Jirí Srba (TFM, 2009)

Discount-Optimal Infinite Runs in Priced Timed Automata. - Ulrich Fahrenberg; Kim Guldstrand Larsen (INFINITY, 2009)

Discounting in Time. - Ulrich Fahrenberg; Kim Guldstrand Larsen (QAPL, 2009)

On determinism in modal transition systems. - Nikola Benes; Jan Kretínský; Kim Guldstrand Larsen; Jirí Srba (Theor. Comput. Sci., 2009)

ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems. - Alexandre David; Kim Guldstrand Larsen; Axel Legay; Ulrik Nyman; Andrzej Wasowski (ATVA, 2010)

10031 Abstracts Collection - Quantitative Models: Expressiveness and Analysis. - Christel Baier; Manfred Droste; Paul Gastin; Kim Guldstrand Larsen (Quantitative Models: Expressiveness and Analysis, 2010)

10031 Executive Summary - Quantitative Models: Expressiveness and Analysis. - Christel Baier; Manfred Droste; Paul Gastin; Kim Guldstrand Larsen (Quantitative Models: Expressiveness and Analysis, 2010)

Scenario-based analysis and synthesis of real-time systems using uppaal. - Kim Guldstrand Larsen; Shuhao Li; Brian Nielsen; Saulius Pusinskas (DATE, 2010)

Quantitative system validation in model driven design. - Holger Hermanns; Kim Guldstrand Larsen; Jean-François Raskin; Jan Tretmans (EMSOFT, 2010)

Application of Model-Checking Technology to Controller Synthesis. - Alexandre David; Jacob Deleuran Grunnet; Jan Jakob Jessen; Kim Guldstrand Larsen; Jacob Illum Rasmussen (FMCO, 2010)

Testing Real-Time Systems under Uncertainty. - Alexandre David; Kim Guldstrand Larsen; Shuhao Li; Marius Mikucionis; Brian Nielsen (FMCO, 2010)

Timed automata with observers under energy constraints. - Patricia Bouyer; Uli Fahrenberg; Kim G. Larsen; Nicolas Markey (HSCC, 2010)

Timed I/O automata: a complete specification theory for real-time systems. - Alexandre David; Kim G. Larsen; Axel Legay; Ulrik Nyman; Andrzej Wasowski (HSCC, 2010)

Quantitative Verification in Practice. - Boudewijn R. Haverkort; Joost-Pieter Katoen; Kim G. Larsen (ISoLA (2), 2010)

Schedulability Analysis Using Uppaal: Herschel-Planck Case Study. - Marius Mikucionis; Kim Guldstrand Larsen; Jacob Illum Rasmussen; Brian Nielsen; Arne Skou; Steen Ulrik Palm; Jan Storbank Pedersen; Poul Hougaard (ISoLA (2), 2010)

Compositional Design Methodology with Constraint Markov Chains. - Benoît Caillaud; Benoît Delahaye; Kim G. Larsen; Axel Legay; Mikkel L. Pedersen; Andrzej Wasowski (QEST, 2010)

Symbolic and Compositional Reachability for Timed Automata. - Kim Guldstrand Larsen (RP, 2010)

New Results on Timed Specifications. - Timothy Bourke; Alexandre David; Kim G. Larsen; Axel Legay; Didier Lime; Ulrik Nyman; Andrzej Wasowski (WADT, 2010)

METAMOC: Modular Execution Time Analysis using Model Checking. - Andreas Engelbredt Dalsgaard; Mads Chr. Olesen; Martin Toft; René Rydhof Hansen; Kim Guldstrand Larsen (WCET, 2010)

On Zone-Based Analysis of Duration Probabilistic Automata - Oded Maler; Kim G. Larsen; Bruce H. Krogh (INFINITY, 2010)

Present and Absent Sets: Abstraction for Testing of Reactive Systems with Databases. - Petur Olsen; Kim G. Larsen; Arne Skou (MBT@ETAPS, 2010)

Scenario-based verification of real-time systems using Uppaal. - Shuhao Li; Sandie Balaguer; Alexandre David; Kim G. Larsen; Brian Nielsen; Saulius Pusinskas (Formal Methods Syst. Des., 2010)

Quantitative analysis of weighted transition systems. - Claus R. Thrane; Uli Fahrenberg; Kim G. Larsen (J. Log. Algebraic Methods Program., 2010)

Modal and mixed specifications: key decision problems and their complexities. - Adam Antonik; Michael Huth 001; Kim G. Larsen; Ulrik Nyman; Andrzej Wasowski (Math. Struct. Comput. Sci., 2010)

New Results on Abstract Probabilistic Automata. - Benoît Delahaye; Joost-Pieter Katoen; Kim G. Larsen; Axel Legay; Mikkel L. Pedersen; Falak Sher; Andrzej Wasowski (ACSD, 2011)

Parametric Modal Transition Systems. - Nikola Benes; Jan Kretínský; Kim G. Larsen; Mikael H. Møller; Jirí Srba (ATVA, 2011)

Time for Statistical Model Checking of Real-Time Systems. - Alexandre David; Kim G. Larsen; Axel Legay; Marius Mikucionis; Zheng Wang 005 (CAV, 2011)

Timed Automata Can Always Be Made Implementable. - Patricia Bouyer; Kim G. Larsen; Nicolas Markey; Ocan Sankur; Claus R. Thrane (CONCUR, 2011)

Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas. - Luca Cardelli; Kim G. Larsen; Radu Mardare (CSL, 2011)

A Modal Specification Theory for Components with Data. - Sebastian S. Bauer; Kim Guldstrand Larsen; Axel Legay; Ulrik Nyman; Andrzej Wasowski (FACS, 2011)

Statistical Model Checking for Networks of Priced Timed Automata. - Alexandre David; Kim G. Larsen; Axel Legay; Marius Mikucionis; Danny Bøgsted Poulsen; Jonas van Vliet; Zheng Wang 005 (FORMATS, 2011)

Robust Specification of Real Time Components. - Kim G. Larsen; Axel Legay; Louis-Marie Traonouez; Andrzej Wasowski (FORMATS, 2011)

Modular Markovian Logic. - Luca Cardelli; Kim G. Larsen; Radu Mardare (ICALP (2), 2011)

Energy Games in Multiweighted Automata. - Uli Fahrenberg; Line Juhl; Kim G. Larsen; Jirí Srba (ICTAC, 2011)

Decision Problems for Interval Markov Chains. - Benoît Delahaye; Kim G. Larsen; Axel Legay; Mikkel L. Pedersen; Andrzej Wasowski (LATA, 2011)

Quantitative Refinement for Weighted Modal Transition Systems. - Sebastian S. Bauer; Uli Fahrenberg; Line Juhl; Kim G. Larsen; Axel Legay; Claus R. Thrane (MFCS, 2011)

opaal: A Lattice Model Checker. - Andreas Engelbredt Dalsgaard; René Rydhof Hansen; Kenneth Yrke Jørgensen; Kim Guldstrand Larsen; Mads Chr. Olesen; Petur Olsen; Jirí Srba (NASA Formal Methods, 2011)

Monitoring Dynamical Signals While Testing Timed Aspects of a System. - Goran Frehse; Kim G. Larsen; Marius Mikucionis; Brian Nielsen (ICTSS, 2011)

APAC: A Tool for Reasoning about Abstract Probabilistic Automata. - Benoît Delahaye; Kim G. Larsen; Axel Legay; Mikkel L. Pedersen; Andrzej Wasowski (QEST, 2011)

Learning Probabilistic Automata for Model Checking. - Hua Mao; Yingke Chen; Manfred Jaeger; Thomas D. Nielsen; Kim G. Larsen; Brian Nielsen (QEST, 2011)

Adaptable Value-Set Analysis for Low-Level Code. - Jörg Brauer; René Rydhof Hansen; Stefan Kowalewski; Kim G. Larsen; Mads Chr. Olesen (SSV, 2011)

Abstract Probabilistic Automata. - Benoît Delahaye; Joost-Pieter Katoen; Kim G. Larsen; Axel Legay; Mikkel L. Pedersen; Falak Sher; Andrzej Wasowski (VMCAI, 2011)

Quantitative analysis of real-time systems using priced timed automata. - Patricia Bouyer; Uli Fahrenberg; Kim G. Larsen; Nicolas Markey (Commun. ACM, 2011)

Stochastic Semantics and Statistical Model Checking for Networks of Priced Timed Automata - Alexandre David; Kim G. Larsen; Axel Legay; Marius Mikucionis; Danny Bøgsted Poulsen; Jonas van Vliet; Zheng Wang 005 (CoRR, 2011)

Distances for Weighted Transition Systems: Games and Properties - Uli Fahrenberg; Claus R. Thrane; Kim G. Larsen (QAPL, 2011)

Distributed Parametric and Statistical Model Checking - Peter E. Bulychev; Alexandre David; Kim Guldstrand Larsen; Marius Mikucionis; Axel Legay (PDMC, 2011)

Developing UPPAAL over 15 years. - Gerd Behrmann; Alexandre David; Kim Guldstrand Larsen; Paul Pettersson; Wang Yi 001 (Softw. Pract. Exp., 2011)

Constraint Markov Chains. - Benoît Caillaud; Benoît Delahaye; Kim G. Larsen; Axel Legay; Mikkel L. Pedersen; Andrzej Wasowski (Theor. Comput. Sci., 2011)

Metrics for weighted transition systems: Axiomatization and complexity. - Kim G. Larsen; Uli Fahrenberg; Claus R. Thrane (Theor. Comput. Sci., 2011)

Model-Based Verification and Analysis for Real-Time Systems. - Uli Fahrenberg; Kim G. Larsen; Claus R. Thrane (Software and Systems Safety - Specification and Verification, 2011)

Controllers with Minimal Observation Power (Application to Timed Systems). - Peter E. Bulychev; Franck Cassez; Alexandre David; Kim Guldstrand Larsen; Jean-François Raskin; Pierre-Alain Reynier (ATVA, 2012)

State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems. - Marius Bozga; Alexandre David; Arnd Hartmanns; Holger Hermanns; Kim G. Larsen; Axel Legay; Jan Tretmans (DATE, 2012)

Code-level timing analysis of embedded software: emsoft'12 invited talk session outline. - Heiko Falk; Kevin Hammond; Kim G. Larsen; Björn Lisper; Stefan M. Petters (EMSOFT, 2012)

Moving from Specifications to Contracts in Component-Based Design. - Sebastian S. Bauer; Alexandre David; Rolf Hennicker; Kim Guldstrand Larsen; Axel Legay; Ulrik Nyman; Andrzej Wasowski (FASE, 2012)

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example. - Hengjun Zhao; Naijun Zhan; Deepak Kapur; Kim G. Larsen (FM, 2012)

Multi-core Reachability for Timed Automata. - Andreas Engelbredt Dalsgaard; Alfons Laarman; Kim G. Larsen; Mads Chr. Olesen; Jaco van de Pol (FORMATS, 2012)

Statistical Model Checking, Refinement Checking, Optimization, ... for Stochastic Hybrid Systems. - Kim G. Larsen (FORMATS, 2012)

Schedulability of Herschel-Planck Revisited Using Statistical Model Checking. - Alexandre David; Kim Guldstrand Larsen; Axel Legay; Marius Mikucionis (ISoLA (2), 2012)

Runtime Verification of Biological Systems. - Alexandre David; Kim Guldstrand Larsen; Axel Legay; Marius Mikucionis; Danny Bøgsted Poulsen; Sean Sedwards (ISoLA (1), 2012)

Quantitative Modelling and Analysis. - Joost-Pieter Katoen; Kim Guldstrand Larsen (ISoLA (2), 2012)

Schedulability Analysis Abstractions for Safety Critical Java. - Thomas Bøgholm; Bent Thomsen; Kim G. Larsen; Alan Mycroft (ISORC, 2012)

Nash Equilibria in Concurrent Priced Games. - Miroslav Klimos; Kim G. Larsen; Filip Stefanak; Jeppe Thaarup (LATA, 2012)

Dual-Priced Modal Transition Systems with Time Durations. - Nikola Benes; Jan Kretínský; Kim Guldstrand Larsen; Mikael H. Møller; Jirí Srba (LPAR, 2012)

Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. - Peter E. Bulychev; Alexandre David; Kim Guldstrand Larsen; Axel Legay; Guangyuan Li; Danny Bøgsted Poulsen; Amélie Stainer (LPAR, 2012)

Action Investment Energy Games. - Kim G. Larsen; Simon Laursen; Jirí Srba (MEMICS, 2012)

Taking It to the Limit: Approximate Reasoning for Markov Processes. - Kim Guldstrand Larsen; Radu Mardare; Prakash Panangaden (MFCS, 2012)

Checking and Distributing Statistical Model Checking. - Peter E. Bulychev; Alexandre David; Kim Guldstrand Larsen; Axel Legay; Marius Mikucionis; Danny Bøgsted Poulsen (NASA Formal Methods, 2012)

Learning Markov Models for Stationary System Behaviors. - Yingke Chen; Hua Mao; Manfred Jaeger; Thomas Dyhre Nielsen; Kim Guldstrand Larsen; Brian Nielsen (NASA Formal Methods, 2012)

Lower-Bound Constrained Runs in Weighted Timed Automata. - Patricia Bouyer; Kim Guldstrand Larsen; Nicolas Markey (QEST, 2012)

Rewrite-Based Statistical Model Checking of WMTL. - Peter E. Bulychev; Alexandre David; Kim G. Larsen; Axel Legay; Guangyuan Li; Danny Bøgsted Poulsen (RV, 2012)

A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata. - Sebastian S. Bauer; Line Juhl; Kim G. Larsen; Jirí Srba; Axel Legay (TASE, 2012)

Quantitative Modal Transition Systems. - Kim G. Larsen; Axel Legay (WADT, 2012)

An evaluation framework for energy aware buildings using statistical model checking. - Alexandre David; Dehui Du; Kim G. Larsen; Marius Mikucionis; Arne Skou (Sci. China Inf. Sci., 2012)

Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach - Peter E. Bulychev; Alexandre David; Kim G. Larsen; Axel Legay; Marius Mikucionis (IWIGP, 2012)

MDM: A Mode Diagram Modeling Framework for Periodic Control Systems - Zheng Wang 005; Geguang Pu; Shengchao Qin; Jianwen Li; Kim G. Larsen; Jan Madsen; Bin Gu 006; Jifeng He 001 (CoRR, 2012)

UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata - Peter E. Bulychev; Alexandre David; Kim Guldstrand Larsen; Marius Mikucionis; Danny Bøgsted Poulsen; Axel Legay; Zheng Wang 005 (QAPL, 2012)

On the Relationship between LTL Normal Forms and Buechi Automata - Jianwen Li; Geguang Pu; Lijun Zhang 001; Zheng Wang 005; Jifeng He 001; Kim G. Larsen (CoRR, 2012)

Statistical Model Checking for Stochastic Hybrid Systems - Alexandre David; Dehui Du; Kim G. Larsen; Axel Legay; Marius Mikucionis; Danny Bøgsted Poulsen; Sean Sedwards (HSB, 2012)

Continuous Markovian Logics - Axiomatization and Quantified Metatheory - Radu Mardare; Luca Cardelli; Kim G. Larsen (Log. Methods Comput. Sci., 2012)

Time-Darts: A Data Structure for Verification of Closed Timed Automata - Kenneth Yrke Jørgensen; Kim G. Larsen; Jirí Srba (SSV, 2012)

Parameterized Metatheory for Continuous Markovian Logic - Kim G. Larsen; Radu Mardare; Claus R. Thrane (QFM, 2012)

Learning Markov Decision Processes for Model Checking - Hua Mao; Yingke Chen; Manfred Jaeger; Thomas D. Nielsen; Kim G. Larsen; Brian Nielsen (QFM, 2012)

MDM: A Mode Diagram Modeling Framework - Zheng Wang 005; Geguang Pu; Jianwen Li; Jifeng He 001; Shengchao Qin; Kim G. Larsen; Jan Madsen; Bin Gu 006 (FTSCS, 2012)

EXPTIME-completeness of thorough refinement on modal transition systems. - Nikola Benes; Jan Kretínský; Kim G. Larsen; Jirí Srba (Inf. Comput., 2012)

Consistency and refinement for Interval Markov Chains. - Benoît Delahaye; Kim G. Larsen; Axel Legay; Mikkel L. Pedersen; Andrzej Wasowski (J. Log. Algebraic Methods Program., 2012)

Modal transition systems with weight intervals. - Line Juhl; Kim G. Larsen; Jirí Srba (J. Log. Algebraic Methods Program., 2012)

Reachability analysis for timed automata using max-plus algebra. - Qi Lu; Michael Madsen; Martin Milata; Søren Ravn; Uli Fahrenberg; Kim G. Larsen (J. Log. Algebraic Methods Program., 2012)

Extending modal transition systems with structured labels. - Sebastian S. Bauer; Line Juhl; Kim G. Larsen; Axel Legay; Jirí Srba (Math. Struct. Comput. Sci., 2012)

New results for Constraint Markov Chains. - Benoît Delahaye; Kim G. Larsen; Axel Legay; Mikkel L. Pedersen; Andrzej Wasowski (Perform. Evaluation, 2012)

Compositional verification of real-time systems using Ecdar. - Alexandre David; Kim Guldstrand Larsen; Axel Legay; Mikael H. Møller; Ulrik Nyman; Anders P. Ravn; Arne Skou; Andrzej Wasowski (Int. J. Softw. Tools Technol. Transf., 2012)

Tools for Model-Checking Timed Systems. - Alexandre David; Gerd Behrmann; Peter E. Bulychev; Joakim Byg; Thomas Chatain; Kim G. Larsen; Paul Pettersson; Jacob Illum Rasmussen; Jirí Srba; Wang Yi 001; Kenneth Yrke Jørgensen; Didier Lime; et al. (Communicating Embedded Systems, 2013)

Optimal Bounds for Multiweighted and Parametrised Energy Games. - Line Juhl; Kim Guldstrand Larsen; Jean-François Raskin (Theories of Programming and Formal Methods, 2013)

On the Relationship between LTL Normal Forms and Büchi Automata. - Jianwen Li; Geguang Pu; Lijun Zhang 001; Zheng Wang 005; Jifeng He 001; Kim Guldstrand Larsen (Theories of Programming and Formal Methods, 2013)

Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction. - Alfons Laarman; Mads Chr. Olesen; Andreas Engelbredt Dalsgaard; Kim Guldstrand Larsen; Jaco van de Pol (CAV, 2013)

Hierarchical Scheduling Framework Based on Compositional Analysis Using Uppaal. - Abdeldjalil Boudjadar; Alexandre David; Jin Hyun Kim; Kim Guldstrand Larsen; Marius Mikucionis; Ulrik Nyman; Arne Skou (FACS, 2013)

Probabilistic Modal Specifications (Invited Extended Abstract). - Kim G. Larsen; Axel Legay (FACS, 2013)

Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems. - Uli Fahrenberg; Kim G. Larsen; Axel Legay (ICTAC Training School on Software Engineering, 2013)

Priced Timed Automata and Statistical Model Checking. - Kim Guldstrand Larsen (IFM, 2013)

TetaSARTS: a tool for modular timing analysis of safety critical Java systems. - Kasper Søe Luckow; Thomas Bøgholm; Bent Thomsen; Kim Guldstrand Larsen (JTRES, 2013)

Stuttering for Abstract Probabilistic Automata. - Benoît Delahaye; Kim G. Larsen; Axel Legay (LFCS, 2013)

Stone Duality for Markov Processes. - Dexter Kozen; Kim G. Larsen; Radu Mardare; Prakash Panangaden (LICS, 2013)

Computing Behavioral Distances, Compositionally. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Radu Mardare (MFCS, 2013)

Optimizing Control Strategy Using Statistical Model Checking. - Alexandre David; Dehui Du; Kim Guldstrand Larsen; Axel Legay; Marius Mikucionis (NASA Formal Methods, 2013)

Remote Testing of Timed Specifications. - Alexandre David; Kim G. Larsen; Marius Mikucionis; Omer Nguena-Timo; Antoine Rollet (ICTSS, 2013)

The BisimDist Library: Efficient Computation of Bisimilarity Distances for Markovian Models. - Giorgio Bacci; Giovanni Bacci 001; Kim Guldstrand Larsen; Radu Mardare (QEST, 2013)

Refinement and Difference for Probabilistic Automata. - Benoît Delahaye; Uli Fahrenberg; Kim Guldstrand Larsen; Axel Legay (QEST, 2013)

Local Model Checking of Weighted CTL with Upper-Bound Constraints. - Jonas Finnemann Jensen; Kim Guldstrand Larsen; Jirí Srba; Lars Kaerlund Oestergaard (SPIN, 2013)

On-the-Fly Exact Computation of Bisimilarity Distances. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Radu Mardare (TACAS, 2013)

Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata. - Alexandre David; Kim G. Larsen; Axel Legay; Danny Bøgsted Poulsen (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Weighted modal transition systems. - Sebastian S. Bauer; Uli Fahrenberg; Line Juhl; Kim G. Larsen; Axel Legay; Claus R. Thrane (Formal Methods Syst. Des., 2013)

Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems. - Uli Fahrenberg; Kim G. Larsen; Axel Legay; Claus R. Thrane (Engineering Dependable Software Systems, 2013)

Quantified Dynamic Metric Temporal Logic for Dynamic Networks of Stochastic Hybrid Automata. - Alexandre David; Kim G. Larsen; Axel Legay; Guangyuan Li; Danny Bøgsted Poulsen (ACSD, 2014)

On Time with Minimal Expected Cost! - Alexandre David; Peter Gjøl Jensen; Kim Guldstrand Larsen; Axel Legay; Didier Lime; Mathias Grund Sørensen; Jakob Haahr Taankvist (ATVA, 2014)

Bisimulation on Markov Processes over Arbitrary Measurable Spaces. - Giorgio Bacci; Giovanni Bacci 001; Kim Guldstrand Larsen; Radu Mardare (Horizons of the Mind, 2014)

Synchronizing Strategies under Partial Observability. - Kim Guldstrand Larsen; Simon Laursen; Jirí Srba (CONCUR, 2014)

Model Checking Process Algebra of Communicating Resources for Real-Time Systems. - Abdeldjalil Boudjadar; Jin Hyun Kim; Kim G. Larsen; Ulrik Nyman (ECRTS, 2014)

Decidability and Expressiveness of Recursive Weighted Logic. - Kim Guldstrand Larsen; Radu Mardare; Bingtian Xue (Ershov Memorial Conference, 2014)

Parametric and Quantitative Extensions of Modal Transition Systems. - Uli Fahrenberg; Kim Guldstrand Larsen; Axel Legay; Louis-Marie Traonouez (FPS@ETAPS, 2014)

Widening the Schedulability of Hierarchical Scheduling Systems. - Abdeldjalil Boudjadar; Alexandre David; Jin Hyun Kim; Kim Guldstrand Larsen; Marius Mikucionis; Ulrik Nyman; Arne Skou (FACS, 2014)

Verification and Performance Evaluation of Timed Game Strategies. - Alexandre David; Huixing Fang; Kim Guldstrand Larsen; Zhengkui Zhang (FORMATS, 2014)

Synchronizing Words for Weighted and Timed Automata. - Laurent Doyen 001; Line Juhl; Kim Guldstrand Larsen; Nicolas Markey; Mahsa Shirmohammadi (FSTTCS, 2014)

Compositional Schedulability Analysis of An Avionics System Using UPPAAL. - Abdeldjalil Boudjadar; Jin Hyun Kim; Kim Guldstrand Larsen; Ulrik Nyman (ICAASE, 2014)

A Decidable Recursive Logic for Weighted Transition Systems. - Kim Guldstrand Larsen; Radu Mardare; Bingtian Xue (ICTAC, 2014)

Statistical Model Checking Past, Present, and Future - (Track Introduction). - Kim Guldstrand Larsen; Axel Legay (ISoLA (2), 2014)

Battery-Aware Scheduling of Mixed Criticality Systems. - Erik Ramsgaard Wognsen; René Rydhof Hansen; Kim Guldstrand Larsen (ISoLA (2), 2014)

Memory Efficient Data Structures for Explicit Verification of Timed Systems. - Peter Gjøl Jensen; Kim Guldstrand Larsen; Jirí Srba; Mathias Grund Sørensen; Jakob Haahr Taankvist (NASA Formal Methods, 2014)

Verification and Performance Analysis of Embedded and Cyber-Physical Systems using UPPAAL. - Kim G. Larsen (PECCS, 2014)

Continuity Properties of Distances for Markov Processes. - Manfred Jaeger; Hua Mao; Kim Guldstrand Larsen; Radu Mardare (QEST, 2014)

Degree of Schedulability of Mixed-Criticality Real-Time Systems with Probabilistic Sporadic Tasks. - Abdeldjalil Boudjadar; Alexandre David; Jin Hyun Kim; Kim G. Larsen; Marius Mikucionis; Ulrik Nyman; Arne Skou (TASE, 2014)

Efficient controller synthesis for a fragment of MTL0,∞. - Peter E. Bulychev; Alexandre David; Kim G. Larsen; Guangyuan Li (Acta Informatica, 2014)

Topologies of Stochastic Markov Models: Computational Aspects. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Radu Mardare (CoRR, 2014)

Adequacy and Complete Axiomatization for Timed Modal Logic. - Samy Jaziri; Kim Guldstrand Larsen; Radu Mardare; Bingtian Xue (MFPS, 2014)

Formal verification and simulation for platform screen doors and collision avoidance in subway control systems. - Huixing Fang; Jianqi Shi; Huibiao Zhu; Jian Guo 005; Kim Guldstrand Larsen; Alexandre David (Int. J. Softw. Tools Technol. Transf., 2014)

Robust synthesis for real-time systems. - Kim G. Larsen; Axel Legay; Louis-Marie Traonouez; Andrzej Wasowski (Theor. Comput. Sci., 2014)

Complete proof systems for weighted modal logic. - Kim G. Larsen; Radu Mardare (Theor. Comput. Sci., 2014)

Safe and Optimal Adaptive Cruise Control. - Kim Guldstrand Larsen; Marius Mikucionis; Jakob Haahr Taankvist (Correct System Design, 2015)

Quantitative Schedulability Analysis of Continuous Probability Tasks in a Hierarchical Context. - Jin Hyun Kim; Abdeldjalil Boudjadar; Ulrik Nyman; Marius Mikucionis; Kim G. Larsen; Arne Skou; Insup Lee 001; Linh Thi Xuan Phan (CBSE, 2015)

Modelling Social-Technical Attacks with Timed Automata. - Nicolas David 002; Alexandre David; René Rydhof Hansen; Kim Guldstrand Larsen; Axel Legay; Mads Chr. Olesen; Christian W. Probst (MIST@CCS, 2015)

Polynomial Time Decidability of Weighted Synchronization under Partial Observability. - Jan Kretínský; Kim Guldstrand Larsen; Simon Laursen; Jirí Srba (CONCUR, 2015)

A Cost/Reward Method for Optimal Infinite Scheduling in Mobile Cloud Computing. - Luca Aceto; Kim G. Larsen; Andrea Morichetta 001; Francesco Tiezzi 001 (FACS, 2015)

Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools. - Jin Hyun Kim; Kim G. Larsen; Brian Nielsen; Marius Mikucionis; Petur Olsen (FMICS, 2015)

A Score Function for Optimizing the Cycle-Life of Battery-Powered Embedded Systems. - Erik Ramsgaard Wognsen; Boudewijn R. Haverkort; Marijn R. Jongerden; René Rydhof Hansen; Kim Guldstrand Larsen (FORMATS, 2015)

On the Total Variation Distance of Semi-Markov Chains. - Giorgio Bacci; Giovanni Bacci 001; Kim Guldstrand Larsen; Radu Mardare (FoSSaCS, 2015)

Compositional Metric Reasoning with Probabilistic Process Calculi. - Daniel Gebler; Kim Guldstrand Larsen; Simone Tini (FoSSaCS, 2015)

Resource-Parameterized Timing Analysis of Real-Time Systems. - Jin Hyun Kim; Axel Legay; Kim Guldstrand Larsen; Marius Mikucionis; Brian Nielsen (Haifa Verification Conference, 2015)

Language Emptiness of Continuous-Time Parametric Timed Automata. - Nikola Benes; Peter Bezdek; Kim Guldstrand Larsen; Jirí Srba (ICALP (2), 2015)

CAAL: Concurrency Workbench, Aalborg Edition. - Jesper Rank Andersen; Nicklas Andersen; Søren Enevoldsen; Mathias M. Hansen; Kim G. Larsen; Simon R. Olesen; Jirí Srba; Jacob K. Wortmann (ICTAC, 2015)

Converging from Branching to Linear Metrics on Markov Chains. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Radu Mardare (ICTAC, 2015)

Formal Methods for Modelling and Analysis of Single-Event Upsets. - René Rydhof Hansen; Kim Guldstrand Larsen; Mads Chr. Olesen; Erik Ramsgaard Wognsen (IRI, 2015)

Flexible Framework for Statistical Schedulability Analysis of Probabilistic Sporadic Tasks. - Abdeldjalil Boudjadar; Jin Hyun Kim; Alexandre David; Kim G. Larsen; Marius Mikucionis; Ulrik Nyman; Arne Skou; Insup Lee 001; Linh Thi Xuan Phan (ISORC, 2015)

Model checking of finite-state machine-based scenario-aware dataflow using timed automata. - Mladen Skelin; Erik Ramsgaard Wognsen; Mads Chr. Olesen; René Rydhof Hansen; Kim Guldstrand Larsen (SIES, 2015)

Parametric Verification of Weighted Systems. - Peter Christoffersen; Mikkel Hansen; Anders Mariegaard; Julian Trier Ringsmose; Kim Guldstrand Larsen; Radu Mardare (SynCoP, 2015)

Uppaal Stratego. - Alexandre David; Peter Gjøl Jensen; Kim Guldstrand Larsen; Marius Mikucionis; Jakob Haahr Taankvist (TACAS, 2015)

Refinement checking on parametric modal transition systems. - Nikola Benes; Jan Kretínský; Kim G. Larsen; Mikael H. Møller; Salomon Sickert; Jirí Srba (Acta Informatica, 2015)

Average-energy games (full version). - Patricia Bouyer; Nicolas Markey; Mickael Randour; Kim G. Larsen; Simon Laursen (CoRR, 2015)

The EATCS Award 2016 - Call for Nominations. - Kim Guldstrand Larsen (Bull. EATCS, 2015)

Alternation-Free Weighted Mu-Calculus: Decidability and Completeness. - Kim G. Larsen; Radu Mardare; Bingtian Xue (MFPS, 2015)

Concurrent weighted logic. - Kim G. Larsen; Radu Mardare; Bingtian Xue (J. Log. Algebraic Methods Program., 2015)

A reconfigurable framework for compositional schedulability and power analysis of hierarchical scheduling systems with frequency scaling. - Abdeldjalil Boudjadar; Alexandre David; Jin Hyun Kim; Kim G. Larsen; Marius Mikucionis; Ulrik Nyman; Arne Skou (Sci. Comput. Program., 2015)

Schedulability of Herschel revisited using statistical model checking. - Alexandre David; Kim Guldstrand Larsen; Axel Legay; Marius Mikucionis (Int. J. Softw. Tools Technol. Transf., 2015)

Uppaal SMC tutorial. - Alexandre David; Kim G. Larsen; Axel Legay; Marius Mikucionis; Danny Bøgsted Poulsen (Int. J. Softw. Tools Technol. Transf., 2015)

Statistical model checking for biological systems. - Alexandre David; Kim G. Larsen; Axel Legay; Marius Mikucionis; Danny Bøgsted Poulsen; Sean Sedwards (Int. J. Softw. Tools Technol. Transf., 2015)

Real-time specifications. - Alexandre David; Kim G. Larsen; Axel Legay; Ulrik Nyman; Louis-Marie Traonouez; Andrzej Wasowski (Int. J. Softw. Tools Technol. Transf., 2015)

An Automata-Based Approach to Trace Partitioned Abstract Interpretation. - Mads Christian Olesen; René Rydhof Hansen; Kim Guldstrand Larsen (Semantics, Logics, and Calculi, 2016)

Complete Axiomatization for the Bisimilarity Distance on Markov Chains. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Radu Mardare (CONCUR, 2016)

Energy-aware scheduling of FIR filter structures using a timed automata model. - Erik Ramsgaard Wognsen; René Rydhof Hansen; Kim Guldstrand Larsen; Peter Koch 001 (DDECS, 2016)

A Model-Based Framework for the Specification and Analysis of Hierarchical Scheduling Systems. - Mounir Chadli; Jin Hyun Kim; Axel Legay; Louis-Marie Traonouez; Stefan Naujokat; Bernhard Steffen; Kim Guldstrand Larsen (FMICS-AVoCS, 2016)

Modelling Attack-defense Trees Using Timed Automata. - Olga Gadyatskaya; René Rydhof Hansen; Kim Guldstrand Larsen; Axel Legay; Mads Chr. Olesen; Danny Bøgsted Poulsen (FORMATS, 2016)

Distributed Algorithms for Time Optimal Reachability Analysis. - Zhengkui Zhang; Brian Nielsen; Kim G. Larsen (FORMATS, 2016)

Probabilistic Mu-Calculus: Decidability and Complete Axiomatization. - Kim G. Larsen; Radu Mardare; Bingtian Xue (FSTTCS, 2016)

Toolchain for user-centered intelligent floor heating control. - Mads Kronborg Agesen; Kim Guldstrand Larsen; Marius Mikucionis; Marco Muñiz; Petur Olsen; Thomas Pedersen; Jirí Srba; Arne Skou (IECON, 2016)

Statistical Model Checking: Past, Present, and Future. - Kim G. Larsen; Axel Legay (ISoLA (1), 2016)

On the Power of Statistical Model Checking. - Kim G. Larsen; Axel Legay (ISoLA (2), 2016)

WNetKAT: A Weighted SDN Programming and Verification Language. - Kim G. Larsen; Stefan Schmid 001; Bingtian Xue (OPODIS, 2016)

Time optimal reachability analysis using swarm verification. - Zhengkui Zhang; Brian Nielsen; Kim G. Larsen (SAC, 2016)

Distributed Computation of Fixed Points on Dependency Graphs. - Andreas Engelbredt Dalsgaard; Søren Enevoldsen; Kim Guldstrand Larsen; Jirí Srba (SETTA, 2016)

A Complete Approximation Theory for Weighted Transition Systems. - Mikkel Hansen; Kim Guldstrand Larsen; Radu Mardare; Mathias Ruggaard Pedersen; Bingtian Xue (SETTA, 2016)

Importance Sampling for Stochastic Timed Automata. - Cyrille Jégourel; Kim G. Larsen; Axel Legay; Marius Mikucionis; Danny Bøgsted Poulsen; Sean Sedwards (SETTA, 2016)

Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization. - Peter Gjøl Jensen; Kim Guldstrand Larsen; Jirí Srba (SPIN, 2016)

Online and Compositional Learning of Controllers with Application to Floor Heating. - Kim G. Larsen; Marius Mikucionis; Marco Muñiz; Jirí Srba; Jakob Haahr Taankvist (TACAS, 2016)

Automatic Verification, Performance Analysis, Synthesis and Optimization of Timed Systems. - Kim Guldstrand Larsen (TIME, 2016)

Weighted Branching Simulation Distance for Parametric Weighted Kripke Structures. - Louise Foshammer; Kim Guldstrand Larsen; Anders Mariegaard (Cassting/SynCoP, 2016)

Compositional bisimulation metric reasoning with Probabilistic Process Calculi. - Daniel Gebler; Kim G. Larsen; Simone Tini (Log. Methods Comput. Sci., 2016)

Limit Your Consumption! Finding Bounds in Average-energy Games. - Kim G. Larsen; Simon Laursen; Martin Zimmermann 002 (QAPL, 2016)

Formal modelling and analysis of Bitflips in ARM assembly code. - René Rydhof Hansen; Kim Guldstrand Larsen; Mads Chr. Olesen; Erik Ramsgaard Wognsen (Inf. Syst. Frontiers, 2016)

Learning deterministic probabilistic automata from a model checking perspective. - Hua Mao; Yingke Chen; Manfred Jaeger; Thomas D. Nielsen; Kim G. Larsen; Brian Nielsen (Mach. Learn., 2016)

Statistical and exact schedulability analysis of hierarchical scheduling systems. - Abdeldjalil Boudjadar; Alexandre David; Jin Hyun Kim; Kim G. Larsen; Marius Mikucionis; Ulrik Nyman; Arne Skou (Sci. Comput. Program., 2016)

Optimizing the resource requirements of hierarchical scheduling systems. - Jin Hyun Kim; Axel Legay; Louis-Marie Traonouez; Abdeldjalil Boudjadar; Ulrik Nyman; Kim G. Larsen; Insup Lee 001; Jin-Young Choi (SIGBED Rev., 2016)

Efficient model-checking of weighted CTL with upper-bound constraints. - Jonas Finnemann Jensen; Kim Guldstrand Larsen; Jirí Srba; Lars Kaerlund Oestergaard (Int. J. Softw. Tools Technol. Transf., 2016)

Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation. - Andreas Engelbredt Dalsgaard; Søren Enevoldsen; Peter Fogh; Lasse S. Jensen; Tobias Skovgaard Jepsen; Isabella Kaufmann; Kim G. Larsen; Søren M. Nielsen; Mads Chr. Olesen; Samuel Pastva; Jirí Srba (Petri Nets, 2017)

Compositional Testing of Real-Time Systems. - Kim G. Larsen; Axel Legay; Marius Mikucionis; Brian Nielsen; Ulrik Nyman (ModelEd, TestEd, TrustEd, 2017)

Quantitative Evaluation of Attack Defense Trees Using Stochastic Timed Automata. - René Rydhof Hansen; Peter Gjøl Jensen; Kim Guldstrand Larsen; Axel Legay; Danny Bøgsted Poulsen (GraMSec@CSF, 2017)

Symbolic Dependency Graphs for $$ text {PCTL}^{>}_{ le }$$ Model-Checking. - Anders Mariegaard; Kim Guldstrand Larsen (FORMATS, 2017)

On the Metric-Based Approximate Minimization of Markov Chains. - Giovanni Bacci 001; Giorgio Bacci; Kim G. Larsen; Radu Mardare (ICALP, 2017)

Integrating Tools: Co-simulation in UPPAAL Using FMI-FMU. - Peter Gjøl Jensen; Kim Guldstrand Larsen; Axel Legay; Ulrik Nyman (ICECCS, 2017)

Pareto Optimal Reachability Analysis for Simple Priced Timed Automata. - Zhengkui Zhang; Brian Nielsen; Kim Guldstrand Larsen; Gilles Nies; Marvin Stenger; Holger Hermanns (ICFEM, 2017)

Mutation-Based Test-Case Generation with Ecdar. - Kim G. Larsen; Florian Lorber; Brian Nielsen; Ulrik Nyman (ICST Workshops, 2017)

PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing. - Peter Gjøl Jensen; Kim Guldstrand Larsen; Jirí Srba (ICTAC, 2017)

Formal validation of supervisory energy management systems for microgrids. - Gayathri Sugumar; Rajasekar Selvamuthukumaran; Tomislav Dragicevic; Ulrik Nyman; Kim G. Larsen; Frede Blaabjerg (IECON, 2017)

Unrestricted stone duality for Markov processes. - Robert Furber; Dexter Kozen; Kim G. Larsen; Radu Mardare; Prakash Panangaden (LICS, 2017)

Refinement of Trace Abstraction for Real-Time Programs. - Franck Cassez; Peter Gjøl Jensen; Kim Guldstrand Larsen (RP, 2017)

Dependable and Optimal Cyber-Physical Systems. - Kim Guldstrand Larsen (SOFSEM, 2017)

Practical controller synthesis for MTL0, ∞. - Guangyuan Li; Peter Gjøl Jensen; Kim Guldstrand Larsen; Axel Legay; Danny Bøgsted Poulsen (SPIN, 2017)

Validation, Synthesis and Optimization for Cyber-Physical Systems. - Kim Guldstrand Larsen (TACAS (1), 2017)

Memory-Efficient Tactics for Randomized LTL Model Checking. - Kim G. Larsen; Doron Peled; Sean Sedwards (VSTTE, 2017)

Timed and Untimed Energy Games. - Kim Guldstrand Larsen (CIAA, 2017)

Reasoning About Bounds in Weighted Transition Systems. - Mikkel Hansen; Kim Guldstrand Larsen; Radu Mardare; Mathias Ruggaard Pedersen; Bingtian Xue (CoRR, 2017)

On-the-Fly Computation of Bisimilarity Distances. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Radu Mardare (Log. Methods Comput. Sci., 2017)

From Timed Automata to Stochastic Hybrid Games Model Checking, Synthesis, Performance Analysis and Machine Learning. - Kim G. Larsen; Uli Fahrenberg; Axel Legay (Dependable Software Systems Engineering, 2017)

Analyzing Spreadsheets for Parallel Execution via Model Checking. - Thomas Bøgholm; Kim G. Larsen; Marco Muñiz; Bent Thomsen; Lone Leth Thomsen (Models, Mindsets, Meta, 2018)

Models, Mindsets, Meta: The What, the How, and the Why Not? - Tiziana Margaria; Susanne Graf; Kim G. Larsen (Models, Mindsets, Meta, 2018)

Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. - Frederik M. Bønneland; Peter Gjøl Jensen; Kim Guldstrand Larsen; Marco Muñiz; Jirí Srba (CAV (1), 2018)

Time Optimal Robust Fleet Management of Micro UAV Through Timed Games Formulation. - Henrik Schiøler; Luminita Totu; Jan Dimon Bendtsen; Kim Guldstrand Larsen; Jakob Haahr Taankvist (CCTA, 2018)

Guaranteed Control Synthesis for Continuous Systems in Uppaal Tiga. - Kim Guldstrand Larsen; Adrien Le Coënt; Marius Mikucionis; Jakob Haahr Taankvist (CyPhy/WESE, 2018)

Optimal and Robust Controller Synthesis - Using Energy Timed Automata with Uncertainty. - Giovanni Bacci 001; Patricia Bouyer; Uli Fahrenberg; Kim Guldstrand Larsen; Nicolas Markey; Pierre-Alain Reynier (FM, 2018)

20 Years of Real Real Time Model Validation. - Kim Guldstrand Larsen; Florian Lorber; Brian Nielsen (FM, 2018)

Weighted Branching Systems: Behavioural Equivalence, Behavioural Distance, and Their Logical Characterisations. - Mathias Claus Jensen; Kim Guldstrand Larsen; Radu Mardare (FORMATS, 2018)

Model-Based Mutation Testing of Real-Time Systems via Model Checking. - Florian Lorber; Kim G. Larsen; Brian Nielsen (ICST Workshops, 2018)

Statistical Model Checking the 2018 Edition! - Kim Guldstrand Larsen; Axel Legay (ISoLA (2), 2018)

20 Years of UPPAAL Enabled Industrial Model-Based Validation and Beyond. - Kim G. Larsen; Florian Lorber; Brian Nielsen (ISoLA (4), 2018)

Generic Formal Framework for Compositional Analysis of Hierarchical Scheduling Systems. - Jalil Boudjadar; Jin Hyun Kim; Linh Thi Xuan Phan; Insup Lee 001; Kim G. Larsen; Ulrik Nyman (ISORC, 2018)

Timed Comparisons of Semi-Markov Processes. - Mathias Ruggaard Pedersen; Nathanaël Fijalkow; Giorgio Bacci; Kim G. Larsen; Radu Mardare (LATA, 2018)

Energiautomater, energifunktioner og Kleene-algebra. - Uli Fahrenberg; Kim G. Larsen (NIK, 2018)

On the Verification of Weighted Kripke Structures Under Uncertainty. - Giovanni Bacci 001; Mikkel Hansen; Kim Guldstrand Larsen (QEST, 2018)

Analytical Solution for Long Battery Lifetime Prediction in Nonadaptive Systems. - Dmitry Ivanov; Kim G. Larsen; Sibylle Schupp; Jirí Srba (QEST, 2018)

A Hemimetric Extension of Simulation for Semi-Markov Decision Processes. - Mathias Ruggaard Pedersen; Giorgio Bacci; Kim Guldstrand Larsen; Radu Mardare (QEST, 2018)

Average-energy games. - Patricia Bouyer; Nicolas Markey; Mickael Randour; Kim G. Larsen; Simon Laursen (Acta Informatica, 2018)

Learning Timed Automata via Genetic Programming. - Martin Tappler; Bernhard K. Aichernig; Kim Guldstrand Larsen; Florian Lorber (CoRR, 2018)

Parameter Synthesis Problems for one parametric clock Timed Automata. - Liyun Dai; Taolue Chen 001; Zhiming Liu 001; Bican Xia; Naijun Zhan; Kim G. Larsen (CoRR, 2018)

Complete Axiomatization for the Total Variation Distance of Markov Chains. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Radu Mardare (MFPS, 2018)

Contracts for System Design. - Albert Benveniste; Benoît Caillaud; Dejan Nickovic; Roberto Passerone; Jean-Baptiste Raclet; Philipp Reinkemeier; Alberto L. Sangiovanni-Vincentelli; Werner Damm; Thomas A. Henzinger; Kim G. Larsen (Found. Trends Electron. Des. Autom., 2018)

A Distributed Fixed-Point Algorithm for Extended Dependency Graphs. - Andreas Engelbredt Dalsgaard; Søren Enevoldsen; Peter Fogh; Lasse S. Jensen; Peter Gjøl Jensen; Tobias Skovgaard Jepsen; Isabella Kaufmann; Kim G. Larsen; Søren M. Nielsen; Mads Chr. Olesen; Samuel Pastva; Jirí Srba (Fundam. Informaticae, 2018)

A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Radu Mardare (Log. Methods Comput. Sci., 2018)

Reasoning About Bounds in Weighted Transition Systems. - Mikkel Hansen; Kim Guldstrand Larsen; Radu Mardare; Mathias Ruggaard Pedersen (Log. Methods Comput. Sci., 2018)

Preface: Dedicated to the memory of Zoltán Ésik (1951-2016). - Manfred Droste; Kim G. Larsen (Soft Comput., 2018)

On decidability of recursive weighted logics. - Kim G. Larsen; Radu Mardare; Bingtian Xue (Soft Comput., 2018)

High-level frameworks for the specification and verification of scheduling problems. - Mounir Chadli; Jin Hyun Kim; Kim G. Larsen; Axel Legay; Stefan Naujokat; Bernhard Steffen; Louis-Marie Traonouez (Int. J. Softw. Tools Technol. Transf., 2018)

Discrete and continuous strategies for timed-arc Petri net games. - Peter Gjøl Jensen; Kim Guldstrand Larsen; Jirí Srba (Int. J. Softw. Tools Technol. Transf., 2018)

Reachability problems: Special issue. - Kim G. Larsen; Igor Potapov; Jirí Srba (Theor. Comput. Sci., 2018)

Model Checking Real-Time Systems. - Patricia Bouyer; Uli Fahrenberg; Kim Guldstrand Larsen; Nicolas Markey; Joël Ouaknine; James Worrell 001 (Handbook of Model Checking, 2018)

Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs. - Manfred Jaeger; Peter Gjøl Jensen; Kim Guldstrand Larsen; Axel Legay; Sean Sedwards; Jakob Haahr Taankvist (ATVA, 2019)

Computing Probabilistic Bisimilarity Distances for Probabilistic Automata. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Radu Mardare; Qiyi Tang 001; Franck van Breugel (CONCUR, 2019)

Partial Order Reduction for Reachability Games. - Frederik M. Bønneland; Peter Gjøl Jensen; Kim G. Larsen; Marco Muñiz; Jirí Srba (CONCUR, 2019)

Synthesis of Safe, Optimal and Compact Strategies for Stochastic Hybrid Games (Invited Paper). - Kim G. Larsen (CONCUR, 2019)

L*-Based Learning of Markov Decision Processes. - Martin Tappler; Bernhard K. Aichernig; Giovanni Bacci 001; Maria Eichlseder; Kim G. Larsen (FM, 2019)

Time to Learn - Learning Timed Automata from Tests. - Martin Tappler; Bernhard K. Aichernig; Kim Guldstrand Larsen; Florian Lorber (FORMATS, 2019)

Symbolic Model Checking of Weighted PCTL Using Dependency Graphs. - Mathias Claus Jensen; Anders Mariegaard; Kim Guldstrand Larsen (NFM, 2019)

Model Checking Constrained Markov Reward Models with Uncertainties. - Giovanni Bacci 001; Mikkel Hansen; Kim Guldstrand Larsen (QEST, 2019)

SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes. - Pranav Ashok; Jan Kretínský; Kim Guldstrand Larsen; Adrien Le Coënt; Jakob Haahr Taankvist; Maximilian Weininger (QEST, 2019)

Safe and Time-Optimal Control for Railway Games. - Shyam Lal Karra; Kim Guldstrand Larsen; Florian Lorber; Jirí Srba (RSSRail, 2019)

Model Verification Through Dependency Graphs. - Søren Enevoldsen; Kim Guldstrand Larsen; Jirí Srba (SPIN, 2019)

Abstract Dependency Graphs and Their Application to Model Checking. - Søren Enevoldsen; Kim Guldstrand Larsen; Jirí Srba (TACAS (1), 2019)

A Faster-Than Relation for Semi-Markov Decision Processes. - Mathias Ruggaard Pedersen; Giorgio Bacci; Kim G. Larsen (QAPL@ETAPS, 2019)

L*-Based Learning of Markov Decision Processes (Extended Version). - Martin Tappler; Bernhard K. Aichernig; Giovanni Bacci 001; Maria Eichlseder; Kim G. Larsen (CoRR, 2019)

Selected papers from the 28th Nordic Workshop on Programming Theory (NWPT'16). - Kim G. Larsen; Jirí Srba (J. Log. Algebraic Methods Program., 2019)

Model checking and synthesis for branching multi-weighted logics. - Lasse S. Jensen; Isabella Kaufmann; Kim G. Larsen; Søren M. Nielsen; Jirí Srba (J. Log. Algebraic Methods Program., 2019)

Continuous-Time Models for System Design and Analysis. - Rajeev Alur; Mirco Giacobbe; Thomas A. Henzinger; Kim G. Larsen; Marius Mikucionis (Computing and Software Science, 2019)

On-the-Fly Synthesis for Strictly Alternating Games. - Shyam Lal Karra; Kim Guldstrand Larsen; Marco Muñiz; Jirí Srba (Petri Nets, 2020)

Synthesis for Multi-weighted Games with Branching-Time Winning Conditions. - Isabella Kaufmann; Kim Guldstrand Larsen; Jirí Srba (Petri Nets, 2020)

Urgent Partial Order Reduction for Extended Timed Automata. - Kim G. Larsen; Marius Mikucionis; Marco Muñiz; Jirí Srba (ATVA, 2020)

Approximating Euclidean by Imprecise Markov Decision Processes. - Manfred Jaeger; Giorgio Bacci; Giovanni Bacci 001; Kim Guldstrand Larsen; Peter Gjøl Jensen (ISoLA (1), 2020)

Fluid Model-Checking in UPPAAL for Covid-19. - Peter Gjøl Jensen; Kenneth Yrke Jørgensen; Kim G. Larsen; Marius Mikucionis; Marco Muñiz; Danny Bøgsted Poulsen (ISoLA (1), 2020)

30 Years of Statistical Model Checking. - Kim G. Larsen; Axel Legay (ISoLA (1), 2020)

Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs. - Søren Enevoldsen; Mathias Claus Jensen; Kim Guldstrand Larsen; Anders Mariegaard; Jirí Srba (LOPSTR, 2020)

From Statistical Model Checking to Run-Time Monitoring Using a Bayesian Network Approach. - Manfred Jaeger; Kim G. Larsen; Alessandro Tibo (RV, 2020)

Randomized Refinement Checking of Timed I/O Automata. - Andrej Kiviriga; Kim Guldstrand Larsen; Ulrik Nyman (SETTA, 2020)

A complete axiomatization of weighted branching bisimulation. - Mathias Claus Jensen; Kim Guldstrand Larsen (Acta Informatica, 2020)

A general framework for defining and optimizing robustness. - Alessandro Tibo; Manfred Jaeger; Kim G. Larsen (CoRR, 2020)

It's Time to Play Safe: Shield Synthesis for Timed Systems. - Roderick Bloem; Peter Gjøl Jensen; Bettina Könighofer; Kim Guldstrand Larsen; Florian Lorber; Alexander Palmisano (CoRR, 2020)

Mixed Nondeterministic-Probabilistic Interfaces. - Albert Benveniste; Kim G. Larsen; Jean-Baptiste Raclet (CoRR, 2020)

Dependency graphs with applications to verification. - Søren Enevoldsen; Kim G. Larsen; Anders Mariegaard; Jirí Srba (Int. J. Softw. Tools Technol. Transf., 2020)

Learning Safe and Optimal Control Strategies for Storm Water Detention Ponds. - Martijn A. Goorden; Kim G. Larsen; Jesper E. Nielsen; Thomas D. Nielsen; Michael R. Rasmussen; Jirí Srba (ADHS, 2021)

A Bayesian Framework for Large-Scale Identification of Nonlinear Hybrid Systems. - Ahmad Madary; Hamid Reza Momeni; Alessandro Abate; Kim G. Larsen (ADHS, 2021)

Quantitative Analysis of Interval Markov Chains. - Giovanni Bacci 001; Benoît Delahaye; Kim G. Larsen; Anders Mariegaard (Model Checking, Synthesis, and Learning, 2021)

Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems. - Andrej Kiviriga; Kim Guldstrand Larsen; Ulrik Nyman (FMICS, 2021)

Stubborn Set Reduction for Timed Reachability and Safety Games. - Frederik M. Bønneland; Peter Gjøl Jensen; Kim G. Larsen; Marco Muñiz; Jirí Srba (FORMATS, 2021)

An Integer Static Analysis for Better Extrapolation in Uppaal. - Sebastian Lund; Jesper van Diepen; Kim G. Larsen; Marco Muñiz; Tobias Ringholm Jørgensen; Tobias Skaarup Daa Andersen (FORMATS, 2021)

Active Learning of Markov Decision Processes using Baum-Welch algorithm. - Giovanni Bacci 001; Anna Ingólfsdóttir; Kim G. Larsen; Raphaël Reynouard (ICMLA, 2021)

A Model-Checking Static Analysis of Task-Based Energy Neutrality for Energy Harvesting IoT. - Michele Albano; Stefano Chessa; Kim Guldstrand Larsen (ISCC, 2021)

Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods. - Giorgio Bacci; Giovanni Bacci 001; Kim G. Larsen; Mirco Tribastone; Max Tschaikowski; Andrea Vandin (LICS, 2021)

Battery Aware Analysis of Sensor Networks in Uppaal SMC. - Muhammad Naeem 011; Michele Albano; Kim G. Larsen; Brian Nielsen; Anders Høedholt; Christian Ø. Laursen (MECO, 2021)

Preliminary Security Analysis, Formalisation, and Verification of OpenTitan Secure Boot Code. - Bjarke Hilmer Møller; Jacob Gosch Søndergaard; Kristoffer Skagbæk Jensen; Magnus Winkel Pedersen; Tobias Worm Bøgedal; Anton Christensen; Danny Bøgsted Poulsen; Kim Guldstrand Larsen; René Rydhof Hansen; Thomas Rosted Jensen; Heino Juvoll Madsen; Henrik Uhrenfeldt (NordSec, 2021)

Lumpability for Uncertain Continuous-Time Markov Chains. - Luca Cardelli; Radu Grosu; Kim G. Larsen; Mirco Tribastone; Max Tschaikowski; Andrea Vandin (QEST, 2021)

Active Learning of Markov Decision Processes using Baum-Welch algorithm (Extended). - Giovanni Bacci 001; Anna Ingólfsdóttir; Kim G. Larsen; Raphaël Reynouard (CoRR, 2021)

L*-based learning of Markov decision processes (extended version). - Martin Tappler; Bernhard K. Aichernig; Giovanni Bacci 001; Maria Eichlseder; Kim G. Larsen (Formal Aspects Comput., 2021)

2018 CAV award. - Kim G. Larsen; Natarajan Shankar; Pierre Wolper; Somesh Jha (Formal Methods Syst. Des., 2021)

Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction. - Franck Cassez; Peter Gjøl Jensen; Kim Guldstrand Larsen (Fundam. Informaticae, 2021)

Stubborn Set Reduction for Two-Player Reachability Games. - Frederik Meyer Bønneland; Peter Gjøl Jensen; Kim Guldstrand Larsen; Marco Muñiz; Jirí Srba (Log. Methods Comput. Sci., 2021)

Preface to the Special Issue on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2017). - Kim G. Larsen; Oleg Sokolsky; Ji Wang 001 (Sci. Comput. Program., 2021)

ADTLang: a programming language approach to attack defense trees. - René Rydhof Hansen; Kim Guldstrand Larsen; Axel Legay; Peter Gjøl Jensen; Danny Bøgsted Poulsen (Int. J. Softw. Tools Technol. Transf., 2021)

Distributed Fleet Management in Noisy Environments via Model-Predictive Control. - Simon Bøgh; Peter Gjøl Jensen; Martin Kristjansen; Kim Guldstrand Larsen; Ulrik Nyman (ICAPS, 2022)

STOMPC: Stochastic Model-Predictive Control with Uppaal Stratego. - Martijn A. Goorden; Peter Gjøl Jensen; Kim G. Larsen; Mihhail Samusev; Jirí Srba; Guohan Zhao (ATVA, 2022)

Convex Lattice Equation Systems. - Giorgio Bacci; Giovanni Bacci 001; Mathias Claus Jensen; Kim G. Larsen (Principles of Systems Design, 2022)

Playing Wordle with Uppaal Stratego. - Peter Gjøl Jensen; Kim G. Larsen; Marius Mikucionis (A Journey from Process Algebra via Timed Automata to Model Learning, 2022)

Simulation Relations and Applications in Formal Methods. - Kim G. Larsen; Christian Schilling 001; Jirí Srba (Principles of Systems Design, 2022)

Monitoring Timed Properties (Revisited). - Thomas Møller Grosen; Sean Kauffman; Kim Guldstrand Larsen; Martin Zimmermann 002 (FORMATS, 2022)

Importance Splitting in Uppaal. - Kim Guldstrand Larsen; Axel Legay; Marius Mikucionis; Danny Bøgsted Poulsen (ISoLA (3), 2022)

Formal Methods Meet Machine Learning (F3ML). - Kim G. Larsen; Axel Legay; Gerrit Nolte; Maximilian Schlüter; Mariëlle Stoelinga; Bernhard Steffen (ISoLA (3), 2022)

Automata Learning Meets Shielding. - Martin Tappler; Stefan Pranger; Bettina Könighofer; Edi Muskardin; Roderick Bloem; Kim G. Larsen (ISoLA (1), 2022)

Balancing Flexible Production and Consumption of Energy using Resource Timed Automata. - Jonas Hansen; Kim Guldstrand Larsen; Pieter J. L. Cuijpers (MECO, 2022)

Monte Carlo Tree Search for Priced Timed Automata. - Peter Gjøl Jensen; Andrej Kiviriga; Kim Guldstrand Larsen; Ulrik Nyman; Adriana Mijacika; Jeppe Høiriis Mortensen (QEST, 2022)

Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals. - Shiraj Arora; René Rydhof Hansen; Kim Guldstrand Larsen; Axel Legay; Danny Bøgsted Poulsen (SPIN, 2022)

End-to-End Heat-Pump Control Using Continuous Time Stochastic Modelling and Uppaal Stratego. - Imran Riaz Hasrat; Peter Gjøl Jensen; Kim Guldstrand Larsen; Jirí Srba (TASE, 2022)

AllSynth: Transiently Correct Network Update Synthesis Accounting for Operator Preferences. - Kim Guldstrand Larsen; Anders Mariegaard; Stefan Schmid 001; Jirí Srba (TASE, 2022)

A Sigfox Module for the Network Simulator 3. - Muhammad Naeem 011; Michele Albano; Davide Magrin; Brian Nielsen; Kim Guldstrand Larsen (WNS3, 2022)

Hierarchical identification of nonlinear hybrid systems in a Bayesian framework. - Ahmad Madary; Hamid Reza Momeni; Alessandro Abate; Kim G. Larsen (Inf. Comput., 2022)

Formal methods and tools for industrial critical systems. - Maurice H. ter Beek; Kim G. Larsen; Dejan Nickovic; Tim A. C. Willemse (Int. J. Softw. Tools Technol. Transf., 2022)

Extended abstract dependency graphs. - Søren Enevoldsen; Kim Guldstrand Larsen; Jirí Srba (Int. J. Softw. Tools Technol. Transf., 2022)

Assume-Guarantee Reasoning for Additive Hybrid Behaviour. - Pieter J. L. Cuijpers; Jonas Hansen; Kim G. Larsen (Theories of Programming and Formal Methods, 2023)

Guaranteed safe controller synthesis for switched systems using analytical solutions*. - Martijn A. Goorden; Kim G. Larsen; Jesper E. Nielsen; Thomas D. Nielsen; Weizhu Qian; Michael R. Rasmussen; Guohan Zhao (CCTA, 2023)

Comparative Analysis of Uppaal SMC, ns-3 and MATLAB/Simulink. - Muhammad Naeem 011; Michele Albano; Kim Guldstrand Larsen; Brian Nielsen (ECBS, 2023)

A Modeling Concept for Formal Verification of OS-Based Compositional Software. - Leandro Batista Ribeiro; Florian Lorber; Ulrik Nyman; Kim Guldstrand Larsen; Marcel Baunach (FASE, 2023)

Modelling of Hot Water Buffer Tank and Mixing Loop for an Intelligent Heat Pump Control. - Imran Riaz Hasrat; Peter Gjøl Jensen; Kim Guldstrand Larsen; Jirí Srba (FMICS, 2023)

Refinement of Systems with an Attacker Focus. - Kim Guldstrand Larsen; Axel Legay; Danny Bøgsted Poulsen (FMICS, 2023)

Usage-and Risk-Aware Falsification Testing for Cyber-Physical Systems. - Andrej Kiviriga; Kim Guldstrand Larsen; Dejan Nickovic; Ulrik Nyman (FORMATS, 2023)

Dynamic Extrapolation in Extended Timed Automata. - Nicolaj Ø. Jensen; Peter Gjøl Jensen; Kim G. Larsen (ICFEM, 2023)

Dual Balancing of SoC/SoT in Smart Batteries Using Reinforcement Learning in Uppaal Stratego. - Martin Kristjansen; Abhijit Kulkarni; Peter Gjøl Jensen; Remus Teodorescu; Kim Guldstrand Larsen (IECON, 2023)

Learning Symbolic Timed Models from Concrete Timed Data. - Simon Dierl; Falk Maria Howar; Sean Kauffman; Martin Kristjansen; Kim Guldstrand Larsen; Florian Lorber; Malte Mauritz (NFM, 2023)

Safety Verification of Decision-Tree Policies in Continuous Time. - Christian Schilling 001; Anna Lukina; Emir Demirovic; Kim Guldstrand Larsen (NeurIPS, 2023)

An MM Algorithm to Estimate Parameters in Continuous-Time Markov Chains. - Giovanni Bacci 001; Anna Ingólfsdóttir; Kim G. Larsen; Raphaël Reynouard (QEST, 2023)

Elimination of Detached Regions in Dependency Graph Verification. - Peter Gjøl Jensen; Kim Guldstrand Larsen; Jirí Srba; Nikolaj Jensen Ulrik (SPIN, 2023)

Shielded Reinforcement Learning for Hybrid Systems. - Asger Horn Brorholt; Peter Gjøl Jensen; Kim Guldstrand Larsen; Florian Lorber; Christian Schilling 001 (AISoLA, 2023)

Welcome Remarks from AISoLA 2023/Track C2 Chairs. - Nils Jansen 001; Bettina Könighofer; Jan Kretínský; Kim G. Larsen (AISoLA, 2023)

Timed I/O Automata: It is never too late to complete your timed specification theory. - Martijn A. Goorden; Kim G. Larsen; Axel Legay; Florian Lorber; Ulrik Nyman; Andrzej Wasowski (CoRR, 2023)

MM Algorithms to Estimate Parameters in Continuous-time Markov Chains. - Giovanni Bacci 001; Anna Ingólfsdóttir; Kim G. Larsen; Raphaël Reynouard (CoRR, 2023)

Energy Consumption Optimization in Radio Access Networks (ECO-RAN). - Anders Mariegaard; Kim G. Larsen; Marco Muñiz; Thomas Dyhre Nielsen (CoRR, 2023)

Efficient Simulation of Quantum Circuits by Model Order Reduction. - Antonio Jiménez-Pastor; Kim G. Larsen; Mirco Tribastone; Max Tschaikowski (CoRR, 2023)

CGAAL: Distributed On-The-Fly ATL Model Checker with Heuristics. - Falke B. Ø. Carlsen; Lars Bo P. Frydenskov; Nicolaj Ø. Jensen; Jener Rasmussen; Mathias M. Sørensen; Asger G. Weirsøe; Mathias Claus Jensen; Kim G. Larsen (GandALF, 2023)

A toolchain for domestic heat-pump control using Uppaal Stratego. - Imran Riaz Hasrat; Peter Gjøl Jensen; Kim Guldstrand Larsen; Jirí Srba (Sci. Comput. Program., 2023)

AllSynth: A BDD-based approach for network update synthesis. - Kim G. Larsen; Anders Mariegaard; Stefan Schmid 001; Jirí Srba (Sci. Comput. Program., 2023)

Algorithmic Minimization of Uncertain Continuous-Time Markov Chains. - Luca Cardelli; Radu Grosu; Kim Guldstrand Larsen; Mirco Tribastone; Max Tschaikowski; Andrea Vandin (IEEE Trans. Autom. Control., 2023)

GPU Accelerating Statistical Model Checking for Extended Timed Automata. - Oliver S. Bak; Mathias W. B. Christiansen; Oliver V. Eriksen; Sergio Feo-Arenis; Peter Gjøl Jensen; Marcus D. Jensen; Simas Juozapaitis; Kim G. Larsen; Marius Mikucionis; Marco Muñiz; Andreas Windfeld (Principles of Verification (2), 2024)

SyRep: Efficient Synthesis and Repair of Fast Re-Route Forwarding Tables for Resilient Networks. - Csaba Györgyi; Kim G. Larsen; Stefan Schmid 001; Jirí Srba (DSN, 2024)

Compositional Control Synthesis for Water Management System. - Esther H. Kim; Kim G. Larsen; Martijn A. Goorden; Thomas D. Nielsen (ECC, 2024)

Optimal Infinite Temporal Planning: Cyclic Plans for Priced Timed Automata. - Rasmus G. Tollund; Nicklas S. Johansen; Kristian Ø. Nielsen; Álvaro Torralba; Kim G. Larsen (ICAPS, 2024)

Monitoring Real-Time Systems Under Parametric Delay. - Martin Fränzle; Thomas Møller Grosen; Kim G. Larsen; Martin Zimmermann 002 (IFM, 2024)

SyPer: Synthesis of Perfectly Resilient Local Fast Re-Routing Rules for Highly Dependable Networks. - Csaba Györgyi; Kim G. Larsen; Stefan Schmid 001; Jirí Srba (INFOCOM, 2024)

CommonUppRoad: A Framework of Formal Modelling, Verifying, Learning, and Visualisation of Autonomous Vehicles. - Rong Gu 002; Kaige Tan; Andreas Holck Høeg-Petersen; Lei Feng 002; Kim Guldstrand Larsen (ISoLA (3), 2024)

Optimality-Preserving Reduction of Chemical Reaction Networks. - Kim G. Larsen; Daniele Toller; Mirco Tribastone; Max Tschaikowski; Andrea Vandin (ISoLA (2), 2024)

Dissimilarity for Linear Dynamical Systems. - Giorgio Bacci; Giovanni Bacci 001; Kim Guldstrand Larsen; Giuseppe Squillace; Mirco Tribastone; Max Tschaikowski; Andrea Vandin (QEST+FORMATS, 2024)

The Complexity of Data-Free Nfer. - Sean Kauffman; Kim Guldstrand Larsen; Martin Zimmermann 002 (RV, 2024)

Exploiting Assumptions for Effective Monitoring of Real-Time Properties Under Partial Observability. - Alessandro Cimatti; Thomas Møller Grosen; Kim G. Larsen; Stefano Tonetta; Martin Zimmermann 002 (SEFM, 2024)

Forward and Backward Constrained Bisimulations for Quantum Circuits. - Antonio Jiménez-Pastor; Kim G. Larsen; Mirco Tribastone; Max Tschaikowski (TACAS (2), 2024)

Safe and Infinite Resource Scheduling Using Energy Timed Automata. - Pieter J. L. Cuijpers; Jonas Hansen; Kim G. Larsen (TASE, 2024)

Energy-Efficient Motion Planning for Autonomous Vehicles Using Uppaal Stratego. - Muhammad Naeem 011; Rong Gu 002; Cristina Seceleanu; Kim Guldstrand Larsen; Brian Nielsen; Michele Albano (TASE, 2024)

Statistical Analysis of the Impact of Bit-Flips in Security Critical Code. - Tobias Worm Bøgedal; René Rydhof Hansen; Kim Guldstrand Larsen; Axel Legay; Danny Bøgsted Poulsen (AISoLA, 2024)

Efficient Shield Synthesis via State-Space Transformation. - Asger Horn Brorholt; Andreas Holck Høeg-Petersen; Kim Guldstrand Larsen; Christian Schilling 001 (AISoLA, 2024)

Reinforcement Learning for Discretized Euclidean MDPs. - Manfred Jaeger; Kim Guldstrand Larsen (AISoLA, 2024)

Statistical Model Checking the 2024 Edition! - Sudeep Kanav; Jan Kretínský; Kim G. Larsen (AISoLA, 2024)

Digital Twin-Empowered Voltage Control for Power Systems. - Jiachen Xu; Yushuai Li; Torben Bach Pedersen; Yuqiang He; Kim Guldstrand Larsen; Tianyi Li 005 (CoRR, 2024)

Contraction Heuristics for Tensor Decision Diagrams. - Christian Bøgh Larsen; Simon Brun Olsen; Kim Guldstrand Larsen; Christian Schilling 001 (Entropy, 2024)

Controlling stormwater detention ponds under partial observability. - Esther H. Kim; Martijn A. Goorden; Kim G. Larsen; Thomas D. Nielsen (J. Log. Algebraic Methods Program., 2024)

Reproducibility Package for SYPER: Synthesis of Perfectly Resilient Local Fast Re-Routing Rules for Highly Dependable Networks. - Csaba Györgyi; Kim Guldstrand Larsen; Stefan Schmid 001; Jirí Srba (Zenodo, 2024)

Artefact for: "Optimal Infinite Temporal Planning: Cyclic Plans for Priced Timed Automata". - Rasmus G. Tollund; Nicklas S. Johansen; Kristian Ødum Knorborg; Kim Guldstrand Larsen; Álvaro Torralba (Zenodo, 2024)

Uncertainty-Aware Temporal Graph Convolutional Network for Traffic Speed Forecasting. - Weizhu Qian; Thomas Dyhre Nielsen; Yan Zhao 008; Kim Guldstrand Larsen; James Jianqiao Yu (IEEE Trans. Intell. Transp. Syst., 2024)

Statistical Model Checking of Stochastic Timed-Arc Petri Nets. - Tanguy Dubois; Kim G. Larsen; Jirí Srba (Petri Nets, 2025)

Performance Analysis of Stochastic Digraph Real-Time Task Model. - Martin Kristjansen; Kim Guldstrand Larsen (Real Time and Such, 2025)

Time for Timed Monitorability. - Thomas Møller Grosen; Sean Kauffman; Kim G. Larsen; Martin Zimmermann 002 (CONCUR, 2025)

On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions. - Nicolaj Ø. Jensen; Kim G. Larsen; Didier Lime; Jirí Srba (CONCUR, 2025)

Exact Schedulability Analysis for Limited-Preemptive Parallel Applications Using Timed Automata in UPPAAL. - Jonas Hansen; Srinidhi Srinivasan; Geoffrey Nelissen; Kim G. Larsen (DATE, 2025)

Building a Modular Platform for Model Checking Glitch Attacks in RISC-V Programs. - Andreas Kjeldgaard Brandhøj; Tobias Worm Bøgedal; René Rydhof Hansen; Kim Guldstrand Larsen; Danny Bøgsted Poulsen (FMICS, 2025)

Data-Driven Shielding of Online Reinforcement Learning: A Stormwater Pond Case Study. - Esther H. Kim; Martijn A. Goorden; Kim Guldstrand Larsen; Thomas Dyhre Nielsen (FSEN, 2025)

Compositional Shielding and Reinforcement Learning for Multi-Agent Systems. - Asger Horn Brorholt; Kim Guldstrand Larsen; Christian Schilling 001 (AAMAS, 2025)

What Makes You Special? Contrastive Heuristics Based on Qualified Dominance. - Rasmus G. Tollund; Kim G. Larsen; Álvaro Torralba (IJCAI, 2025)

Extended Timed Regular Expressions. - Marco Muñiz; Marius Mikucionis; Kim G. Larsen (RV, 2025)

Token Elimination in Model Checking of Petri Nets. - Nicolaj Ø. Jensen; Kim G. Larsen; Jirí Srba (TACAS (1), 2025)

Kano Model for Enhanced Satisfaction in User-Centric EV Charging and P2P Energy Trading. - Min Zhang 058; Yushuai Li; Tianyi Li 005; Torben Bach Pedersen; Kim Guldstrand Larsen; Christian S. Jensen (VTC2025-Spring, 2025)

Digital Twin for Secure Peer-to-Peer Trading in Cyber-Physical Energy Systems. - Yushuai Li; Peiyuan Guan; Tianyi Li 005; Kim Guldstrand Larsen; Marco Aiello 001; Torben Bach Pedersen; Tingwen Huang; Yan Zhang 002 (IEEE Trans. Netw. Sci. Eng., 2025)

Token Elimination in Model Checking of Petri Nets Reproducibility Package. - Nicolaj Østerby Jensen; Kim Guldstrand Larsen; Jirí Srba (Zenodo, 2025)

Token Elimination in Model Checking of Petri Nets Reproducibility Package. - Nicolaj Østerby Jensen; Kim Guldstrand Larsen; Jirí Srba (Zenodo, 2025)

You May Delay, but Time Will Not: Timed Games Under Delayed Control. - Kim G. Larsen; Martin Zimmermann 002 (CoRR, 2025)

On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions Reproducibility Package. - Nicolaj Østerby Jensen; Kim Guldstrand Larsen; Didier Lime; Jirí Srba (Zenodo, 2025)

On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions Reproducibility Package. - Nicolaj Østerby Jensen; Kim Guldstrand Larsen; Didier Lime; Jirí Srba (Zenodo, 2025)

On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions Reproducibility Package. - Nicolaj Østerby Jensen; Kim Guldstrand Larsen; Didier Lime; Jirí Srba (Zenodo, 2025)

Doing More With Less: A Survey of Data Selection Methods for Mathematical Modeling. - Nicolai A. Weinreich; Arman Oshnoei; Remus Teodorescu; Kim G. Larsen (IEEE Trans. Knowl. Data Eng., 2025)

Dynamic Modeling and Analysis for Electricity-Gas Systems With Electric-Driven Compressors. - Yujia Huang; Qiuye Sun; Zhe Chen 007; David Wenzhong Gao; Torben Bach Pedersen; Kim Guldstrand Larsen; Yushuai Li (IEEE Trans. Smart Grid, 2025)

A Neuro-Symbolic Approach for Probabilistic Reasoning on Graph Data. - Raffaele Pojer; Andrea Passerini; Kim G. Larsen; Manfred Jaeger (CoRR, 2025)

Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems. - Asger Horn Brorholt; Andreas Holck Høeg-Petersen; Peter Gjøl Jensen; Kim Guldstrand Larsen; Marius Mikucionis; Christian Schilling 001; Andrzej Wasowski (CoRR, 2025)