@inproceedings{FMCO09,
 author ={A. David and K.G. Larsen and U. Nyman and A. Legay and A. Wasowski},
 title ={Methodologies for Specification of Real-Time Systems Using Timed I/O Automata},
 booktitle ={Proceedings of FMCO 2009},
 series ={Lecture Notes in Computer Science},
 note ={To appear},
 abstract ={We present a real-time specification framework based on Timed I/O Automata and a comprehensive tool support for it. The framework supports various design methodologies including: top-down refinement—for decomposition of abstract specifications towards increasingly detailed models; bottom-up abstraction for synthesis of complex systems from more concrete models; and step-wise modularisation of requirements to factor out behaviours given by existing available components from a complex global requirements specification to be implemented. These methodologies are realized by consecutive applications of operators from the following set: refinement, consistency checking, log- ical and structural composition and quotienting. Additionally, our tool allows combining the component-oriented design process with verification of temporal logic properties increasing the flexibility of the process.},
}

@article{AntonikHLNW10,
 author ={Adam Antonik and Michael Huth and Kim G. Larsen and Ulrik Nyman and Andrzej Wasowski},
 title ={Modal and mixed specifications: key decision problems and their complexities},
 journal ={Mathematical Structures in Computer Science},
 volume ={20},
 number ={1},
 year ={2010},
 pages ={75-103},
 abstract ={Modal and mixed transition systems are specification formalisms that allow the mixing of over- and under-approximation. We discuss three fundamental decision problems for such specifications: 1) whether a set of specifications has a common implementation; 2) whether an individual specification has an implementation; and 3) whether all implementations of an individual specification are implementations of another one. For each of these decision problems we investigate the worst-case computational complexity for the modal and mixed cases. We show that the first decision problem is EXPTIME-complete for both modal and mixed specifications. We prove that the second decision problem is EXPTIME-complete for mixed specifications (it is known to be trivial for modal ones). The third decision problem is also shown to be EXPTIME-complete for mixed specifications.},
}

@incollection{ESHandbook,
 author ={A. David and J. Illum and K.G. Larsen and A. Skou},
 title ={Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1},
 booktitle ={Model-Based Design for Embedded Systems},
 pages ={93-119},
 publisher ={C. R. C. Press LLC},
 year ={2009},
 editor ={G. Nicolescu and P.J. Mosterman},
 abstract ={Embedded systems involve the monitoring and control of complex physical processes using applications running on dedicated executin platforms in a resource constrained manner in terms of for example memory, processing power, bandwidth, energy consumption, as well as timing behavior. Viewing the application as a collection of (interdependent tasks) various scheduling principles may be applied to coordinate the execuiton of tasks in order to ensure orderly and efficient usage of resources. Based on the physical process to be controlled, timing deadlines may be required for the individual tasks as well as the overall system. The challenge of schedulability analysis is now concerned with guaranteeing that the applied scheduling principle(s) ensure that the timining deadlines are met.},
}

@inproceedings{Infty10,
 author ={O. Maler and K.G. Larsen and B. Krogh},
 title ={On Zone-Based Analysis of Duration Probabilistic Automata},
 booktitle ={Proceedings of INFINITY, International Workshop on Verification of Infinite-State Systems},
 year ={2010},
 abstract ={ We propose an extension of the zone-based algorithmics for analyzing timed automata to handle systems where timing uncertainty is considered as probabilistic rather than set-theoretic. We study duration probabilistic automata (DPA), expressing multiple parallel processes admitting memoryfull continuouslydistributed durations. For this model we develop an extension of the zone-based forward reachability algorithm whose successor operator is a density transformer, thus providing a solution to verification and performance evaluation problems concerning acyclic DPA (or the bounded-horizon behavior of cyclic DPA).},
}

@inproceedings{Terma10,
 author ={M. Mikucionis and K.G. Larsen and B. Nielsen and J. Illum and A. Skou and S.U. Palm and J.S. Pedersen and P. Hougaard},
 title ={Schedulability Analysis Using Uppaal: Herscehl-Planck Case Study},
 booktitle ={Proceedings of 4th International Symposiumo on Leveraging Applications of Formal Methods, Verification and Validation; track: Quantitative Verification in Practice},
 year ={2010},
 series ={Lecture Notes in Computer Science},
 publisher ={Springer},
 abstract ={ We propose a modeling framework for performing schedulability analysis by using Uppaal real-time model-checker. The frame-work is inspired by a case study where schedulability analysis of a satellite system is performed. The framework assumes a single CPU hardware where a fixed priority preemptive scheduler is used in a combination with two resource sharing protocols and in addition voluntary task suspension is considered. The contributions include the modeling framework, its application on an industrial case study and a comparison of results with classical response time analysis. },
}

@inproceedings{DBLP:conf/rp/Larsen10,
 author ={Kim Guldstrand Larsen},
 title ={Symbolic and Compositional Reachability for Timed Automata},
 booktitle ={RP},
 year ={2010},
 pages ={24-28},
 ee ={http://dx.doi.org/10.1007/978-3-642-15349-5_2},
 crossref ={DBLP:conf/rp/2010},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 abstract ={The model-checker UPPAAL is based on the theory of timed automata and its modeling languague offers additional features such as networks of timed automata, clocks and stop-watches, synchronizing over synchronous and broadcast channels, discrete variables ranging over bounded integers or structured types (arrays and records) as well as user-defined types and functions. In the following we give an overview of the development of the datastuctures and algorithms underlying the verification engines of UPPAAL and CORA as well as indicate on-going research directions.},
}

@proceedings{DBLP:conf/rp/2010,
 editor ={Anton\'{\i}n Kucera and Igor Potapov},
 title ={Reachability Problems, 4th International Workshop, RP 2010, Brno, Czech Republic, August 28-29, 2010. Proceedings},
 booktitle ={RP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6227},
 year ={2010},
 isbn ={978-3-642-15348-8},
 ee ={http://dx.doi.org/10.1007/978-3-642-15349-5},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{CAI,
 author ={Uli Fahrenberg and Kim G. Larsen and Claus Thrane},
 title ={A Quantitatve Characterization of Weighted Kripke Structures in Temporal Logic},
 journal ={Journal of Computing and Informatics},
 year ={2010},
 note ={to appear},
 abstract ={We extend the usual notion of Kripke structures with a weighted transition relation and generalize the classical Boolean interpretation of CTL to a map which assigns to states and temporal formulae a real-valued distance describing the degree of satisfaction. We describe a general approach to obtaining quantitative interpretations for a generic extension of the CTL syntax and show that, for one such interpretation, the logic is both adequate and expressive with respect to quantitative bisimulation. },
}

@inproceedings{MEMICS09,
 author ={Uli Fahrenberg and Kim G. Larsen and Claus Thrane},
 title ={A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic},
 booktitle ={Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMIC'09)},
 year ={2009},
 editor ={Petr Hlineny and Vashek Matyas and Tomas Vojnar},
 note ={Best paper award},
}

@inproceedings{MBT10,
 author ={Petur Olsen and Kim G. Larsen and Arne Skou},
 title ={Present and Absent Sets: Abstraction for Testing of Reactive Systems with Databases},
 booktitle ={Proceedings of 6th Workshop on Model-Based Testing},
 year ={2010},
 abstract ={We present a new abstraction of reactive systems interacting with databases. This abstraction is intended to be used for model-based testing. We abstract the database into two sets: present set and absent set, and present a proof of this abstrac- tion. We present two extensions of FSM, the DBFSM and PAFSM. DBFSM are a form of FSM incorporating databases. PAFSM are an abstraction of DBFSM using present-absent sets. Depending on what type of testing is to be done, the translation is tailored to fit this purpose. We show how this translation is related to the present-absent abstraction. Finally, we illustrate the approach through a small example and show how this can be used for testing with the model-based testing tool Uppaal TRON. },
}

@inproceedings{WADT10,
 author ={Alexandre David and Kim G. Larsen and Axel Legay and Ulrik Nyman and Andrzej Wasowski},
 title ={An Interface Theory for Timed Systems},
 booktitle ={Proceedings of 20th International Workshop on Algebraic Development Techniques WADT},
 year ={2010},
 note ={To appear},
 abstract ={We propose to survey our new theory for compositional design and verification of real time systems. In our theory, a component interface describes both the behavior of the component and the component's assumptions about the environment. The theory supports the important operations of a good compositional reasoning theory: composition, conjunction, quotient, consistency/satisfaction checking, and refinement. The operators can be used to combine basic models into larger specifications to construct comprehensive system descriptions from basic requirements. Algorithms to perform these operations have been based on a game theoretical setting that permits, for example, to capture the real-time constraints on communication events between components. The compositional approach allows for scalability in the verification. The theory has been implemented in a tool that will also be presented.},
}

@article{SPE10,
 author ={Gerd Behrmann and Alexandere David and Kim G. Larsen and Paul Pettersson and Wang Yi},
 title ={Developing UPPAAL over 15 Years},
 journal ={Software - Practice and Experience},
 year ={2010},
 note ={To appear},
 abstract ={Uppaal is a tool suitable for model checking real-time systems described as networks of timed automata communicating by channel synchronisations and extended with integer variables. Its first version was released in 1995 and its development is still very active. It now features an advanced modelling language, a user-friendly graphical interface, and a performant model checker engine. In addition, several flavours of the tool have matured in recent years. In this paper, we present how we managed to maintain the tool during 15 years, its current architecture with its challenges, and we give future directions of the tool.},
}

@inproceedings{ATVA10,
 author ={Alexandre David and Kim G. Larsen and Axel Legay and Ulrik Nyman and Andrzej Wasowski},
 title ={ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems},
 booktitle ={Proceedings of 8th International Symposium on Automated Technology for Verification and Analysis (ATVA)},
 year ={2010},
 note ={To appear},
 abstract ={We present Ecdar a new tool for compositional design and verification of real time systems. In Ecdar, a component interface describes both the behavior of the component and the component's assumptions about the environment. The tool supports the important operations of a good compositional reasoning theory: composition, conjunction, quotient, consistency/satisfaction checking, and refinement. The operators can be used to combine basic models into larger specifications to construct comprehensive system descriptions from basic requirements. Algorithms to perform these operations have been based on a game theoretical setting that permits, for example, to capture the real-time constraints on communication events between components. The compositional approach allows for scalability in the verification.},
}

@inproceedings{QEST01,
 author ={Benoit Caillaud and Benoit Delahaye and Kim G. Larsen and Axel Legay and Mikkel Larsen Pedersen and Andrzej Wasowski},
 title ={Compositional Design Methodology with Constraint Markov Chains},
 booktitle ={Proceedings of 7th International Conference on Quantitative Evaluation of SysTems (QEST)},
 year ={2010},
 note ={To appear},
 abstract ={Notions of specification, implementation, satisfaction, and refinement, together with operators supporting stepwise design, constutes a specification theory. We construct such a theory for Markov Chains (MCs) employing a new abstraction of a Constraint MC. Constraint MCs permit rich constraints on probability distributions and thus generalize prior abstractions such as Interval MCs. Linear (polynomial) constraints suffice for closure under conjunction (respectively parallel composition). This is the first specification theory for MCs with such closure properties. We discuss its relation to simpler operators for known languages such as probabilistic process algebra. Despite the generality, all operators and relations are computable. },
}

@inproceedings{WCET10,
 author ={Andreas E. Dalsgaard and Mads Chr. Olesen and Martin Toft and Rene R. Hansen and Kim G. Larsen},
 title ={METAMOC: Modular Execution Tiem Analysis using Model Checking},
 booktitle ={Proceedings of 10th International Workshop on Worst-Case Execution Time Analysis},
 year ={2010},
 note ={To appear.},
 abstract ={Safe and tight worst-case execution times (WCETs) are important when scheduling hard real-time systems. This paper presents METAMOC, a path-based, modular method, based on model checking and stastic analysis, that determines safe and tight WCETs for programs running on platforms featuring caching and pipelining. The method works by constructing a UPPAAL model of the program being analysed and annotating the model with information from an inter-procedural value analysis. The program model is then combined with a model of the hardware platform, and model checked for the WCET. Through support for the platforms ARM7, ARM9 and ATMEL AVR 8-bit the modularity and retargetability of the method is demonstrated, as only the pipeline needs to be remodelled. Modelling the hardware is performed in a state-ofthe- art graphical modeling environment. Experiments on the Malardalen WCET benchmark programs show that taking caching into account yields much a tighter WCETs, and that METAMOC is a fast and versatile approach for WCET analysis.},
}

@inproceedings{DBLP:conf/date/LarsenLNP10,
 author ={Kim Guldstrand Larsen and Shuhao Li and Brian Nielsen and Saulius Pusinskas},
 title ={Scenario-based analysis and synthesis of real-time systems using uppaal},
 booktitle ={DATE: Design, Automation and Test in Europe, DATE 2010, Dresden, Germany, March 8-12},
 year ={2010},
 pages ={447-452},
 ee ={http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5457164},
 publisher ={IEEE},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 abstract ={ We propose an automated, tool-supported approach to scenario-based analysis and synthesis of real-time embedded systems. The inter-object behaviors of a system are modeled as a set of live sequence charts (LSCs), and the scenario-based user requirement is specified as a separate LSC. By translating the set of LSC charts into a behavior-equivalent network of med automata (TA), we reduce the problems of model consistency checking and property verification to classical CTL real-time model checking problems, and reduce the problem of centralized synthesis for open systems to a timed game solving problem. We implement a prototype LSC-to-TA translator, which can be linked to exisisting real-time model checker UPPAAL and timed game solver UPPAALTIGA. Preliminary experiments on a number of examples show that it is a viable approach.},
}

@inproceedings{DBLP:conf/hybrid/BouyerFLM10,
 author ={Patricia Bouyer and Uli Fahrenberg and Kim G. Larsen and Nicolas Markey},
 title ={Timed automata with observers under energy constraints},
 booktitle ={HSCC},
 year ={2010},
 pages ={61-70},
 ee ={http://doi.acm.org/10.1145/1755952.1755963},
 crossref ={DBLP:conf/hybrid/2010},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 abstract ={In this paper, we study one-clock priced timed automata in which prices can grow linearly or exponentially, with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs (or reachability of some goal location) with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero).},
}

@proceedings{DBLP:conf/hybrid/2010,
 editor ={Karl Henrik Johansson and Wang Yi},
 title ={Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010},
 booktitle ={HSCC},
 publisher ={ACM ACM},
 year ={2010},
 isbn ={978-1-60558-955-8},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/hybrid/DavidLLNW10,
 author ={Alexandre David and Kim G. Larsen and Axel Legay and Ulrik Nyman and Andrzej Wasowski},
 title ={Timed I/O automata: a complete specification theory for real-time systems},
 booktitle ={HSCC},
 year ={2010},
 pages ={91-100},
 ee ={http://doi.acm.org/10.1145/1755952.1755967},
 crossref ={DBLP:conf/hybrid/2010},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 abstract ={A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation and a set of operators supporting stepwise design. We develop a complete specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications---all indispensable ingredients of a compositional design methodology. The theory is implemented on top of an engine for timed games, \tiga, and illustrated with a small case study. },
}

@proceedings{DBLP:conf/hybrid/2010,
 editor ={Karl Henrik Johansson and Wang Yi},
 title ={Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010},
 booktitle ={HSCC},
 publisher ={ACM ACM},
 year ={2010},
 isbn ={978-1-60558-955-8},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fm/LarsenLNP09,
 author ={Kim Guldstrand Larsen and Shuhao Li and Brian Nielsen and Saulius Pusinskas},
 title ={Verifying Real-Time Systems against Scenario-Based Requirements},
 booktitle ={FM},
 year ={2009},
 pages ={676-691},
 ee ={http://dx.doi.org/10.1007/978-3-642-05089-3_43},
 crossref ={DBLP:conf/fm/2009},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={LarsenLNP09.pdf},
 abstract ={We propose an approach to automatic verification of realtime systems against scenario-based requirements. A real-time system is modeled as a network of Timed Automata (TA), and a scenario-based requirement is specified as a Live Sequence Chart (LSC). We define a trace-based semantics for a kernel subset of the LSC language. By equivalently translating an LSC chart into an observer TA and then nonintrusively composing this observer with the original system model, the problem of verifying a real-time system against a scenario-based requirement reduces to a classical real-time model checking problem. We show how this is accomplished in the context of the Uppaal model checker.},
}

@proceedings{DBLP:conf/fm/2009,
 editor ={Ana Cavalcanti and Dennis Dams},
 title ={FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings},
 booktitle ={FM},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={5850},
 year ={2009},
 isbn ={978-3-642-05088-6},
 ee ={http://dx.doi.org/10.1007/978-3-642-05089-3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@book{hermes08,
 author ={Gerd Behrmann and B\'eatrice B'erard and Franck Cassez and Thao Dang and Alexandre David and Susanna Donatelli and Jean-Pierre Elloy and Goran Frehse and Antoine Girard and Serge Haddad and Claude Jard and Kim Guldstrand Larsen and Colas Le Guernic and Didier Lime and Morgan Magnin and Nicolas Markey and Paul Pettersson and Jacob Illum Rasmussen and Olivier H. Roux and Stavros Tripakis and Wang Yi},
 title ={Approches formelles des syst\`emes embarqu\'es communicant},
 publisher ={Hermes Lavoisier, s\'erie Informatique et syst\`emes d'information},
 year ={2008},
 isbn ={978-2-7462-1942-7},
 url ={http://www.afsec-cnrs.org/wp-content/uploads/2008/11/afsec.pdf},
}

@book{reactive,
 author ={Luca Aceto and Anna Ingolfsdottir and Kim Guldstrand Larsen and Jiri Srba},
 title ={Reactive Systems:~ Modelling, Specification and Verification},
 publisher ={Cambridge University Press},
 year ={2007},
 isbn ={9780521875462},
}

@inbook{LarsenNielsen:ARTIST,
 author ={Kim Guldstrand Larsen and Brian Nielsen},
 editor ={Hutchison, D., Kanade, T., Kittler, J., Kleinberg, J., Kobsa, A., Mattern, F., Mitchell, J.C., Naor, M., Nierstrasz, O.M., Pandu Rangan, C., Steffen, B., Sudan, M., Terzopoulos, D., Tygar, J.D., Weikum, G.},
 title ={Embedded Systems Design The ARTIST Roadmap for Research and Development Series},
 chapter ={Testing and Verification},
 publisher ={Springer-Verlag},
 year ={2005},
 series ={Lecture Notes in Computer Science},
}

@inbook{HLMNPS:05,
 author ={Anders Hessel and Kim Guldstrand Larsen and Marius Mikucionis and Brian Nielsen and Paul Pettersson and Arne Skou},
 editor ={Jonathan Bowen, Mark Harman, Rob Hierons},
 title ={Formal Methods and Testing},
 chapter ={Automated Model-Based Conformance Testing of Real-Time Systems},
 publisher ={Springer-Verlag},
 year ={2005},
 pages ={39},
 note ={to appear},
}

@misc{Godskesen89usersmanual,
 author ={Jens Godskesen and Kim Guldstrand Larsen and Michael Zeeberg},
 title ={TAV -- tools for automatic verification -- Users Manual},
 year ={1989},
}

@misc{uppaal2k,
 author ={Kim Guldstrand Larsen and P. Pettersson},
 title ={UPPAAL2k},
 booktitle ={BRICS Newsletter no 10},
 year ={1999},
 month ={October},
}

@misc{BDHHL,
 key ={},
 author ={G. Behrmann and A. David and J. H{\aa}konsson and M. Hendriks and Kim Guldstrand Larsen and P. Pettesson and Wang Yi},
 title ={Unleash the Power of UPPAAL 4.0},
 note ={Under submission},
}

@misc{BCDFLL,
 author ={G. Behrmann and A., Cougnard and A. David and E. Fleury, Kim Guldstrand Larsen and D. Lime},
 title ={Be a Winner with UPPAAL-Tiga},
 note ={Under submission},
}

@misc{teaching,
 author ={Luca Aceto and Anna Ingolfsdottir and Kim Guldstrand Larsen and Jiri Srba},
 title ={Teaching Concurrency: Theory in Practice},
 year ={2009},
 note ={Under submission},
}

@misc{uppaalpro,
 author ={Alexandre David and Arild Haugstad and Kim G. Larsen},
 title ={UPPAAL PRO: Tool for Performance Analysis of Probabilistic Timed Automata},
 howpublished ={Under submittion},
 year ={2009},
 note ={Under submission},
}

@inproceedings{10.1007/978-3-540-75454-1,
 author ={Henning Dierks and Sebastian Kupferschmid and Kim Guldstrand Larsen},
 title ={Automatic Abstraction Refinement for Timed Automata},
 booktitle ={Proceedings of Formal Modeling and Analysis of Timed Systems, 5th International Conference, (FORMATS)},
 pages ={114-129},
 year ={2007},
 doi ={10.1007/978-3-540-75454-1},
 volume ={4763},
 series ={Lecture Notes in Computer Science},
 publisher ={Springer-Verlag},
 abstract ={We present a fully automatic approach for counterexample guided abstraction refinement of real-time systems modelled in a subset of timed automata. Our approach is implemented in the Moby/RT tool environment, which is a CASE tool for embedded system specifications. Verification in Moby/RT is done by constructing abstractions of the semantics in terms of timed automata which are fed into the model checker Uppaal. Since the abstractions are over-approximations, absence of abstract counterexamples implies a valid result for the full model. Our new approach deals with the situation in which an abstract counterexample is found by Uppaal. The generated abstract counterexample is used to construct either a crete counterexample for the full model or to identify a slightly refined abstraction in which the found spurious counterexample cannot occur anymore. Hence, the approach allows for a fully automatic abstraction refinement loop starting from the coarsest abstraction towards an abstraction for which a valid verification result is found. Nontrivial case studies demonstrate that this approach computes small abstractions fast without any user interaction. -- This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center "Automatic Verification and Analysis of Complex Systems" (SFB/TR 14 AVACS). See http://www.avacs.org/ for more information.},
}

@inproceedings{j.entcs.2008.11.007,
 author ={Alexandre David and Kim Guldstrand Larsen and Shuhao Li and Brian Nielsen},
 title ={Cooperative Testing of Timed Systems},
 key ={Timed game automata; test purpose; winning strategy; cooperative strategy; test case},
 booktitle ={Proceedings of the 4th Workshop on Model-based Testing (MBT)},
 pages ={79-92},
 year ={2008},
 series ={Electronic Notes in Theoretical Computer Science},
 volume ={220},
 publisher ={Elsevier Science Publishers},
 ee ={http://dx.doi.org/10.1016/j.entcs.2008.11.007},
 abstract ={This paper deals with targeted testing of timed systems whose models may have uncontrollable behavior. The testing activity is viewed as a game between the tester and the system under test (SUT) towards a given test purpose. The SUT is modeled as Timed Game Automaton and the test purpose is specified in Timed CTL formula. We employ a timed game solver UPPAAL-TIGA to check if the test purpose is ture w.r.t. the model, and if yes, to generate a winning strategy and use it for black-box conformance testing of the SUT implementation. Specifically, we show that in case the checking yields a negative result, we can still test the SUT implementation against the test purpose as long as the SUT implementation reacts to our moves in a cooperative style. We present an operational framework of cooperative winning strategy generation, test case derivation and execution. The test method is proved to be sound and complete. Preliminary experimental results indicate that this approach is applicable to non-trivial timed systems.},
}

@article{10.1109/ICST.2009.38,
 author ={Alexandre David and Kim Guldstrand Larsen and Shuhao Li and Brian Nielsen},
 title ={Timed Testing under Partial Observability},
 journal ={Software Testing, Verification, and Validation, 2008 International Conference on},
 volume ={0},
 year ={2009},
 isbn ={978-0-7695-3601-9},
 pages ={61-70},
 ee ={http://doi.ieeecomputersociety.org/10.1109/ICST.2009.38},
 publisher ={IEEE Computer Society},
 address ={Los Alamitos, CA, USA},
 abstract ={This paper studies the problem of model-based testing of real-time systems that are only partially observable. We model the System Under Test (SUT) using Timed Game Automata (TGA) which has internal actions, uncontrollable outputs and timing uncertainty of outputs. We define the partial observability of SUT using a set of predicates over the TGA state space, and specify the test purposes in Computation Tree Logic (CTL) formulas. A recently developed partially observable timed game solver is used to generate winning strategies, which are used as test cases. We propose a conformance testing framework, define a partial observation-based conformance relation, present the test execution algorithms, and prove the soundness and completeness of this test method (i.e., a detected error really violates the conformance relation; and if the SUT violates the test purpose, then a test case can be generated to detect this violation). Experiments on some non-trivial examples show that this method yields encouraging results.},
}

@inproceedings{FL09,
 author ={Ulrich Fahrenberg and Kim Guldstrand Larsen},
 title ={Discounting in Time},
 booktitle ={proceedings of 7th Workshop on Quantitative Aspects of Programming Languages},
 year ={2009},
 note ={to appear},
}

@inproceedings{Larsen09Verification,
 author ={Kim Guldstrand Larsen},
 title ={Quantitative Verification and Validation of Embedded Systems},
 booktitle ={Proceedings of of 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE09, Tianjin, China},
 year ={2009},
 note ={to appear},
}

@inproceedings{Larsen09Quantitative,
 author ={Kim Guldstrand Larsen},
 title ={Quantitative and Compositional Model Checking},
 booktitle ={Proceedings of Seventh International Andrei Ershov Memorial Conference (PSI), Novosibirsk, Russia},
 year ={2009},
 note ={to appear},
}

@inproceedings{DLL09,
 author ={Alexandre David and Kim Guldstrand Larsen and Didier Lime},
 title ={UPPAAL TIGA 2009 - towards realizable strategies},
 booktitle ={Proceedings of Workshop on Games for Design, Verification and Synthesis, GASICS},
 year ={2009},
 note ={to appear},
}

@article{BKLS09,
 author ={Nikola Benes and Jan Kretinsky and Kim Guldstrand Larsen and Jiri Srba},
 title ={On Determinism in Modal Transition Systems},
 journal ={Special Issue of Theoretical Computer Science},
 year ={2009},
 note ={to appear},
}

@article{BFLM09,
 author ={Patricia Bouyer and Ulrich Fahrenberg and Kim Guldstrand Larsen and Nicolas Markey},
 title ={Quantitative Modeling and Analysis of Embedded Systems},
 journal ={Communications of the ACM},
 year ={2009},
 note ={Invited paper, to appear},
}

@article{JLAP10,
 author ={Claus Thrane and Uli Fahrenberg and Kim Guldstrand Larsen},
 title ={Quantitative Analysis of Weighted Transition Systems},
 journal ={Journal of Logic and Algebraic Programming},
 year ={2010},
 volume ={79},
 number ={7},
 pages ={689-703},
 abstract ={We present a general framework for the analysis of quantitative and qualitative properties of reactive systems, based on a notion of weighted transition systems. We introduce and analyze three different types of distances on weighted transi- tion systems, both in a linear and a branching version. Our quantitative notions appear to be reasonable extensions of the standard qualitative concepts, and the three different types introduced are shown to measure inequivalent properties. When applied to the formalism of weighted timed automata, we show that some standard decidability and undecidability results for timed automata extend to our quantitative setting.},
 pdf ={TFL09.pdf},
}

@inproceedings{ThraneSorensenLarsen:jlap:08,
 author ={Claus Thrane and Uffe S{\o}rensen and Kim Guldstrand Larsen},
 title ={Slicing for Uppaal},
 crossref ={NWPT:08},
 booktitle ={NWPT},
 pages ={100-103},
 year ={2008},
 abstract ={We present slicing for the model-checking tool Uppaal [5]. Slicing is a technique based on static analysis used here to reduce the syntactic size of models based on an extension of Timed Automata [1]. We show how our approach will obtain reachability preserving reductions of models, possibly improving the performance of the tool. Finally, we present the results of experimental conducted to further validate our claims...},
}

@inproceedings{ThraneFahrenbergLarsen:jlap:08,
 author ={Claus Thrane and Uli Fahrenberg and Kim Guldstrand Larsen},
 title ={Quantitative Simulations of Weighted Transition Systems},
 crossref ={NWPT:08},
 booktitle ={NWPT},
 pages ={97-100},
 year ={2008},
 note ={Extended version invited for publication in Special Issue of Journal of Logic and Algebraic Programming, 2009},
 abstract ={We present research motivated by the Challenge on embedded systems design, posed by Henzinger and Sifakis in [5]. Henzinger and Sifakis express the need for a co- herent theory of embedded systems design, where concern for physical constraints is supported by the computational models used to model software, thus achieving a more het- erogeneous approach to systems design. Highly distilled, Henzinger and Sifakis call for a new mathematical basis for systems modeling, which facilitates modeling of be- havioural properties as well as environmental constraints. In this work we propose a notion of weighted transi- tion systems (WTS), a quantitative extension... },
}

@proceedings{NWPT:08,
 title ={Proceedings of 20th Nordic Workshop of Programming Theory},
 year ={2008},
 booktitle ={NWPT},
 editor ={Tarmo Uustalu, J{\"u}ri Vain and Juhan Ernits},
 month ={November},
 organization ={Institute of Cybernetics at Tallinn University of Technology Akadeemia tee 21, 12618 Tallinn, Estonia},
 note ={Published as an Institute of Cybernetics report},
 ee ={http://cs.ioc.ee/nwpt08/abstracts-book.pdf},
}

@unpublished{FahrenbergLarsenThrane:Quantlog,
 author ={Uli Fahrenberg and Kim Guldstrand Larsen and Claus Thrane},
 title ={A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic.},
 year ={2009},
 note ={Submitted as abstract for invited talk at QUANTLOG, a satellite event of ICALP 2009, Rhodes},
 abstract ={We extend the usual notion of Kripke Structures with a weighted tran- sition relation, and generalize the usual Boolean satisfaction relation of CTL, to a map assigning states and temporal formulae with a real-valued distance, describing the degree of satisfaction. We describe a general ap- proach to obtaining quantitative interpretations for a generic extension of the CTL syntax, and show that, for one such interpretation, the logic is both adequate and expressive with respect quantitative bisimulation.},
}

@inproceedings{FahrenbergLarsenThrane:FSEN:09,
 author ={Uli Fahrenberg and Kim Guldstrand Larsen and Claus Thrane},
 title ={Verification, Performance Analysis and Controller Synthesis for Real-Time Systems},
 crossref ={FSEN:09},
 booktitle ={FSEN 09},
 year ={2009},
 note ={to appear},
 abstract ={This note aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the timed automata mod- eling formalism introduced by Alur and Dill [7,8]. The note gives com- prehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on asso- ciated decision problems related to model checking, equivalence checking, optimal scheduling, and winning strategies},
}

@proceedings{FSEN:09,
 title ={Proceedings of 3rd International Conference on Fundamentals of Software Engineering, 15 - 17 April, Kish Island, Persian Gulf, Iran},
 year ={2009},
 booktitle ={FSEN 09},
 month ={April},
 publisher ={Springer-Verlag},
 note ={to appear},
}

@inproceedings{FahrenbergLarsenThrane:ASI:08,
 author ={Uli Fahrenberg and Kim Guldstrand Larsen and Claus Thrane},
 title ={Verification, Performance Analysis and Controller Synthesis for Real-Time Systems},
 crossref ={ASI:08},
 booktitle ={ASI 08},
 year ={2008},
 abstract ={This note aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the timed automata mod- eling formalism introduced by Alur and Dill [7,8]. The note gives com- prehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on asso- ciated decision problems related to model checking, equivalence checking, optimal scheduling, and winning strategies},
}

@proceedings{ASI:08,
 title ={Proceedings of the NATO Advanced Study Institute on Engineering Methods and Tools for Software Safety and Security Marktoberdorf, Germany 5-17 August 2008},
 year ={2008},
 booktitle ={ASI 08},
 editor ={Manfred Broy , Wassiou Sitou and Tony Hoare},
 volume ={22},
 series ={NATO Science for Peace and Security Series - D: Information and Communication Security},
 publisher ={IOS Press BV},
 ee ={http://www.booksonline.iospress.com/Content/View.aspx?piid=11975},
}

@inproceedings{LarsenSkov:91,
 author ={Kim Guldstrand Larsen and Arne Skou},
 title ={Bisimulation Through Probabilistic Testing},
 booktitle ={Information and Control (IC'91)},
 year ={1991},
 volume ={9},
 number ={1},
}

@inproceedings{Larsen97timeabstracted,
 author ={Kim Guldstrand Larsen and Yi Wang},
 title ={Time Abstracted Bisimulation: Implicit Specifications and Decidability},
 booktitle ={Information and Computation},
 year ={1997},
 publisher ={Springer Verlag},
}

@inproceedings{Jonsson01probabilisticextensions,
 author ={Bengt Jonsson and Kim Guldstrand Larsen and Wang Yi},
 title ={Probabilistic Extensions of Process Algebras},
 booktitle ={Handbook of Process Algebra},
 year ={2001},
 pages ={685--710},
 publisher ={Elsevier},
 ee ={http://www.elsevier.com/wps/find/bookdescription.cws_home/621352/description},
 abstract ={Classic process, algebras such as CCS, CSP and ACP, are well-established techniques for modelling and reasoning about functional aspects of concurrent processes. The motivation for studying probabilistic extensions of process algebras is to develop techniques dealing with non-functional aspects of process behavior, such as performance and reliability. We may want to investigate, e.g., the average response time of a system, or the ? This chapter is dedicated to the fond memory of Linda Christoff. probability that a certain failure occurs. An analysis of these and similar properties requires that some form of information about the stochastic distribution over the occurrence of relevant events is put into the model. For instance, performance evaluation is often based on modeling a system as a continuous-time Markov process, in which distributions over delays between actions and over the choice between different actions are specified. Similar},
}

@article{1331460,
 author ={Patricia Bouyer and Ed Brinksma and Kim Guldstrand Larsen},
 title ={Optimal infinite scheduling for multi-priced timed automata},
 journal ={Form. Methods Syst. Des.},
 volume ={32},
 number ={1},
 year ={2008},
 issn ={0925-9856},
 pages ={3--23},
 ee ={http://dx.doi.org/10.1007/s10703-007-0043-4},
 publisher ={Kluwer Academic Publishers},
 address ={Hingham, MA, USA},
 bibsource ={ACM Portal},
 abstract ={This paper is concerned with the derivation of infinite schedules for timed automata that are in some sense optimal. To cover a wide class of optimality criteria we start out by introducing an extension of the (priced) timed automata model that includes both costs and rewards as separate modelling features. A precise definition is then given of what constitutes optimal infinite behaviours for this class of models. We subsequently show that the derivation of optimal non-terminating schedules for such double-priced timed automata is computable. This is done by a reduction of the problem to the determination of optimal mean-cycles in finite graphs with weighted edges. This reduction is obtained by introducing the so-called corner-point abstraction, a powerful abstraction technique of which we show that it preserves optimal schedules.},
 pdf ={1331460.pdf},
}

@inproceedings{216510,
 author ={Havelund, Klaus and Larsen, Kim Guldstrand},
 title ={A refinement logic for the Fork Calculus},
 booktitle ={PSTV '94: Proceedings of the fourteenth of a series of annual meetings on Protocol specification, testing and verification XIV},
 year ={1995},
 isbn ={0-412-63640-9},
 pages ={5--20},
 location ={Vancouver, Canada},
 publisher ={Chapman \& Hall, Ltd.},
 address ={London, UK, UK},
}

@inproceedings{Jensen96modellingand,
 author ={Henrik Ejersbo Jensen and Jensen Kim and Kim Guldstrand Larsen and Arne Skou},
 title ={Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL},
 booktitle ={Proceedings of the 2nd International Workshop on the SPIN Verification System},
 year ={1996},
 abstract ={This paper compares the tools SPIN and UPPAAL by modelling and verifying a Collision Avoidance Protocol for an Ethernet--like medium. We find that SPIN is well suited for modelling the untimed aspects of the protocol processes and for expressing the relevant (untimed) properties. However, the modelling of the media becomes ackward due to the lack of broadcast communication in the PROMELA language. On the other hand we find it easy to model the timed aspects using the UPPAAL tool. Especially, the notion of committed locations supports the modelling of broadcast communication. However, the property language of UPPAAL lacks some expessivity for verification of bounded liveness properties, and we indicate how timed testing automata may be constructed for such properties, inspired by the (untimed) checking automata of SPIN. 1 Motivation During the last few years, the SPIN tool [Hol91] has attracted much interest from university people teaching formal methods and from industrial developers....},
}

@inproceedings{Behrmann97contextdependent,
 author ={Gerd Behrmann and Kåre Kristoffersen and Kim Larsen},
 title ={Context Dependent Minimization of State/Event Systems},
 booktitle ={Proceedings of Nordic Workshop of Programming Correctness},
 year ={1997},
 abstract ={This paper presents a technique for efficiently checking reachability properties of concurrent state/event systems. The technique improves the traditional algorithm for forwards exploration of the global state space by incremental construction of subsystems which are kept small using a context dependent minimization. A tool has been implemented with the specific purpose of verifying state/event systems. Experimental results reports on a feasible automatic verification of correctness of Milner's Scheduler -- an often used benchmark -- with 100 cells. This result dramatically improves the previous best results for this benchmark. Also our tehcnique has been shown to perform well on industrial designs of sizes up to 400 concurrent state machines. Keywords: State/event systems; Reachability analysis; Compositionality; Subsystems; Context Dependent Minimization. 1 Introduction Model checking of finite--state concurrent systems suffers from the potential combinatorial explosion o...},
}

@techreport{BRICS-RS-97-13,
 author ={Andersen, J{\o}rgen H. and Larsen, Kim Guldstrand},
 title ={Compositional Safety Logics},
 institution ={brics},
 year ={1997},
 type ={rs},
 number ={RS-97-13},
 address ={iesd},
 month ={jun},
 note ={16~pp},
 abstract ={In this paper we present a generalisation of a promising compositional model checking technique introduced for finite-state systems by Andersen and extended to networks of timed automata by Larsen et al. In our generalized setting, programs are modelled as arbitrary (possibly infinite-state) transition systems and verified with respect to properties of a basic safety logic. As the fundamental prerequisite of the compositional technique, it is shown how logical properties of a parallel program may be transformed into necessary and sufficient properties of components of the program. Finally, a set of axiomatic laws are provided useful for simplifying formulae and complete with respect to validity and unsatisfiability},
}

@article{10.1109/REAL.1997.641265,
 author ={Kim Guldstrand Larsen and F. Larsson and P. Pettersson and W. Yi},
 title ={Efficient verification of real-time systems: compact data structure and state-space reduction},
 journal ={Real-Time Systems Symposium, IEEE International},
 volume ={0},
 year ={1997},
 issn ={1052-8725},
 pages ={14},
 ee ={http://doi.ieeecomputersociety.org/10.1109/REAL.1997.641265},
 publisher ={IEEE Computer Society},
 address ={Los Alamitos, CA, USA},
 abstract ={During the past few years, a number of verification tools have been developed for real-time systems in the framework of timed automata (e.g. KRONOS and UPPAAL). One of the major problems in applying these tools to industrial-size systems is the huge memory-usage for the exploration of the state-space of a network (or product) of timed automata, as the model-checkers must keep information on not only the control structure of the automata but also the clock values specified by clock constraints. In this paper, we present a compact data structure for representing clock constraints. The data structure is based on an O(n/sup 3/) algorithm which, given a constraint system over real-valued variables consisting of bounds on differences, constructs an equivalent system with a minimal number of constraints. In addition, we have developed an on-the-fly, reduction technique to minimize the space-usage. Based on static analysis of the control structure of a network of timed automata, we are able to compute a set of symbolic states that cover all the dynamic loops of the network in an on-the-fly searching algorithm, and thus ensure termination in reachability analysis. The two techniques and their combination have been implemented in the tool UPPAAL. Our experimental results demonstrate that the techniques result in truly significant space-reductions: for six examples from the literature, the space saving is between 75\% and 94\%, and in (nearly) all examples time-performance is improved. Also noteworthy is the observation that the two techniques are completely orthogonal.},
}

@inproceedings{10.1109/REAL.1997.641264,
 author ={Klaus Havelund and Arne Skou and Kim Guldstrand Larsen and Kristian Lund},
 title ={Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL},
 booktitle ={Proceedings of the 18th IEEE Real-Time Systems Symposium (December 03 - 05, 1997)},
 pages ={2},
 year ={1997},
 publisher ={IEEE Computer Society},
 ee ={http://doi.ieeecomputersociety.org/10.1109/REAL.1997.641264},
 abstract ={A formal and automatic verification of a real-life protocol is presented. The protocol, about 2800 lines of assembler code, has been used in products from the audio/video company Bang & Olufsen throughout more than a decade, and its purpose is to control the transmission of messages between audio/video components over a single bus. Such communications may collide, and one essential purpose of the protocol is to detect such collisions. The functioning is highly dependent on real-time considerations. Though the protocol was known to be faulty in that messages were lost occasionally, the protocol was too complicated in order for Bang & Olufsen to locate the bug using normal testing. However using the real-time verification tool UPPAAL, an error trace was automatically generated, which caused the detection of "the error" in the implementation. The error was corrected and the correction was automatically proven correct, again using UPPAAL. A future, and more automated, version of the protocol, where this error is fatal, will incorporate the correction. Hence, this work is an elegant demonstration of how model checking has had an impact on practical software development. The effort of modeling this protocol has in addition generated a number of suggestions for enriching the UPPAAL language. Hence, it's also an excellent example of the reverse impact.},
}

@inproceedings{Bengtsson98newgeneration,
 author ={Johan Bengtsson and Kim Larsen and Fredrik Larsson and Paul Pettersson and Yi Wang and Carsten Weise},
 title ={New Generation of UPPAAL},
 booktitle ={proceedings of the International Workshop on Software Tools for Technology Transfer},
 year ={1998},
 address ={Aalborg, Denmark},
 abstract ={Uppaal is a tool-set for the design and analysis of real-time systems. In [6] a relatively complete description of Uppaal before 1997 has been given. This paper is focused on the most recent developments and also to complement the paper of [6]. 1 UPPAAL's Past: the History The first prototype of Uppaal, named Tab at the time, was developed at Uppsala University in 1993 by Wang Yi et al. Its theoretical foundation was presented in FORTE94 [11] and the initial design was to check safety properties that can be formalized as simple reachability properties for networks of timed automata. The restriction to this simple class of properties was in sharp contrast to other real-time verification tools at that time, which where developed to check timed bisimularities or formulae of timed modal ¯-calculi. However, the ambition of catering for more complicated formulae lead to extremely severe restrictions in the size of systems that could be verified by those tools. The essential ideas behind T...},
}

@inproceedings{Larsen99clockdifference,
 author ={Kim Guldstrand Larsen and Justin Pearson and Carsten Weise and Wang Yi},
 title ={Clock Difference Diagrams},
 booktitle ={Proceedings of Nordic Workshop of Programming Theory},
 year ={1999},
 address ={Turku},
 address ={In this paper, we present Clock Difference Diagrams, a new BDD- like data-structure for effective representation and manipulation of certain non-convex subsets of the Euclidean space, notably those encountered in verification of timed automata. It is shown that all set-theoretic operations including inclusion checking may be carried out efficiently on Clock Difference Diagrams. Other central operations needed for analysing timed automata (e.g. future- and reset-operations), are readily defined using an effectively obtained, relative normal form. A version of the real-time verification tool Uppaal using Clock Difference Diagrams as the main data-structure has been implemented. Experimental results demonstrate significant space-savings: between 46\% and 99\% for a number of industrial examples. 1 Introduction Model-checking has established itself as a very powerful technique for checking whether a given formally described system satisfies a desired property. For parallel systems, model-c...},
}

@inproceedings{ABBL:FSTTCS:98,
 author ={L. Aceto and P. Bouyer and A. Burgueno and Kim Guldstrand Larsen},
 title ={The Limit of Testing for Timed Automata},
 year ={1998},
 volume ={1579},
 series ={Lecture Notes in Computer Science},
 booktitle ={Proceedings of Foundations of Software Technology and Theoretical Computer Science, India, 1998.},
}

@inproceedings{Bodentien_verificationof,
 author ={Nicky Oliver Bodentien and Jacob Vestergaard and Jakob Friis and Nicky Oliver and Bodentien Jacob and Vestergaard Jakob Friis and Kåre Jelling Kristoffersen and Kristoffersen Kim and Kim Guldstrand Larsen},
 title ={Verification of State/Event Systems by Quotienting},
 booktitle ={Proceedings of Nordic Workshop of Programming Theory},
 year ={1999},
 address ={Sweden},
 abstract ={A rather new approach towards compositional verification of concurrent systems is the quotient technique, where components are gradually removed from the concurrent system while transforming the specification accordingly. When the intermediate specifications can be kept small using heuristics for minimization, the state explosion problem is avoided and there are already promising experimental results for systems with an interleaving semantics, including real-time systems. This paper extends the quotienting approach to deal with a synchronous framework in the shape of state/event systems. A state/event system is a concurrent system with a set of interdependent components operating synchronously according to stimuli (input events) provided by an environment while producing output events in return for the environment. A compositional modal logic M suitable for expressing general safety and liveness properties subsystems is introduced. A quotient construction for bulding components from a...},
}

@techreport{Kristoffersen99experimentalbatch,
 author ={Kare Kristoffersen and Kim Guldstrand Larsen and Paul Pettersson and Carsten Weise},
 title ={Experimental Batch Plant - Case Study 1 Using Timed Automata and UPPAAL},
 institution ={},
 year ={1999},
 note ={Deliverable of ESPRIT-LTR Project 26270 VHS (Verification of Hybrid Systems). Full version to appear in Special Issue of European Journal of Control on ``Verification of Hybrid Systems'},
 abstract ={In this report we present the modelling of the experimental batch plant of case study 1 using timed automata. Requirements of safety and bounded liveness (efficiency requirements) are given as reachability properties and the model checker UPPAAL is applied to perform verification. 1 The Model 1.1 Timed automata and UPPAAL We describe the experimental batch plant as a parallel composition of timed automata. In UPPAAL a timed automaton is a finite state machine extended with clocks, integer variables and synchronization labels. The synchronization mechanism is that of binary handshake between two automata. This work was partially supported by the European Community Esprit-LTR Project 26270 VHS (Verification of Hybrid systems) 1 The framework of timed automata offers the possibility to model continous behaviour, i.e. the plant, as well as discrete behaviour, i.e. the control programs. The model checker UPPAAL with its built--in simulation facility provides a fast and efficient ...},
}

@inproceedings{980713,
 title ={UPPAAL - present and future},
 author ={Behrmann, G. and Kim Guldstrand Larsen and Moller, O. and David, A. and Pettersson, P. and Wang Yi},
 booktitle ={Decision and Control, 2001. Proceedings of the 40th IEEE Conference on},
 year ={2001},
 month ={},
 volume ={3},
 number ={},
 pages ={2881-2886 vol.3},
 abstract ={UPPAAL is a tool for modelling, simulation and verification of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool is appropriate for systems that can be modelled as a collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels or shared variables. Typical application areas include real-time controllers and communication protocols in particular, those where timing aspects are critical. In this paper, we review the status of the currently distributed version of the tool as well as facilities to be found in upcoming releases},
 keywords ={control system CAD, digital simulation, graphical user interfaces, protocols, real-time systems, software toolsAalborg University, UPPAAL, Uppsala University, car locking system, communication protocols, digital simulation, graphical user interface, modelling tool, real-time systems},
 ee ={http://doi.ieeecomputersociety.org/10.1109/.2001.980713},
}

@inproceedings{10.1007/3-540-44804-7,
 author ={Pedro R. D'Argenio and Bertrand Jeannet and Henrik E. Jensen and Kim Guldstrand Larsen},
 title ={Reachability Analysis of Probabilistic Systems by Successive Refinements},
 booktitle ={Process Algebra and Probabilistic Methods. Performance Modelling and Verification},
 pages ={39-56},
 year ={2001},
 volume ={2165},
 series ={Lecture Notes in Computer Science},
 address ={Aachen, Germany},
 month ={September},
 publisher ={Springer-Verlag},
 ee ={http://doi.ieeecomputersociety.org/10.1007/3-540-44804-7},
}

@inproceedings{Into02solvingplanning,
 author ={Henning Dierks and Gerd Behrmann and Kim Guldstrand Larsen},
 title ={Solving Planning Problems Using Real-Time Model Checking},
 booktitle ={AIPS-Workshop Planning via Model-Checking},
 year ={2002},
 pages ={30--39},
}

@inproceedings{,
 author ={Alexandre David and Gerd Behrmann and Kim Guldstrand Larsen and Wang Yi},
 title ={New uppaal architecture},
 booktitle ={In Proceedings of RT-TOOLS 2002},
 note ={to appear in SPIN Proceedings 2003},
 abstract ={We present the design and internal data structures for the next generation of UPPAAL. Early experimental results demonstrate that the new implementation based on these structures improves the efficiency of UPPAAL by about 80\% in both time and space. In addition, the new version is built to handle hierarchical models. The challenge in handling hierarchy comes from the very dynamic structure of hierarchical systems: the levels of concurrency and the scope of data variables and clocks are changing. We present data structures and a searching scheme for state space exploration of hierarchical models.},
}

@inproceedings{1342774,
 title ={T-UPPAAL: online model-based testing of real-time systems},
 author ={Mikucionis, M. and Larsen, Kim Guldstrand and Nielsen, B.},
 booktitle ={Automated Software Engineering, 2004. Proceedings. 19th International Conference on},
 year ={2004},
 month ={Sept.},
 volume ={},
 number ={},
 pages ={396-397},
 abstract ={The goal of testing is to gain confidence in a physical computer based system by means of executing it. More than one third of typical project resources are spent on testing embedded and real-time systems, but still it remains ad-hoc, based on heuristics, and error-prone. Therefore systematic, theoretically well-founded and effective automated real-time testing techniques are of great practical value. Testing conceptually consists of three activities: test case generation, test case execution and verdict assignment. We present T-UPPAAL-a new tool for model based testing of embedded real-time systems that automatically generates and executes tests "online" from a state machine model of the implementation under test (IUT) and its assumed environment which combined specify the required and allowed observable (realtime) behavior of the IUT. T-UPPAAL implements a sound and complete randomized testing algorithm, and uses a formally defined notion of correctness (relativized timed input/output conformance) to assign verdicts. Using online testing, events are generated and simultaneously executed.},
 keywords ={ automatic testing, embedded systems, program testing, program verification T-UPPAAL, automated real-time testing, embedded real-time systems, implementation under test, online model-based testing, physical computer based system, randomized testing algorithm, state machine model, test case execution, test case generation, verdict assignment},
 ee ={http://doi.ieeecomputersociety.org/10.1109/ASE.2004.1342774},
 issn ={1068-3062},
}

@inproceedings{LNW:FIT:05,
 author ={Kim Guldstrand Larsen and Ulrik Nyman and Andrzej Wasowski},
 title ={Interface Input/Output Automata: Splitting Assumptions from Guarantees},
 booktitle ={Foundations of Interface Technologies (FIT 2005)},
 year ={2005},
 note ={affiliated workshop of CONCUR 2005. San Francisco, CA, USA, August 20, 2005. Preliminary Proceedings. To be published in ENTCS.},
}

@inproceedings{SNLJ:RTS:05,
 author ={Henrik Schi{\o}ler and Jens Dalsgaard Nielsen and Kim Guldstrand Larsen and Jan Jakob Jessen},
 title ={CyNC - a method for Real Time Analysis of Systems with Cyclic Data Flows},
 booktitle ={Proceedings of 13 th. RTS Conference on Embedded Systems},
 year ={2005},
 month ={April},
}

@inproceedings{SJNL:ECRTS:05,
 author ={Henrik Schi{\o}ler and Jan Jakob Jessen and Jens F. Dalsgaard Nielsen and Kim Guldstrand Larsen},
 title ={CyNC - towards a General Tool for Performance Analysis of Complex Distributed Real Time Systems},
 booktitle ={Proccedings of 17th Euromicro Conference on Real-Time Systems (ECRTS 05)},
 year ={2005},
 address ={Palma de Mallorca, Spanien},
}

@www{DBLP:homepages/l/KimGuldstrandLarsen,
 author ={Kim Guldstrand Larsen},
 title ={Home Page},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/hybrid/CassezJLRR09,
 author ={Franck Cassez and Jan Jakob Jessen and Kim Guldstrand Larsen and Jean-Fran\c{c}ois Raskin and Pierre-Alain Reynier},
 title ={Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study},
 booktitle ={HSCC},
 year ={2009},
 pages ={90-104},
 ee ={http://dx.doi.org/10.1007/978-3-642-00602-9_7},
 crossref ={DBLP:conf/hybrid/2009},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={CassezJLRR09.pdf},
}

@proceedings{DBLP:conf/hybrid/2009,
 editor ={Rupak Majumdar and Paulo Tabuada},
 title ={Hybrid Systems: Computation and Control, 12th International Conference, HSCC 2009, San Francisco, CA, USA, April 13-15, 2009. Proceedings},
 booktitle ={HSCC},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={5469},
 year ={2009},
 isbn ={978-3-642-00601-2},
 ee ={http://dx.doi.org/10.1007/978-3-642-00602-9},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/ictac/BenesKLS09,
 author ={Nikola Benes and Jan Kret\'{\i}nsk{\'y} and Kim Guldstrand Larsen and Jir\'{\i} Srba},
 title ={Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete},
 booktitle ={ICTAC},
 year ={2009},
 pages ={112-126},
 ee ={http://dx.doi.org/10.1007/978-3-642-03466-4_7},
 crossref ={DBLP:conf/ictac/2009},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={BenesKLS09.pdf},
}

@proceedings{DBLP:conf/ictac/2009,
 editor ={Martin Leucker and Carroll Morgan},
 title ={Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings},
 booktitle ={ICTAC},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={5684},
 year ={2009},
 isbn ={978-3-642-03465-7},
 ee ={http://dx.doi.org/10.1007/978-3-642-03466-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/entcs/FahrenbergL09,
 author ={Ulrich Fahrenberg and Kim Guldstrand Larsen},
 title ={Discount-Optimal Infinite Runs in Priced Timed Automata},
 journal ={Electr. Notes Theor. Comput. Sci.},
 volume ={239},
 year ={2009},
 pages ={179-191},
 ee ={http://dx.doi.org/10.1016/j.entcs.2009.05.039},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={FahrenbergL09.pdf},
}

@article{DBLP:journals/entcs/AntonikHLNW09,
 author ={Adam Antonik and Michael Huth and Kim Guldstrand Larsen and Ulrik Nyman and Andrzej Wasowski},
 title ={EXPTIME-complete Decision Problems for Modal and Mixed Specifications},
 journal ={Electr. Notes Theor. Comput. Sci.},
 volume ={242},
 number ={1},
 year ={2009},
 pages ={19-33},
 ee ={http://dx.doi.org/10.1016/j.entcs.2009.06.011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={AntonikHLNW09.pdf},
}

@inproceedings{DBLP:conf/date/DavidLLN08,
 author ={Alexandre David and Kim Guldstrand Larsen and Shuhao Li and Brian Nielsen},
 title ={A Game-Theoretic Approach to Real-Time System Testing},
 booktitle ={DATE},
 year ={2008},
 pages ={486-491},
 ee ={http://dx.doi.org/10.1109/DATE.2008.4484728},
 crossref ={DBLP:conf/date/2008},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 abstract ={This paper presents a game-theoretic approach to the testing of uncontrollable real-time systems. By modelling the systems with timed I/O game automata and specifying the test purposes as Timed CTL formulas, we employ a recently developed timed game solver UPPAAL-TIGA to synthesize winning strategies, and then use these strategies to conduct black-box conformance testing of the systems. The testing process is proved to be sound and complete with respect to the given test purposes. Case study and preliminary experimental results indicate that this is a viable approach to uncontrollable timed system testing.},
 pdf ={DavidLLN08a.pdf},
}

@proceedings{DBLP:conf/date/2008,
 title ={Design, Automation and Test in Europe, DATE 2008, Munich, Germany, March 10-14, 2008},
 booktitle ={DATE},
 publisher ={IEEE},
 year ={2008},
 isbn ={978-3-9810801-3-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/formats/BouyerFLMS08,
 author ={Patricia Bouyer and Ulrich Fahrenberg and Kim Guldstrand Larsen and Nicolas Markey and Jir\'{\i} Srba},
 title ={Infinite Runs in Weighted Timed Automata with Energy Constraints},
 booktitle ={FORMATS},
 year ={2008},
 pages ={33-47},
 ee ={http://dx.doi.org/10.1007/978-3-540-85778-5_4},
 crossref ={DBLP:conf/formats/2008},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 abstract ={We study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (e.g. energy). We ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (e.g. remains between 0 and some given upper-bound). We also consider a game version of the above, where certain transitions may be uncontrollable.},
 pdf ={BouyerFLMS08.pdf},
}

@proceedings{DBLP:conf/formats/2008,
 editor ={Franck Cassez and Claude Jard},
 title ={Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings},
 booktitle ={FORMATS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={5215},
 year ={2008},
 isbn ={978-3-540-85777-8},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fossacs/AntonikHLNW08,
 author ={Adam Antonik and Michael Huth and Kim Guldstrand Larsen and Ulrik Nyman and Andrzej Wasowski},
 title ={Complexity of Decision Problems for Mixed and Modal Specifications},
 booktitle ={FoSSaCS},
 year ={2008},
 pages ={112-126},
 ee ={http://dx.doi.org/10.1007/978-3-540-78499-9_9},
 crossref ={DBLP:conf/fossacs/2008},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 abstract ={We consider decision problems for modal and mixed transition systems used as specifications: the common implementation problem (whether a set of specifications has a common implementation), the consistency problem (whether a single specification has an implementation), and the thorough refinement problem (whether all implementations of one specification are also implementations of another one). Common implementation and thorough refinement are shown to be PSPACE-hard for modal, and so also for mixed, specifications. Consistency is PSPACE-hard for mixed, while trivial for modal specifications. We also supply upper bounds suggesting strong links between these problems.},
 pdf ={AntonikHLNW08.pdf},
}

@proceedings{DBLP:conf/fossacs/2008,
 editor ={Roberto M. Amadio},
 title ={Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings},
 booktitle ={FoSSaCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4962},
 year ={2008},
 isbn ={978-3-540-78497-5},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fortest/HesselLMNPS08,
 author ={Anders Hessel and Kim Guldstrand Larsen and Marius Mikucionis and Brian Nielsen and Paul Pettersson and Arne Skou},
 title ={Testing Real-Time Systems Using UPPAAL},
 booktitle ={Formal Methods and Testing},
 year ={2008},
 pages ={77-117},
 ee ={http://dx.doi.org/10.1007/978-3-540-78917-8_3},
 crossref ={DBLP:conf/fortest/2008},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 abstract ={This chapter presents principles and techniques for model-based black-box conformance testing of real-time systems using the Uppaal model-checking tool-suite. The basis for testing is given as a network of concurrent timed automata specified by the test engineer. Relativized input/output conformance serves as the notion of implementation correctness, essentially timed trace inclusion taking environment assumptions into account. Test cases can be generated offline and later executed, or they can be generated and executed online. For both approaches this chapter discusses how to specify test objectives, derive test sequences, apply these to the system under test, and assign a verdict.},
 pdf ={HesselLMNPS08.pdf},
}

@proceedings{DBLP:conf/fortest/2008,
 editor ={Robert M. Hierons and Jonathan P. Bowen and Mark Harman},
 title ={Formal Methods and Testing, An Outcome of the FORTEST Network, Revised Selected Papers},
 booktitle ={Formal Methods and Testing},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4949},
 year ={2008},
 isbn ={978-3-540-78916-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/jtres/BogholmKOTL08,
 author ={Thomas B{\o}gholm and Henrik Kragh-Hansen and Petur Olsen and Bent Thomsen and Kim Guldstrand Larsen},
 title ={Model-based schedulability analysis of safety critical hard real-time Java programs},
 booktitle ={JTRES},
 year ={2008},
 pages ={106-114},
 ee ={http://doi.acm.org/10.1145/1434790.1434807},
 crossref ={DBLP:conf/jtres/2008},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={BogholmKOTL08.pdf},
}

@proceedings{DBLP:conf/jtres/2008,
 editor ={Gregory Bollella and C. Douglas Locke},
 title ={Proceedings of the 6th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES 2008, 24-26 September 2008, Santa Clara, California, USA},
 booktitle ={JTRES},
 publisher ={ACM},
 series ={ACM International Conference Proceeding Series},
 volume ={343},
 year ={2008},
 isbn ={978-1-60558-337-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/KupferschmidHL08,
 author ={Sebastian Kupferschmid and J{\"o}rg Hoffmann and Kim Guldstrand Larsen},
 title ={Fast Directed Model Checking Via Russian Doll Abstraction},
 booktitle ={TACAS},
 year ={2008},
 pages ={203-217},
 ee ={http://dx.doi.org/10.1007/978-3-540-78800-3_15},
 crossref ={DBLP:conf/tacas/2008},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={KupferschmidHL08.pdf},
}

@proceedings{DBLP:conf/tacas/2008,
 editor ={C. R. Ramakrishnan and Jakob Rehof},
 title ={Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings},
 booktitle ={TACAS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4963},
 year ={2008},
 isbn ={978-3-540-78799-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/corr/abs-0805-1457,
 author ={Patricia Bouyer and Kim Guldstrand Larsen and Nicolas Markey},
 title ={Model Checking One-clock Priced Timed Automata},
 journal ={CoRR},
 volume ={abs/0805.1457},
 year ={2008},
 ee ={http://arxiv.org/abs/0805.1457},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/entcs/DavidLLN08,
 author ={Alexandre David and Kim Guldstrand Larsen and Shuhao Li and Brian Nielsen},
 title ={Cooperative Testing of Timed Systems},
 journal ={Electr. Notes Theor. Comput. Sci.},
 volume ={220},
 number ={1},
 year ={2008},
 pages ={79-92},
 ee ={http://dx.doi.org/10.1016/j.entcs.2008.11.007},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={DavidLLN08.pdf},
}

@article{DBLP:journals/fmsd/BouyerBL08,
 author ={Patricia Bouyer and Ed Brinksma and Kim Guldstrand Larsen},
 title ={Optimal infinite scheduling for multi-priced timed automata},
 journal ={Formal Methods in System Design},
 volume ={32},
 number ={1},
 year ={2008},
 pages ={3-23},
 ee ={http://dx.doi.org/10.1007/s10703-007-0043-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 abstract ={This paper is concerned with the derivation of infinite schedules for timed automata that are in some sense optimal. To cover a wide class of optimality criteria we start out by introducing an extension of the (priced) timed automata model that includes both costs and rewards as separate modelling features. A precise definition is then given of what constitutes optimal infinite behaviours for this class of models. We subsequently show that the derivation of optimal non-terminating schedules for such double-priced timed automata is computable. This is done by a reduction of the problem to the determination of optimal mean-cycles in finite graphs with weighted edges. This reduction is obtained by introducing the so-called corner-point abstraction, a powerful abstraction technique of which we show that it preserves optimal schedules.},
 pdf ={BouyerBL08.pdf},
}

@article{DBLP:journals/lmcs/BouyerLM08,
 author ={Patricia Bouyer and Kim Guldstrand Larsen and Nicolas Markey},
 title ={Model Checking One-Clock Priced Timed Automata},
 journal ={Logical Methods in Computer Science},
 volume ={4},
 number ={2},
 year ={2008},
 ee ={http://dx.doi.org/10.2168/LMCS-4(2:9)2008},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/LarsenR08,
 author ={Kim Guldstrand Larsen and Jacob Illum Rasmussen},
 title ={Optimal reachability for multi-priced timed automata},
 journal ={Theor. Comput. Sci.},
 volume ={390},
 number ={2-3},
 year ={2008},
 pages ={197-213},
 ee ={http://dx.doi.org/10.1016/j.tcs.2007.09.021},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={LarsenR08.pdf},
}

@inproceedings{DBLP:conf/atva/CassezDLLR07,
 author ={Franck Cassez and Alexandre David and Kim Guldstrand Larsen and Didier Lime and Jean-Fran\c{c}ois Raskin},
 title ={Timed Control with Observation Based and Stuttering Invariant Strategies},
 booktitle ={ATVA},
 year ={2007},
 pages ={192-206},
 ee ={http://dx.doi.org/10.1007/978-3-540-75596-8_15},
 crossref ={DBLP:conf/atva/2007},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/atva/2007,
 editor ={Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura},
 title ={Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings},
 booktitle ={ATVA},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4762},
 year ={2007},
 isbn ={978-3-540-75595-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/BehrmannCDFLL07,
 author ={Gerd Behrmann and Agn{\`e}s Cougnard and Alexandre David and Emmanuel Fleury and Kim Guldstrand Larsen and Didier Lime},
 title ={UPPAAL-Tiga: Time for Playing Games!},
 booktitle ={CAV},
 year ={2007},
 pages ={121-125},
 ee ={http://dx.doi.org/10.1007/978-3-540-73368-3_14},
 crossref ={DBLP:conf/cav/2007},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/2007,
 editor ={Werner Damm and Holger Hermanns},
 title ={Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4590},
 year ={2007},
 isbn ={978-3-540-73367-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/concur/LarsenNW07,
 author ={Kim Guldstrand Larsen and Ulrik Nyman and Andrzej Wasowski},
 title ={On Modal Refinement and Consistency},
 booktitle ={CONCUR},
 year ={2007},
 pages ={105-119},
 ee ={http://dx.doi.org/10.1007/978-3-540-74407-8_8},
 crossref ={DBLP:conf/concur/2007},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/concur/2007,
 editor ={Lu\'{\i}s Caires and Vasco Thudichum Vasconcelos},
 title ={CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings},
 booktitle ={CONCUR},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4703},
 year ={2007},
 isbn ={978-3-540-74406-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/esop/LarsenNW07,
 author ={Kim Guldstrand Larsen and Ulrik Nyman and Andrzej Wasowski},
 title ={Modal I/O Automata for Interface and Product Line Theories},
 booktitle ={ESOP},
 year ={2007},
 pages ={64-79},
 ee ={http://dx.doi.org/10.1007/978-3-540-71316-6_6},
 crossref ={DBLP:conf/esop/2007},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/esop/2007,
 editor ={Rocco De Nicola},
 title ={Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings},
 booktitle ={ESOP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4421},
 year ={2007},
 isbn ={978-3-540-71314-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/formats/DierksKL07,
 author ={Henning Dierks and Sebastian Kupferschmid and Kim Guldstrand Larsen},
 title ={Automatic Abstraction Refinement for Timed Automata},
 booktitle ={FORMATS},
 year ={2007},
 pages ={114-129},
 ee ={http://dx.doi.org/10.1007/978-3-540-75454-1_10},
 crossref ={DBLP:conf/formats/2007},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/formats/2007,
 editor ={Jean-Fran\c{c}ois Raskin and P. S. Thiagarajan},
 title ={Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings},
 booktitle ={FORMATS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4763},
 year ={2007},
 isbn ={978-3-540-75453-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/formats/JessenRLD07,
 author ={Jan Jakob Jessen and Jacob Illum Rasmussen and Kim Guldstrand Larsen and Alexandre David},
 title ={Guided Controller Synthesis for Climate Controller Using Uppaal Tiga},
 booktitle ={FORMATS},
 year ={2007},
 pages ={227-240},
 ee ={http://dx.doi.org/10.1007/978-3-540-75454-1_17},
 crossref ={DBLP:conf/formats/2007},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fossacs/BouyerLM07,
 author ={Patricia Bouyer and Kim Guldstrand Larsen and Nicolas Markey},
 title ={Model-Checking One-Clock Priced Timed Automata},
 booktitle ={FoSSaCS},
 year ={2007},
 pages ={108-122},
 ee ={http://dx.doi.org/10.1007/978-3-540-71389-0_9},
 crossref ={DBLP:conf/fossacs/2007},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={BouyerLM07.pdf},
}

@proceedings{DBLP:conf/fossacs/2007,
 editor ={Helmut Seidl},
 title ={Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings},
 booktitle ={FoSSaCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4423},
 year ={2007},
 isbn ={978-3-540-71388-3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/RasmussenBL07,
 author ={Jacob Illum Rasmussen and Gerd Behrmann and Kim Guldstrand Larsen},
 title ={Complexity in Simplicity: Flexible Agent-Based State Space Exploration},
 booktitle ={TACAS},
 year ={2007},
 pages ={231-245},
 ee ={http://dx.doi.org/10.1007/978-3-540-71209-1_19},
 crossref ={DBLP:conf/tacas/2007},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/tacas/2007,
 editor ={Orna Grumberg and Michael Huth},
 title ={Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings},
 booktitle ={TACAS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4424},
 year ={2007},
 isbn ={978-3-540-71208-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/sttt/LarsenNW07,
 author ={Kim Guldstrand Larsen and Ulrik Nyman and Andrzej Wasowski},
 title ={Modeling software product lines using color-blind transition systems},
 journal ={STTT},
 volume ={9},
 number ={5-6},
 year ={2007},
 pages ={471-487},
 ee ={http://dx.doi.org/10.1007/s10009-007-0046-x},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/caine/SchiolerJDL06,
 author ={Henrik Schi{\o}ler and Jan Jakob Jessen and Jens Dalsgaard and Kim Guldstrand Larsen},
 title ={Introducing synchronisation in deterministic network models},
 booktitle ={CAINE},
 year ={2006},
 pages ={236-243},
 crossref ={DBLP:conf/caine/2006},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/caine/2006,
 editor ={Thomas Philip},
 title ={Proceedings of the ISCA 19th International Conference on Computer Applications in Industry and Engineering, CAINE 2006, November 13-15, 2006, Las Vegas, Nevada, USA},
 booktitle ={CAINE},
 publisher ={ISCA},
 year ={2006},
 isbn ={978-1-880843-61-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fm/LarsenNW06,
 author ={Kim Guldstrand Larsen and Ulrik Nyman and Andrzej Wasowski},
 title ={Interface Input/Output Automata},
 booktitle ={FM},
 year ={2006},
 pages ={82-97},
 ee ={http://dx.doi.org/10.1007/11813040_7},
 crossref ={DBLP:conf/fm/2006},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fm/2006,
 editor ={Jayadev Misra and Tobias Nipkow and Emil Sekerinski},
 title ={FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings},
 booktitle ={FM},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4085},
 year ={2006},
 isbn ={3-540-37215-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/formats/DavidHLP06,
 author ={Alexandre David and John H{\aa}kansson and Kim Guldstrand Larsen and Paul Pettersson},
 title ={Model Checking Timed Automata with Priorities Using DBM Subtraction},
 booktitle ={FORMATS},
 year ={2006},
 pages ={128-142},
 ee ={http://dx.doi.org/10.1007/11867340_10},
 crossref ={DBLP:conf/formats/2006},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/formats/2006,
 editor ={Eugene Asarin and Patricia Bouyer},
 title ={Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, September 25-27, 2006, Proceedings},
 booktitle ={FORMATS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4202},
 year ={2006},
 isbn ={3-540-45026-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fsttcs/BouyerLMR06,
 author ={Patricia Bouyer and Kim Guldstrand Larsen and Nicolas Markey and Jacob Illum Rasmussen},
 title ={Almost Optimal Strategies in One Clock Priced Timed Games},
 booktitle ={FSTTCS},
 year ={2006},
 pages ={345-356},
 ee ={http://dx.doi.org/10.1007/11944836_32},
 crossref ={DBLP:conf/fsttcs/2006},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fsttcs/2006,
 editor ={S. Arun-Kumar and Naveen Garg},
 title ={FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings},
 booktitle ={FSTTCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={4337},
 year ={2006},
 isbn ={3-540-49994-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/qest/BehrmannDLHPYH06,
 author ={Gerd Behrmann and Alexandre David and Kim Guldstrand Larsen and John H{\aa}kansson and Paul Pettersson and Wang Yi and Martijn Hendriks},
 title ={UPPAAL 4.0},
 booktitle ={QEST},
 year ={2006},
 pages ={125-126},
 ee ={http://doi.ieeecomputersociety.org/10.1109/QEST.2006.59},
 crossref ={DBLP:conf/qest/2006},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/qest/2006,
 title ={Third International Conference on the Quantitative Evaluaiton of Systems (QEST 2006), 11-14 September 2006, Riverside, California, USA},
 booktitle ={QEST},
 publisher ={IEEE Computer Society},
 year ={2006},
 isbn ={0-7695-2665-9},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/fmsd/RasmussenLS06,
 author ={Jacob Illum Rasmussen and Kim Guldstrand Larsen and K. Subramani},
 title ={On using priced timed automata to achieve optimal scheduling},
 journal ={Formal Methods in System Design},
 volume ={29},
 number ={1},
 year ={2006},
 pages ={97-114},
 ee ={http://dx.doi.org/10.1007/s10703-006-0014-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/jec/SchiolerNLJ06,
 author ={Henrik Schi{\o}ler and Jens Dalsgaard Nielsen and Kim Guldstrand Larsen and Jan Jakob Jessen},
 title ={CyNC: A method for real time analysis of systems with cyclic data flows},
 journal ={J. Embedded Computing},
 volume ={2},
 number ={3-4},
 year ={2006},
 pages ={347-360},
 ee ={http://iospress.metapress.com/content/l714587741733r16/},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/sttt/BehrmannBLP06,
 author ={Gerd Behrmann and Patricia Bouyer and Kim Guldstrand Larsen and Radek Pel{\'a}nek},
 title ={Lower and upper bounds in zone-based abstractions of timed automata},
 journal ={STTT},
 volume ={8},
 number ={3},
 year ={2006},
 pages ={204-215},
 ee ={http://dx.doi.org/10.1007/s10009-005-0190-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/concur/CassezDFLL05,
 author ={Franck Cassez and Alexandre David and Emmanuel Fleury and Kim Guldstrand Larsen and Didier Lime},
 title ={Efficient On-the-Fly Algorithms for the Analysis of Timed Games},
 booktitle ={CONCUR},
 year ={2005},
 pages ={66-80},
 ee ={http://dx.doi.org/10.1007/11539452_9},
 crossref ={DBLP:conf/concur/2005},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/concur/2005,
 editor ={Mart\'{\i}n Abadi and Luca de Alfaro},
 title ={CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},
 booktitle ={CONCUR},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={3653},
 year ={2005},
 isbn ={3-540-28309-9},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cata/SchiolerJDL05,
 author ={Henrik Schi{\o}ler and Jan Jakob Jessen and Jens Dalsgaard and Kim Guldstrand Larsen},
 title ={Network Calculus for Real Time Analysis of Embedded Systems with Cyclic Task Dependencies},
 booktitle ={Computers and Their Applications},
 year ={2005},
 pages ={326-332},
 crossref ={DBLP:conf/cata/2005},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cata/2005,
 editor ={Gongzhu Hu},
 title ={20th International Conference on Computers and Their Applications, CATA 2005, March 16-18, 2005, Holiday Inn Downtown-Superdome Hotel, New Orleans, Louisiana, USA, Proceedings},
 booktitle ={Computers and Their Applications},
 publisher ={ISCA},
 year ={2005},
 isbn ={1-880843-54-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/emsoft/LarsenMNS05,
 author ={Kim Guldstrand Larsen and Marius Mikucionis and Brian Nielsen and Arne Skou},
 title ={Testing real-time embedded software using UPPAAL-TRON: an industrial case study},
 booktitle ={EMSOFT},
 year ={2005},
 pages ={299-306},
 ee ={http://doi.acm.org/10.1145/1086228.1086283},
 crossref ={DBLP:conf/emsoft/2005},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/emsoft/2005,
 editor ={Wayne Wolf},
 title ={EMSOFT 2005, September 18-22, 2005, Jersey City, NJ, USA, 5th ACM International Conference On Embedded Software, Proceedings},
 booktitle ={EMSOFT},
 publisher ={ACM},
 year ={2005},
 isbn ={1-59593-091-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fase/LarsenLW05,
 author ={Kim Guldstrand Larsen and Ulrik Larsen and Andrzej Wasowski},
 title ={Color-Blind Specifications for Transformations of Reactive Synchronous Programs},
 booktitle ={FASE},
 year ={2005},
 pages ={160-174},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3442{\&}spage=160},
 crossref ={DBLP:conf/fase/2005},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fase/2005,
 editor ={Maura Cerioli},
 title ={Fundamental Approaches to Software Engineering, 8th International Conference, FASE 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings},
 booktitle ={FASE},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={3442},
 year ={2005},
 isbn ={3-540-25420-X},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/formats/BehrmannLR05,
 author ={Gerd Behrmann and Kim Guldstrand Larsen and Jacob Illum Rasmussen},
 title ={Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness},
 booktitle ={FORMATS},
 year ={2005},
 pages ={81-94},
 ee ={http://dx.doi.org/10.1007/11603009_7},
 crossref ={DBLP:conf/formats/2005},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/formats/2005,
 editor ={Paul Pettersson and Wang Yi},
 title ={Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings},
 booktitle ={FORMATS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={3829},
 year ={2005},
 isbn ={3-540-30946-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fossacs/LarsenR05,
 author ={Kim Guldstrand Larsen and Jacob Illum Rasmussen},
 title ={Optimal Conditional Reachability for Multi-priced Timed Automata},
 booktitle ={FoSSaCS},
 year ={2005},
 pages ={234-249},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3441{\&}spage=234},
 crossref ={DBLP:conf/fossacs/2005},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fossacs/2005,
 editor ={Vladimiro Sassone},
 title ={Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings},
 booktitle ={FoSSaCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={3441},
 year ={2005},
 isbn ={3-540-25388-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/sac/DiazLPCV05,
 author ={Gregorio D\'{\i}az and Kim Guldstrand Larsen and Juan Jos{\'e} Pardo and Fernando Cuartero and Valentin Valero},
 title ={An approach to handle real time and probabilistic behaviors in e-commerce: validating the SET protocol},
 booktitle ={SAC},
 year ={2005},
 pages ={815-820},
 ee ={http://doi.acm.org/10.1145/1066677.1066864},
 crossref ={DBLP:conf/sac/2005},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/sac/2005,
 editor ={Hisham Haddad and Lorie M. Liebrock and Andrea Omicini and Roger L. Wainwright},
 title ={Proceedings of the 2005 ACM Symposium on Applied Computing (SAC), Santa Fe, New Mexico, USA, March 13-17, 2005},
 booktitle ={SAC},
 publisher ={ACM},
 year ={2005},
 isbn ={1-58113-964-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/entcs/BouyerCFL05,
 author ={Patricia Bouyer and Franck Cassez and Emmanuel Fleury and Kim Guldstrand Larsen},
 title ={Synthesis of Optimal Strategies Using HyTech},
 journal ={Electr. Notes Theor. Comput. Sci.},
 volume ={119},
 number ={1},
 year ={2005},
 pages ={11-31},
 ee ={http://dx.doi.org/10.1016/j.entcs.2004.07.006},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/sigmetrics/BehrmannLR05,
 author ={Gerd Behrmann and Kim Guldstrand Larsen and Jacob Illum Rasmussen},
 title ={Optimal scheduling using priced timed automata},
 journal ={SIGMETRICS Performance Evaluation Review},
 volume ={32},
 number ={4},
 year ={2005},
 pages ={34-40},
 ee ={http://doi.acm.org/10.1145/1059816.1059823},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/kbse/MikucionisLN04,
 author ={Marius Mikucionis and Kim Guldstrand Larsen and Brian Nielsen},
 title ={T-UPPAAL: Online Model-based Testing of Real-Time Systems},
 booktitle ={ASE},
 year ={2004},
 pages ={396-397},
 ee ={http://csdl.computer.org/comp/proceedings/ase/2004/2131/00/21310396abs.htm},
 crossref ={DBLP:conf/kbse/2004},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/kbse/2004,
 title ={19th IEEE International Conference on Automated Software Engineering (ASE 2004), 20-25 September 2004, Linz, Austria},
 booktitle ={ASE},
 publisher ={IEEE Computer Society},
 year ={2004},
 isbn ={0-7695-2131-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fates/LarsenMN04,
 author ={Kim Guldstrand Larsen and Marius Mikucionis and Brian Nielsen},
 title ={Online Testing of Real-time Systems Using Uppaal},
 booktitle ={FATES},
 year ={2004},
 pages ={79-94},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3395{\&}spage=79},
 crossref ={DBLP:conf/fates/2004},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fates/2004,
 editor ={Jens Grabowski and Brian Nielsen},
 title ={Formal Approaches to Software Testing, 4th International Workshop, FATES 2004, Linz, Austria, September 21, 2004, Revised Selected Papers},
 booktitle ={FATES},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={3395},
 year ={2005},
 isbn ={3-540-25109-X},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fmco/BehrmannLR04,
 author ={Gerd Behrmann and Kim Guldstrand Larsen and Jacob Illum Rasmussen},
 title ={Priced Timed Automata: Algorithms and Applications},
 booktitle ={FMCO},
 year ={2004},
 pages ={162-182},
 ee ={http://dx.doi.org/10.1007/11561163_8},
 crossref ={DBLP:conf/fmco/2004},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fmco/2004,
 editor ={Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever},
 title ={Formal Methods for Components and Objects, Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2 - 5, 2004, Revised Lectures},
 booktitle ={FMCO},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={3657},
 year ={2005},
 isbn ={3-540-29131-8},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fsttcs/BouyerCFL04,
 author ={Patricia Bouyer and Franck Cassez and Emmanuel Fleury and Kim Guldstrand Larsen},
 title ={Optimal Strategies in Priced Timed Game Automata},
 booktitle ={FSTTCS},
 year ={2004},
 pages ={148-160},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3328{\&}spage=148},
 crossref ={DBLP:conf/fsttcs/2004},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fsttcs/2004,
 editor ={Kamal Lodaya and Meena Mahajan},
 title ={FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings},
 booktitle ={FSTTCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={3328},
 year ={2004},
 isbn ={3-540-24058-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/hybrid/BouyerBL04,
 author ={Patricia Bouyer and Ed Brinksma and Kim Guldstrand Larsen},
 title ={Staying Alive as Cheaply as Possible},
 booktitle ={HSCC},
 year ={2004},
 pages ={203-218},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2993{\&}spage=203},
 crossref ={DBLP:conf/hybrid/2004},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/hybrid/2004,
 editor ={Rajeev Alur and George J. Pappas},
 title ={Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings},
 booktitle ={HSCC},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2993},
 year ={2004},
 isbn ={3-540-21259-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/dagstuhl/LarsenMN04,
 author ={Kim Guldstrand Larsen and Marius Mikucionis and Brian Nielsen},
 title ={Online Testing of Real-Time Systems Using UPPAAL: Status and Future Work},
 booktitle ={Perspectives of Model-Based Testing},
 year ={2004},
 ee ={http://drops.dagstuhl.de/opus/volltexte/2005/326},
 crossref ={DBLP:conf/dagstuhl/2004P4371},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/dagstuhl/2004P4371,
 editor ={Ed Brinksma and Wolfgang Grieskamp and Jan Tretmans},
 title ={Perspectives of Model-Based Testing, 5.-10. September 2004},
 booktitle ={Perspectives of Model-Based Testing},
 publisher ={IBFI, Schloss Dagstuhl, Germany},
 series ={Dagstuhl Seminar Proceedings},
 volume ={04371},
 year ={2005},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/sfm/BehrmannDL04,
 author ={Gerd Behrmann and Alexandre David and Kim Guldstrand Larsen},
 title ={A Tutorial on Uppaal},
 booktitle ={SFM},
 year ={2004},
 pages ={200-236},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3185{\&}spage=200},
 crossref ={DBLP:conf/sfm/2004},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/sfm/2004,
 editor ={Marco Bernardo and Flavio Corradini},
 title ={Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures},
 booktitle ={SFM},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={3185},
 year ={2004},
 isbn ={3-540-23068-8},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/RasmussenLS04,
 author ={Jacob Illum Rasmussen and Kim Guldstrand Larsen and K. Subramani},
 title ={Resource-Optimal Scheduling Using Priced Timed Automata},
 booktitle ={TACAS},
 year ={2004},
 pages ={220-235},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2988{\&}spage=220},
 crossref ={DBLP:conf/tacas/2004},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/tacas/2004,
 editor ={Kurt Jensen and Andreas Podelski},
 title ={Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings},
 booktitle ={TACAS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2988},
 year ={2004},
 isbn ={3-540-21299-X},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/BehrmannBLP04,
 author ={Gerd Behrmann and Patricia Bouyer and Kim Guldstrand Larsen and Radek Pel{\'a}nek},
 title ={Lower and Upper Bounds in Zone Based Abstractions of Timed Automata},
 booktitle ={TACAS},
 year ={2004},
 pages ={312-326},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2988{\&}spage=312},
 crossref ={DBLP:conf/tacas/2004},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/formats/2003,
 editor ={Kim Guldstrand Larsen and Peter Niebert},
 title ={Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003. Revised Papers},
 booktitle ={FORMATS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2791},
 year ={2003},
 isbn ={3-540-21671-5},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/BehrmannLP03,
 author ={Gerd Behrmann and Kim Guldstrand Larsen and Radek Pel{\'a}nek},
 title ={To Store or Not to Store},
 booktitle ={CAV},
 year ={2003},
 pages ={433-445},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2725{\&}spage=433},
 crossref ={DBLP:conf/cav/2003},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/2003,
 editor ={Warren A. Hunt Jr. and Fabio Somenzi},
 title ={Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2725},
 year ={2003},
 isbn ={3-540-40524-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/emsoft/Larsen03,
 author ={Kim Guldstrand Larsen},
 title ={Resource-Efficient Scheduling for Real Time Systems},
 booktitle ={EMSOFT},
 year ={2003},
 pages ={16-19},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2855{\&}spage=16},
 crossref ={DBLP:conf/emsoft/2003},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/emsoft/2003,
 editor ={Rajeev Alur and Insup Lee},
 title ={Embedded Software, Third International Conference, EMSOFT 2003, Philadelphia, PA, USA, October 13-15, 2003, Proceedings},
 booktitle ={EMSOFT},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2855},
 year ={2003},
 isbn ={3-540-20223-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fates/HesselLNPS03,
 author ={Anders Hessel and Kim Guldstrand Larsen and Brian Nielsen and Paul Pettersson and Arne Skou},
 title ={Time-Optimal Real-Time Test Case Generation Using Uppaal},
 booktitle ={FATES},
 year ={2003},
 pages ={114-130},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2931{\&}spage=114},
 crossref ={DBLP:conf/fates/2003},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fates/2003,
 editor ={Alexandre Petrenko and Andreas Ulrich},
 title ={Formal Approaches to Software Testing, Third International Workshop on Formal Approaches to Testing of Software, FATES 2003, Montreal, Quebec, Canada, October 6th, 2003},
 booktitle ={FATES},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2931},
 year ={2004},
 isbn ={3-540-20894-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/formats/HesselLNPS03,
 author ={Anders Hessel and Kim Guldstrand Larsen and Brian Nielsen and Paul Pettersson and Arne Skou},
 title ={Time-Optimal Test Cases for Real-Time Systems},
 booktitle ={FORMATS},
 year ={2003},
 pages ={234-245},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2791{\&}spage=234},
 crossref ={DBLP:conf/formats/2003},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/formats/HendriksBLNV03,
 author ={Martijn Hendriks and Gerd Behrmann and Kim Guldstrand Larsen and Peter Niebert and Frits W. Vaandrager},
 title ={Adding Symmetry Reduction to Uppaal},
 booktitle ={FORMATS},
 year ={2003},
 pages ={46-59},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2791{\&}spage=46},
 crossref ={DBLP:conf/formats/2003},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/spin/DavidBLY03,
 author ={Alexandre David and Gerd Behrmann and Kim Guldstrand Larsen and Wang Yi},
 title ={Unification {\&} Sharing in Timed Automata Verification},
 booktitle ={SPIN},
 year ={2003},
 pages ={225-229},
 ee ={http://link.springer.de/link/service/series/0558/bibs/2648/26480225.htm},
 crossref ={DBLP:conf/spin/2003},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/spin/2003,
 editor ={Thomas Ball and Sriram K. Rajamani},
 title ={Model Checking Software, 10th International SPIN Workshop. Portland, OR, USA, May 9-10, 2003, Proceedings},
 booktitle ={SPIN},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2648},
 year ={2003},
 isbn ={3-540-40117-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/BehrmannBFL03,
 author ={Gerd Behrmann and Patricia Bouyer and Emmanuel Fleury and Kim Guldstrand Larsen},
 title ={Static Guard Analysis in Timed Automata Verification},
 booktitle ={TACAS},
 year ={2003},
 pages ={254-277},
 ee ={http://link.springer.de/link/service/series/0558/bibs/2619/26190254.htm},
 crossref ={DBLP:conf/tacas/2003},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/tacas/2003,
 editor ={Hubert Garavel and John Hatcliff},
 title ={Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings},
 booktitle ={TACAS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2619},
 year ={2003},
 isbn ={3-540-00898-5},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/ita/EsikL03,
 author ={Zolt{\'a}n {\'E}sik and Kim Guldstrand Larsen},
 title ={Regular languages definable by Lindstr{\"o}m quantifiers},
 journal ={ITA},
 volume ={37},
 number ={3},
 year ={2003},
 pages ={179-241},
 ee ={http://dx.doi.org/10.1051/ita:2003017},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/rts/LarsenLPY03,
 author ={Kim Guldstrand Larsen and Fredrik Larsson and Paul Pettersson and Wang Yi},
 title ={Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems},
 journal ={Real-Time Systems},
 volume ={25},
 number ={2-3},
 year ={2003},
 pages ={255-275},
 ee ={http://dx.doi.org/10.1023/A:1025132427497},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/AcetoBBL03,
 author ={Luca Aceto and Patricia Bouyer and Augusto Burgue{\~n}o and Kim Guldstrand Larsen},
 title ={The power of reachability testing for timed automata},
 journal ={Theor. Comput. Sci.},
 volume ={300},
 number ={1-3},
 year ={2003},
 pages ={411-475},
 ee ={http://dx.doi.org/10.1016/S0304-3975(02)00334-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/2002,
 editor ={Ed Brinksma and Kim Guldstrand Larsen},
 title ={Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2404},
 year ={2002},
 isbn ={3-540-43997-8},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/unu/DavidBLY02,
 author ={Alexandre David and Gerd Behrmann and Kim Guldstrand Larsen and Wang Yi},
 title ={A Tool Architecture for the Next Generation of Uppaal},
 booktitle ={10th Anniversary Colloquium of UNU/IIST},
 year ={2002},
 pages ={352-366},
 ee ={http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2757{\&}spage=352},
 crossref ={DBLP:conf/unu/2002},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/unu/2002,
 editor ={Bernhard K. Aichernig and T. S. E. Maibaum},
 title ={Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18-20, 2002, Revised Papers},
 booktitle ={10th Anniversary Colloquium of UNU/IIST},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2757},
 year ={2003},
 isbn ={3-540-20527-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/ftrtft/BehrmannBDLPY02,
 author ={Gerd Behrmann and Johan Bengtsson and Alexandre David and Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
 title ={UPPAAL Implementation Secrets},
 booktitle ={FTRTFT},
 year ={2002},
 pages ={3-22},
 ee ={http://link.springer.de/link/service/series/0558/bibs/2469/24690003.htm},
 crossref ={DBLP:conf/ftrtft/2002},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/ftrtft/2002,
 editor ={Werner Damm and Ernst-R{\"u}diger Olderog},
 title ={Formal Techniques in Real-Time and Fault-Tolerant Systems, 7th International Symposium, FTRTFT 2002, Co-sponsored by IFIP WG 2.2, Oldenburg, Germany, September 9-12, 2002, Proceedings},
 booktitle ={FTRTFT},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2469},
 year ={2002},
 isbn ={3-540-44165-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/papm/DArgenioJJL02,
 author ={Pedro R. D'Argenio and Bertrand Jeannet and Henrik Ejersbo Jensen and Kim Guldstrand Larsen},
 title ={Reduction and Refinement Strategies for Probabilistic Analysis},
 booktitle ={PAPM-PROBMIV},
 year ={2002},
 pages ={57-76},
 ee ={http://link.springer.de/link/service/series/0558/bibs/2399/23990057.htm},
 crossref ={DBLP:conf/papm/2002},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/papm/2002,
 editor ={Holger Hermanns and Roberto Segala},
 title ={Process Algebra and Probabilistic Methods, Performance Modeling and Verification, Second Joint International Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002, Proceedings},
 booktitle ={PAPM-PROBMIV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2399},
 year ={2002},
 isbn ={3-540-43913-7},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/entcs/HendriksL02,
 author ={Martijn Hendriks and Kim Guldstrand Larsen},
 title ={Exact Acceleration of Real-Time Model Checking},
 journal ={Electr. Notes Theor. Comput. Sci.},
 volume ={65},
 number ={6},
 year ={2002},
 ee ={http://www.elsevier.com/gej-ng/31/29/23/117/51/show/Products/notes/index.htt\#010},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/fmsd/BehrmannLAHL02,
 author ={Gerd Behrmann and Kim Guldstrand Larsen and Henrik Reif Andersen and Henrik Hulgaard and J{\o}rn Lind-Nielsen},
 title ={Verification of Hierarchical State/Event Systems using Reusability and Compositionality},
 journal ={Formal Methods in System Design},
 volume ={21},
 number ={2},
 year ={2002},
 pages ={225-244},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/jlp/BengtssonGKLLPY02,
 author ={Johan Bengtsson and W. O. David Griffioen and K{\aa}re J. Kristoffersen and Kim Guldstrand Larsen and Fredrik Larsson and Paul Pettersson and Wang Yi},
 title ={Automated verification of an audio-control protocol using UPPAAL},
 journal ={J. Log. Algebr. Program.},
 volume ={52-53},
 year ={2002},
 pages ={163-181},
 ee ={http://dx.doi.org/10.1016/S1567-8326(02)00036-X},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/concur/2001,
 editor ={Kim Guldstrand Larsen and Mogens Nielsen},
 title ={CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings},
 booktitle ={CONCUR},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2154},
 year ={2001},
 isbn ={3-540-42497-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/LarsenBBFHPR01,
 author ={Kim Guldstrand Larsen and Gerd Behrmann and Ed Brinksma and Ansgar Fehnker and Thomas Hune and Paul Pettersson and Judi Romijn},
 title ={As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata},
 booktitle ={CAV},
 year ={2001},
 pages ={493-505},
 ee ={http://link.springer.de/link/service/series/0558/bibs/2102/21020493.htm},
 crossref ={DBLP:conf/cav/2001},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/2001,
 editor ={G{\'e}rard Berry and Hubert Comon and Alain Finkel},
 title ={Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2102},
 year ={2001},
 isbn ={3-540-42345-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/hybrid/BehrmannFHLPRV01,
 author ={Gerd Behrmann and Ansgar Fehnker and Thomas Hune and Kim Guldstrand Larsen and Paul Pettersson and Judi Romijn and Frits W. Vaandrager},
 title ={Minimum-Cost Reachability for Priced Timed Automata},
 booktitle ={HSCC},
 year ={2001},
 pages ={147-161},
 ee ={http://link.springer.de/link/service/series/0558/bibs/2034/20340147.htm},
 crossref ={DBLP:conf/hybrid/2001},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/hybrid/2001,
 editor ={Maria Domenica Di Benedetto and Alberto L. Sangiovanni-Vincentelli},
 title ={Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings},
 booktitle ={HSCC},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2034},
 year ={2001},
 isbn ={3-540-41866-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/papm/DArgenioJJL01,
 author ={Pedro R. D'Argenio and Bertrand Jeannet and Henrik Ejersbo Jensen and Kim Guldstrand Larsen},
 title ={Reachability Analysis of Probabilistic Systems by Successive Refinements},
 booktitle ={PAPM-PROBMIV},
 year ={2001},
 pages ={39-56},
 ee ={http://link.springer.de/link/service/series/0558/bibs/2165/21650039.htm},
 crossref ={DBLP:conf/papm/2001},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/papm/2001,
 editor ={Luca de Alfaro and Stephen Gilmore},
 title ={Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001, Aachen, Germany, September 12-14, 2001, Proceedings},
 booktitle ={PAPM-PROBMIV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2165},
 year ={2001},
 isbn ={3-540-42556-X},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/fmsd/Lind-NielsenAHBKL01,
 author ={J{\o}rn Lind-Nielsen and Henrik Reif Andersen and Henrik Hulgaard and Gerd Behrmann and K{\aa}re J. Kristoffersen and Kim Guldstrand Larsen},
 title ={Verification of Large State/Event Systems Using Compositionality and Dependency Analysis},
 journal ={Formal Methods in System Design},
 volume ={18},
 number ={1},
 year ={2001},
 pages ={5-23},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/njc/HuneLP01,
 author ={Thomas Hune and Kim Guldstrand Larsen and Paul Pettersson},
 title ={Guided Synthesis of Control Programs Using UPPAAL},
 journal ={Nord. J. Comput.},
 volume ={8},
 number ={1},
 year ={2001},
 pages ={43-64},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/concur/CassezL00,
 author ={Franck Cassez and Kim Guldstrand Larsen},
 title ={The Impressive Power of Stopwatches},
 booktitle ={CONCUR},
 year ={2000},
 pages ={138-152},
 ee ={http://link.springer.de/link/service/series/0558/bibs/1877/18770138.htm},
 crossref ={DBLP:conf/concur/2000},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/concur/2000,
 editor ={Catuscia Palamidessi},
 title ={CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings},
 booktitle ={CONCUR},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1877},
 year ={2000},
 isbn ={3-540-67897-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/ecrts/IversenKLLMMPT00,
 author ={Torsten K. Iversen and K{\aa}re J. Kristoffersen and Kim Guldstrand Larsen and Morten Laursen and Rune G. Madsen and Steffen K. Mortensen and Paul Pettersson and Chris B. Thomasen},
 title ={Model-checking real-time control programs: verifying Lego(R) Mindstorms$^{\mbox{TM}}$ systems using UPPAAL},
 booktitle ={ECRTS},
 year ={2000},
 pages ={147-155},
 ee ={http://dx.doi.org/10.1109/EMRTS.2000.854002},
 crossref ={DBLP:conf/ecrts/2000},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/ecrts/2000,
 title ={12th Euromicro Conference on Real-Time Systems (ECRTS 2000), 19-21 June 2000, Stockholm, Sweden, Proceedings},
 booktitle ={ECRTS},
 publisher ={IEEE Computer Society},
 year ={2000},
 isbn ={0-7695-0734-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/ftrtft/JensenLS00,
 author ={Henrik Ejersbo Jensen and Kim Guldstrand Larsen and Arne Skou},
 title ={Scaling up Uppaal Automatic Verification of Real-Time Systems Using Compositionality and Abstraction},
 booktitle ={FTRTFT},
 year ={2000},
 pages ={19-30},
 ee ={http://link.springer.de/link/service/series/0558/bibs/1926/19260019.htm},
 crossref ={DBLP:conf/ftrtft/2000},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/ftrtft/2000,
 editor ={Mathai Joseph},
 title ={Formal Techniques in Real-Time and Fault-Tolerant Systems, 6th International Symposium, FTRTFT 2000, Pune, India, September 20-22, 2000, Proceedings},
 booktitle ={FTRTFT},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1926},
 year ={2000},
 isbn ={3-540-41055-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/apn/Larsen00,
 author ={Kim Guldstrand Larsen},
 title ={Verification of Timed and Hybrid Systems},
 booktitle ={ICATPN},
 year ={2000},
 pages ={39-42},
 ee ={http://link.springer.de/link/service/series/0558/bibs/1825/18250039.htm},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/icdcsw/HuneLP00,
 author ={Thomas Hune and Kim Guldstrand Larsen and Paul Pettersson},
 title ={Guided Synthesis of Control Programs Using UPPAAL},
 booktitle ={ICDCS Workshop on Distributed System Validation and Verification},
 year ={2000},
 pages ={E15-E22},
 crossref ={DBLP:conf/icdcsw/2000},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/icdcsw/2000,
 editor ={Ten-Hwang Lai},
 title ={Proceedings of the 2000 ICDCS Workshops, April 10, 2000, Taipei, Taiwan, ROC},
 booktitle ={ICDCS Workshops},
 year ={2000},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/movep/AmnellBBDDFHJLMPWY00,
 author ={Tobias Amnell and Gerd Behrmann and Johan Bengtsson and Pedro R. D'Argenio and Alexandre David and Ansgar Fehnker and Thomas Hune and Bertrand Jeannet and Kim Guldstrand Larsen and M. Oliver M{\"o}ller and Paul Pettersson and Carsten Weise and Wang Yi},
 title ={UPPAAL - Now, Next, and Future},
 booktitle ={MOVEP},
 year ={2000},
 pages ={99-124},
 ee ={http://link.springer.de/link/service/series/0558/bibs/2067/20670099.htm},
 crossref ={DBLP:conf/movep/2000},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/movep/2000,
 editor ={Franck Cassez and Claude Jard and Brigitte Rozoy and Mark Dermot Ryan},
 title ={Modeling and Verification of Parallel Processes, 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000},
 booktitle ={MOVEP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={2067},
 year ={2001},
 isbn ={3-540-42787-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/computer/StaunstrupAHLLBKSLT00,
 author ={J{\o}rgen Staunstrup and Henrik Reif Andersen and Henrik Hulgaard and J{\o}rn Lind-Nielsen and Kim Guldstrand Larsen and Gerd Behrmann and K{\aa}re J. Kristoffersen and Arne Skou and Henrik Leerberg and Niels Bo Theilgaard},
 title ={Practical Verification of Embedded Software},
 journal ={IEEE Computer},
 volume ={33},
 number ={5},
 year ={2000},
 pages ={68-75},
 ee ={http://computer.org/computer/co2000/r5068abs.htm},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/arts/HavelundLS99,
 author ={Klaus Havelund and Kim Guldstrand Larsen and Arne Skou},
 title ={Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL},
 booktitle ={ARTS},
 year ={1999},
 pages ={277-298},
 ee ={http://link.springer.de/link/service/series/0558/bibs/1601/16010277.htm},
 crossref ={DBLP:conf/arts/1999},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/arts/1999,
 editor ={Joost-Pieter Katoen},
 title ={Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, ARTS'99, Bamberg, Germany, May 26-28, 1999. Proceedings},
 booktitle ={ARTS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1601},
 year ={1999},
 isbn ={3-540-66010-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/BehrmannLPWY99,
 author ={Gerd Behrmann and Kim Guldstrand Larsen and Justin Pearson and Carsten Weise and Wang Yi},
 title ={Efficient Timed Reachability Analysis Using Clock Difference Diagrams},
 booktitle ={CAV},
 year ={1999},
 pages ={341-353},
 ee ={http://link.springer.de/link/service/series/0558/bibs/1633/16330341.htm},
 crossref ={DBLP:conf/cav/1999},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/1999,
 editor ={Nicolas Halbwachs and Doron Peled},
 title ={Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1633},
 year ={1999},
 isbn ={3-540-66202-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/BehrmannLAHL99,
 author ={Gerd Behrmann and Kim Guldstrand Larsen and Henrik Reif Andersen and Henrik Hulgaard and J{\o}rn Lind-Nielsen},
 title ={Verification of Hierarchical State/Event Systems Using Reusability and Compositionality},
 booktitle ={TACAS},
 year ={1999},
 pages ={163-177},
 ee ={http://link.springer.de/link/service/series/0558/bibs/1579/15790163.htm},
 crossref ={DBLP:conf/tacas/1999},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/tacas/1999,
 editor ={Rance Cleaveland},
 title ={Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings},
 booktitle ={TACAS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1579},
 year ={1999},
 isbn ={3-540-65703-7},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/njc/LarsenPWY99,
 author ={Kim Guldstrand Larsen and Justin Pearson and Carsten Weise and Wang Yi},
 title ={Clock Difference Diagrams},
 journal ={Nord. J. Comput.},
 volume ={6},
 number ={3},
 year ={1999},
 pages ={271-298},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/icalp/1998,
 editor ={Kim Guldstrand Larsen and Sven Skyum and Glynn Winskel},
 title ={Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings},
 booktitle ={ICALP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1443},
 year ={1998},
 isbn ={3-540-64781-3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/forte/LaroussinieL98,
 author ={Fran\c{c}ois Laroussinie and Kim Guldstrand Larsen},
 title ={CMC: A Tool for Compositional Model-Checking of Real-Time Systems},
 booktitle ={FORTE},
 year ={1998},
 pages ={439-456},
 crossref ={DBLP:conf/forte/1998},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/forte/1998,
 editor ={Stanislaw Budkowski and Ana R. Cavalli and Elie Najm},
 title ={Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE XI / PSTV XVIII'98, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV XVIII), 3-6 November, 1998, Paris, France},
 booktitle ={FORTE},
 publisher ={Kluwer},
 series ={IFIP Conference Proceedings},
 volume ={135},
 year ={1998},
 isbn ={0-412-84760-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fsttcs/AcetoBBL98,
 author ={Luca Aceto and Patricia Bouyer and Augusto Burgue{\~n}o and Kim Guldstrand Larsen},
 title ={The Power of Reachability Testing for Timed Automata},
 booktitle ={FSTTCS},
 year ={1998},
 pages ={245-256},
 crossref ={DBLP:conf/fsttcs/1998},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fsttcs/1998,
 editor ={Vikraman Arvind and Ramaswamy Ramanujam},
 title ={Foundations of Software Technology and Theoretical Computer Science, 18th Conference, Chennai, India, December 17-19, 1998, Proceedings},
 booktitle ={FSTTCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1530},
 year ={1998},
 isbn ={3-540-65384-8},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/Lind-NielsenABHKL98,
 author ={J{\o}rn Lind-Nielsen and Henrik Reif Andersen and Gerd Behrmann and Henrik Hulgaard and K{\aa}re J. Kristoffersen and Kim Guldstrand Larsen},
 title ={Verification of Large State/Event Systems Using Compositionality and Dependency Analysis},
 booktitle ={TACAS},
 year ={1998},
 pages ={201-216},
 ee ={http://link.springer.de/link/service/series/0558/bibs/1384/13840201.htm},
 crossref ={DBLP:conf/tacas/1998},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/tacas/1998,
 editor ={Bernhard Steffen},
 title ={Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings},
 booktitle ={TACAS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1384},
 year ={1998},
 isbn ={3-540-64356-7},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/AcetoBL98,
 author ={Luca Aceto and Augusto Burgue{\~n}o and Kim Guldstrand Larsen},
 title ={Model Checking via Reachability Testing for Timed Automata},
 booktitle ={TACAS},
 year ={1998},
 pages ={263-280},
 ee ={http://link.springer.de/link/service/series/0558/bibs/1384/13840263.htm},
 crossref ={DBLP:conf/tacas/1998},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/LarsenPY97,
 author ={Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
 title ={UPPAAL: Status {\&} Developments},
 booktitle ={CAV},
 year ={1997},
 pages ={456-459},
 crossref ={DBLP:conf/cav/1997},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/1997,
 editor ={Orna Grumberg},
 title ={Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1254},
 year ={1997},
 isbn ={3-540-63166-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/rtss/LarsenLPY97,
 author ={Kim Guldstrand Larsen and Fredrik Larsson and Paul Pettersson and Wang Yi},
 title ={Efficient verification of real-time systems: compact data structure and state-space reduction},
 booktitle ={IEEE Real-Time Systems Symposium},
 year ={1997},
 pages ={14-24},
 ee ={http://computer.org/proceedings/rtss/8268/82680014abs.htm},
 crossref ={DBLP:conf/rtss/1997},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/rtss/1997,
 title ={Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS '97), December 3-5, 1997, San Francisco, CA, USA},
 booktitle ={IEEE Real-Time Systems Symposium},
 publisher ={IEEE Computer Society},
 year ={1997},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/rtss/HavelundSLL97,
 author ={Klaus Havelund and Arne Skou and Kim Guldstrand Larsen and K. Lund},
 title ={Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAA},
 booktitle ={IEEE Real-Time Systems Symposium},
 year ={1997},
 pages ={2-13},
 ee ={http://computer.org/proceedings/rtss/8268/82680002abs.htm},
 crossref ={DBLP:conf/rtss/1997},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tapsoft/KristoffersenLLPY97,
 author ={K{\aa}re J. Kristoffersen and Fran\c{c}ois Laroussinie and Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
 title ={A Compositional Proof of a Real-Time Mutual Exclusion Protocol},
 booktitle ={TAPSOFT},
 year ={1997},
 pages ={565-579},
 crossref ={DBLP:conf/tapsoft/1997},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/tapsoft/1997,
 editor ={Michel Bidoit and Max Dauchet},
 title ={TAPSOFT'97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, April 14-18, 1997, Proceedings},
 booktitle ={TAPSOFT},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1214},
 year ={1997},
 isbn ={3-540-62781-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/iandc/LarsenW97,
 author ={Kim Guldstrand Larsen and Wang Yi},
 title ={Time-abstracted Bisimulation: Implicit Specifications and Decidability},
 journal ={Inf. Comput.},
 volume ={134},
 number ={2},
 year ={1997},
 pages ={75-101},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/sttt/LarsenPY97,
 author ={Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
 title ={UPPAAL in a Nutshell},
 journal ={STTT},
 volume ={1},
 number ={1-2},
 year ={1997},
 pages ={134-152},
 ee ={http://link.springer.de/link/service/journals/10009/bibs/7001001/70010134.htm},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/sttt/LarsenSW97,
 author ={Kim Guldstrand Larsen and Bernhard Steffen and Carsten Weise},
 title ={Continuous Modeling of Real-Time and Hybrid Systems: From Concepts to Tools},
 journal ={STTT},
 volume ={1},
 number ={1-2},
 year ={1997},
 pages ={64-85},
 ee ={http://link.springer.de/link/service/journals/10009/bibs/7001001/70010064.htm},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/BengtssonGKLLPY96,
 author ={Johan Bengtsson and W. O. David Griffioen and K{\aa}re J. Kristoffersen and Kim Guldstrand Larsen and Fredrik Larsson and Paul Pettersson and Wang Yi},
 title ={Verification of an Audio Protocol with Bus Collision Using UPPAAL},
 booktitle ={CAV},
 year ={1996},
 pages ={244-256},
 crossref ={DBLP:conf/cav/1996},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/1996,
 editor ={Rajeev Alur and Thomas A. Henzinger},
 title ={Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1102},
 year ={1996},
 isbn ={3-540-61474-5},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/BengtssonLLPY96,
 author ={Johan Bengtsson and Kim Guldstrand Larsen and Fredrik Larsson and Paul Pettersson and Wang Yi},
 title ={UPPAAL in 1995},
 booktitle ={TACAS},
 year ={1996},
 pages ={431-434},
 crossref ={DBLP:conf/tacas/1996},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/tacas/1996,
 editor ={Tiziana Margaria and Bernhard Steffen},
 title ={Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS '96, Passau, Germany, March 27-29, 1996, Proceedings},
 booktitle ={TACAS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1055},
 year ={1996},
 isbn ={3-540-61042-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/concur/LaroussinieL95,
 author ={Fran\c{c}ois Laroussinie and Kim Guldstrand Larsen},
 title ={Compositional Model Checking of Real Time Systems},
 booktitle ={CONCUR},
 year ={1995},
 pages ={27-41},
 crossref ={DBLP:conf/concur/1995},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/concur/1995,
 editor ={Insup Lee and Scott A. Smolka},
 title ={CONCUR '95: Concurrency Theory, 6th International Conference, Philadelphia, PA, USA, August 21-24, 1995, Proceedings},
 booktitle ={CONCUR},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={962},
 year ={1995},
 isbn ={3-540-60218-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fct/LarsenPY95,
 author ={Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
 title ={Model-Checking for Real-Time Systems},
 booktitle ={FCT},
 year ={1995},
 pages ={62-88},
 crossref ={DBLP:conf/fct/1995},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fct/1995,
 editor ={Horst Reichel},
 title ={Fundamentals of Computation Theory, 10th International Symposium, FCT '95, Dresden, Germany, August 22-25, 1995, Proceedings},
 booktitle ={FCT},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={965},
 year ={1995},
 isbn ={3-540-60249-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/hybrid/BengtssonLLPY95,
 author ={Johan Bengtsson and Kim Guldstrand Larsen and Fredrik Larsson and Paul Pettersson and Wang Yi},
 title ={UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems},
 booktitle ={Hybrid Systems},
 year ={1995},
 pages ={232-243},
 crossref ={DBLP:conf/hybrid/1995},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/hybrid/1995,
 editor ={Rajeev Alur and Thomas A. Henzinger and Eduardo D. Sontag},
 title ={Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA},
 booktitle ={Hybrid Systems},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1066},
 year ={1996},
 isbn ={3-540-61155-X},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/hybrid/LarsenPY95,
 author ={Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
 title ={Diagnostic Model-Checking for Real-Time Systems},
 booktitle ={Hybrid Systems},
 year ={1995},
 pages ={575-586},
 crossref ={DBLP:conf/hybrid/1995},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/hybrid/LarsenSW95,
 author ={Kim Guldstrand Larsen and Bernhard Steffen and Carsten Weise},
 title ={Fischer's Protocol Revisited: A Simple Proof Using Modal Constraints},
 booktitle ={Hybrid Systems},
 year ={1995},
 pages ={604-615},
 crossref ={DBLP:conf/hybrid/1995},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/icalp/AndersenKLN95,
 author ={J{\o}rgen H. Andersen and K{\aa}re J. Kristoffersen and Kim Guldstrand Larsen and Jesper Niedermann},
 title ={Automatic Synthesis of Real Time Systems},
 booktitle ={ICALP},
 year ={1995},
 pages ={535-546},
 crossref ={DBLP:conf/icalp/1995},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/icalp/1995,
 editor ={Zolt{\'a}n F{\"u}l{\"o}p and Ferenc G{\'e}cseg},
 title ={Automata, Languages and Programming, 22nd International Colloquium, ICALP95, Szeged, Hungary, July 10-14, 1995, Proceedings},
 booktitle ={ICALP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={944},
 year ={1995},
 isbn ={3-540-60084-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/rtss/LarsenPY95,
 author ={Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
 title ={Compositional and Symbolic Model-Checking of Real-Time Systems},
 booktitle ={IEEE Real-Time Systems Symposium},
 year ={1995},
 pages ={76-89},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/mfcs/GodskesenL95,
 author ={Jens Chr. Godskesen and Kim Guldstrand Larsen},
 title ={Synthesizing Distinguishing Formulae for Real Time Systems (Extended Abstract)},
 booktitle ={MFCS},
 year ={1995},
 pages ={519-528},
 crossref ={DBLP:conf/mfcs/1995},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/mfcs/1995,
 editor ={Jir\'{\i} Wiedermann and Petr H{\'a}jek},
 title ={Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS'95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings},
 booktitle ={MFCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={969},
 year ={1995},
 isbn ={3-540-60246-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/mfcs/LaroussinieLW95,
 author ={Fran\c{c}ois Laroussinie and Kim Guldstrand Larsen and Carsten Weise},
 title ={From Timed Automata to Logic - and Back},
 booktitle ={MFCS},
 year ={1995},
 pages ={529-539},
 crossref ={DBLP:conf/mfcs/1995},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tacas/LarsenSW95,
 author ={Kim Guldstrand Larsen and Bernhard Steffen and Carsten Weise},
 title ={A Constraint Oriented Proof Methodology Based on Modal Transition Systems},
 booktitle ={TACAS},
 year ={1995},
 pages ={17-40},
 crossref ={DBLP:conf/tacas/1995},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/tacas/1995,
 editor ={Ed Brinksma and Rance Cleaveland and Kim Guldstrand Larsen and Tiziana Margaria and Bernhard Steffen},
 title ={Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS '95, Aarhus, Denmark, May 19-20, 1995, Proceedings},
 booktitle ={TACAS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1019},
 year ={1995},
 isbn ={3-540-60630-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/fmsd/BorjessonLS95,
 author ={Anders B{\o}rjesson and Kim Guldstrand Larsen and Arne Skou},
 title ={Generality in Design and Compositional Verification Using TAV},
 journal ={Formal Methods in System Design},
 volume ={6},
 number ={3},
 year ={1995},
 pages ={239-258},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/njc/GodskesenL95,
 author ={Jens Chr. Godskesen and Kim Guldstrand Larsen},
 title ={Synthesizing Distinguishing Formulae for Real Time Systems},
 journal ={Nord. J. Comput.},
 volume ={2},
 number ={3},
 year ={1995},
 pages ={338-357},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/dagstuhl/LarsenSW94,
 author ={Kim Guldstrand Larsen and Bernhard Steffen and Carsten Weise},
 title ={The Methodology of Modal Constraints},
 booktitle ={Formal Systems Specification},
 year ={1994},
 pages ={405-435},
 crossref ={DBLP:conf/dagstuhl/1994fss},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/dagstuhl/1994fss,
 editor ={Manfred Broy and Stephan Merz and Katharina Spies},
 title ={Formal Systems Specification, The RPC-Memory Specification Case Study (the book grow out of a Dagstuhl Seminar, September 1994)},
 booktitle ={Formal Systems Specification},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={1169},
 year ={1996},
 isbn ={3-540-61984-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/pstv/GodskesenLS94,
 author ={Jens Chr. Godskesen and Kim Guldstrand Larsen and Arne Skou},
 title ={Automatic verification of real-tim systems using epsilon},
 booktitle ={PSTV},
 year ={1994},
 pages ={323-330},
 crossref ={DBLP:conf/pstv/1994},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/pstv/1994,
 editor ={Son T. Vuong and Samuel T. Chanson},
 title ={Protocol Specification, Testing and Verification XIV, Proceedings of the Fourteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Vancouver, BC, Canada, 1994},
 booktitle ={PSTV},
 publisher ={Chapman {\&} Hall},
 series ={IFIP Conference Proceedings},
 volume ={1},
 year ={1995},
 isbn ={0-412-63640-9},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/pstv/HavelundL94,
 author ={Klaus Havelund and Kim Guldstrand Larsen},
 title ={A refinement logic for the fork calculus},
 booktitle ={PSTV},
 year ={1994},
 pages ={5-20},
 crossref ={DBLP:conf/pstv/1994},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/njc/HavelundL94,
 author ={Klaus Havelund and Kim Guldstrand Larsen},
 title ={The Fork Calculus},
 journal ={Nord. J. Comput.},
 volume ={1},
 number ={3},
 year ={1994},
 pages ={346-363},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/CeransGL93,
 author ={Karlis Cerans and Jens Chr. Godskesen and Kim Guldstrand Larsen},
 title ={Timed Modal Specification - Theory and Tools},
 booktitle ={CAV},
 year ={1993},
 pages ={253-267},
 crossref ={DBLP:conf/cav/1993},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/1993,
 editor ={Costas Courcoubetis},
 title ={Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={697},
 year ={1993},
 isbn ={3-540-56922-7},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/concur/JensenLJL93,
 author ={Ole H{\o}gh Jensen and Jarl Tuxen Lang and Christian Jeppesen and Kim Guldstrand Larsen},
 title ={Model Construction for Implicit Specifications in Model Logic},
 booktitle ={CONCUR},
 year ={1993},
 pages ={247-261},
 crossref ={DBLP:conf/concur/1993},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/concur/1993,
 editor ={Eike Best},
 title ={CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings},
 booktitle ={CONCUR},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={715},
 year ={1993},
 isbn ={3-540-57208-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/icalp/HavelundL93,
 author ={Klaus Havelund and Kim Guldstrand Larsen},
 title ={The Fork Calculus},
 booktitle ={ICALP},
 year ={1993},
 pages ={544-557},
 crossref ={DBLP:conf/icalp/1993},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/icalp/1993,
 editor ={Andrzej Lingas and Rolf G. Karlsson and Svante Carlsson},
 title ={Automata, Languages and Programming, 20nd International Colloquium, ICALP93, Lund, Sweden, July 5-9, 1993, Proceedings},
 booktitle ={ICALP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={700},
 year ={1993},
 isbn ={3-540-56939-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/mfps/LarsenY93,
 author ={Kim Guldstrand Larsen and Wang Yi},
 title ={Time Abstracted Bisimiulation: Implicit Specifications and Decidability},
 booktitle ={MFPS},
 year ={1993},
 pages ={160-176},
 crossref ={DBLP:conf/mfps/1993},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/mfps/1993,
 editor ={Stephen D. Brookes and Michael G. Main and Austin Melton and Michael W. Mislove and David A. Schmidt},
 title ={Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings},
 booktitle ={MFPS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={802},
 year ={1994},
 isbn ={3-540-58027-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/Larsen93,
 author ={Kim Guldstrand Larsen},
 title ={The Expressive Power of Implicit Specifications},
 journal ={Theor. Comput. Sci.},
 volume ={114},
 number ={1},
 year ={1993},
 pages ={119-147},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/1991,
 editor ={Kim Guldstrand Larsen and Arne Skou},
 title ={Computer Aided Verification, 3rd International Workshop, CAV '91, Aalborg, Denmark, July, 1-4, 1991, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={575},
 year ={1992},
 isbn ={3-540-55179-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/Larsen92,
 author ={Kim Guldstrand Larsen},
 title ={Efficient Local Correctness Checking},
 booktitle ={CAV},
 year ={1992},
 pages ={30-43},
 crossref ={DBLP:conf/cav/1992},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/cav/1992,
 editor ={Gregor von Bochmann and David K. Probst},
 title ={Computer Aided Verification, Fourth International Workshop, CAV '92, Montreal, Canada, June 29 - July 1, 1992, Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={663},
 year ={1993},
 isbn ={3-540-56496-9},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/concur/LarsenS92,
 author ={Kim Guldstrand Larsen and Arne Skou},
 title ={Compositional Verification of Probabilistic Processes},
 booktitle ={CONCUR},
 year ={1992},
 pages ={456-471},
 crossref ={DBLP:conf/concur/1992},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/concur/1992,
 editor ={Rance Cleaveland},
 title ={CONCUR '92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings},
 booktitle ={CONCUR},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={630},
 year ={1992},
 isbn ={3-540-55822-5},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/forte/BorjessonLS92,
 author ={Anders B{\o}rjesson and Kim Guldstrand Larsen and Arne Skou},
 title ={Generality in design and compositional verification using TAV},
 booktitle ={FORTE},
 year ={1992},
 pages ={449-464},
 crossref ={DBLP:conf/forte/1992},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/forte/1992,
 editor ={Michel Diaz and Roland Groz},
 title ={Formal Description Techniques, V, Proceedings of the IFIP TC6/WG6.1 Fifth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, FORTE '92, Perros-Guirec, France, 13-16 October 1992},
 booktitle ={FORTE},
 publisher ={North-Holland},
 series ={IFIP Transactions},
 volume ={C-10},
 year ={1993},
 isbn ={0-444-89282-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fsttcs/GodskesenL92,
 author ={Jens Chr. Godskesen and Kim Guldstrand Larsen},
 title ={Real-Time Calculi and Expansion Theorems},
 booktitle ={FSTTCS},
 year ={1992},
 pages ={302-315},
 crossref ={DBLP:conf/fsttcs/1992},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fsttcs/1992,
 editor ={R. K. Shyamasundar},
 title ={Foundations of Software Technology and Theoretical Computer Science, 12th Conference, New Delhi, India, December 18-20, 1992, Proceedings},
 booktitle ={FSTTCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={652},
 year ={1992},
 isbn ={3-540-56287-7},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/napaw/GodskesenL92,
 author ={Jens Chr. Godskesen and Kim Guldstrand Larsen},
 title ={Real-Time Calculi and Expansion Theorems},
 booktitle ={NAPAW},
 year ={1992},
 pages ={3-12},
 crossref ={DBLP:conf/napaw/1992},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/napaw/1992,
 editor ={S. Purushothaman and Amy E. Zwarico},
 title ={NAPAW 92, Proceedings of the First North American Process Algebra Workshop, Stony Brook, New York, USA, 28 Agust 1992},
 booktitle ={NAPAW},
 publisher ={Springer},
 series ={Workshops in Computing},
 year ={1993},
 isbn ={3-540-19822-9},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/pstv/YiL92,
 author ={Wang Yi and Kim Guldstrand Larsen},
 title ={Testing Probabilistic and Nondeterministic Processes},
 booktitle ={PSTV},
 year ={1992},
 pages ={47-61},
 crossref ={DBLP:conf/pstv/1992},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/pstv/1992,
 editor ={Richard J. Linn Jr. and M. {\"U}mit Uyar},
 title ={Protocol Specification, Testing and Verification XII, Proceedings of the IFIP TC6/WG6.1 Twelth International Symposium on Protocol Specification, Testing and Verification, Lake Buena Vista, Florida, USA, 22-25 June 1992},
 booktitle ={PSTV},
 publisher ={North-Holland},
 series ={IFIP Transactions},
 volume ={C-8},
 year ={1992},
 isbn ={0-444-89874-3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/iandc/LarsenM92,
 author ={Kim Guldstrand Larsen and Robin Milner},
 title ={A Compositional Protocol Verification Using Relativized Bisimulation},
 journal ={Inf. Comput.},
 volume ={99},
 number ={1},
 year ={1992},
 pages ={80-108},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/BoudolL92,
 author ={G{\'e}rard Boudol and Kim Guldstrand Larsen},
 title ={Graphical Versus Logical Specifications},
 journal ={Theor. Comput. Sci.},
 volume ={106},
 number ={1},
 year ={1992},
 pages ={3-20},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/HolmerLY91,
 author ={Uno Holmer and Kim Guldstrand Larsen and Wang Yi},
 title ={Deciding Properties of Regular Real Time Processes},
 booktitle ={CAV},
 year ={1991},
 pages ={443-453},
 crossref ={DBLP:conf/cav/1991},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/icalp/Larsen91,
 author ={Kim Guldstrand Larsen},
 title ={The Expressive Power of Implicit Specifications},
 booktitle ={ICALP},
 year ={1991},
 pages ={204-216},
 crossref ={DBLP:conf/icalp/1991},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/icalp/1991,
 editor ={Javier Leach Albert and Burkhard Monien and Mario Rodr\'{\i}guez-Artalejo},
 title ={Automata, Languages and Programming, 18th International Colloquium, ICALP91, Madrid, Spain, July 8-12, 1991, Proceedings},
 booktitle ={ICALP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={510},
 year ={1991},
 isbn ={3-540-54233-7},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/lics/JonssonL91,
 author ={Bengt Jonsson and Kim Guldstrand Larsen},
 title ={Specification and Refinement of Probabilistic Processes},
 booktitle ={LICS},
 year ={1991},
 pages ={266-277},
 crossref ={DBLP:conf/lics/LICS6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/lics/LICS6,
 title ={Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, 15-18 July, 1991, Amsterdam, The Netherlands},
 booktitle ={LICS},
 publisher ={IEEE Computer Society},
 year ={1991},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/tapsoft/JonssonL91,
 author ={Bengt Jonsson and Kim Guldstrand Larsen},
 title ={On the Complexity of Equation Solving in Process Algebra},
 booktitle ={TAPSOFT, Vol.1},
 year ={1991},
 pages ={381-396},
 crossref ={DBLP:conf/tapsoft/1991-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/tapsoft/1991-1,
 editor ={Samson Abramsky and T. S. E. Maibaum},
 title ={TAPSOFT'91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP'91)},
 booktitle ={TAPSOFT, Vol.1},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={493},
 year ={1991},
 isbn ={3-540-53982-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/iandc/LarsenW91,
 author ={Kim Guldstrand Larsen and Glynn Winskel},
 title ={Using Information Systems to Solve Recursive Domain Equations},
 journal ={Inf. Comput.},
 volume ={91},
 number ={2},
 year ={1991},
 pages ={232-258},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/iandc/LarsenS91,
 author ={Kim Guldstrand Larsen and Arne Skou},
 title ={Bisimulation through Probabilistic Testing},
 journal ={Inf. Comput.},
 volume ={94},
 number ={1},
 year ={1991},
 pages ={1-28},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/logcom/LarsenX91,
 author ={Kim Guldstrand Larsen and Liu Xinxin},
 title ={Compositionality through an Operational Semantics of Contexts},
 journal ={J. Log. Comput.},
 volume ={1},
 number ={6},
 year ={1991},
 pages ={761-795},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/LarsenT91,
 author ={Kim Guldstrand Larsen and Bent Thomsen},
 title ={Partial Specifications and Compositional Verification},
 journal ={Theor. Comput. Sci.},
 volume ={88},
 number ={1},
 year ={1991},
 pages ={15-32},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/caap/BoudolL90,
 author ={G{\'e}rard Boudol and Kim Guldstrand Larsen},
 title ={Graphical versus Logical Specifications},
 booktitle ={CAAP},
 year ={1990},
 pages ={57-71},
 crossref ={DBLP:conf/caap/1990},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/caap/1990,
 editor ={Andr{\'e} Arnold},
 title ={CAAP '90, 15th Colloquium on Trees in Algebra and Programming, Copenhagen, Denmark, May 15-18, 1990, Proceedings},
 booktitle ={CAAP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={431},
 year ={1990},
 isbn ={3-540-52590-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/concur/Larsen90,
 author ={Kim Guldstrand Larsen},
 title ={Ideal Specification Formalism + Expressivity + Compositionality + Decidability + Testability + ..},
 booktitle ={CONCUR},
 year ={1990},
 pages ={33-56},
 crossref ={DBLP:conf/concur/1990},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/concur/1990,
 editor ={Jos C. M. Baeten and Jan Willem Klop},
 title ={CONCUR '90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings},
 booktitle ={CONCUR},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={458},
 year ={1990},
 isbn ={3-540-53048-7},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/icalp/LarsenX90,
 author ={Kim Guldstrand Larsen and Liu Xinxin},
 title ={Compositionality Through an Operational Semantics of Contexts},
 booktitle ={ICALP},
 year ={1990},
 pages ={526-539},
 crossref ={DBLP:conf/icalp/1990},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/icalp/1990,
 editor ={Mike Paterson},
 title ={Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, July 16-20, 1990, Proceedings},
 booktitle ={ICALP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={443},
 year ={1990},
 isbn ={3-540-52826-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/lics/LarsenX90,
 author ={Kim Guldstrand Larsen and Liu Xinxin},
 title ={Equation Solving Using Modal Transition Systems},
 booktitle ={LICS},
 year ={1990},
 pages ={108-117},
 crossref ={DBLP:conf/lics/LICS5},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/lics/LICS5,
 title ={Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, 4-7 June 1990, Philadelphia, Pennsylvania, USA},
 booktitle ={LICS},
 publisher ={IEEE Computer Society},
 year ={1990},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/Larsen90,
 author ={Kim Guldstrand Larsen},
 title ={Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion},
 journal ={Theor. Comput. Sci.},
 volume ={72},
 number ={2{\&}3},
 year ={1990},
 pages ={265-288},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/avmfss/Larsen89,
 author ={Kim Guldstrand Larsen},
 title ={Modal Specifications},
 booktitle ={Automatic Verification Methods for Finite State Systems},
 year ={1989},
 pages ={232-246},
 crossref ={DBLP:conf/avmfss/1989},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/avmfss/1989,
 editor ={Joseph Sifakis},
 title ={Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings},
 booktitle ={Automatic Verification Methods for Finite State Systems},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={407},
 year ={1990},
 isbn ={3-540-52148-8},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/ershov/HuttelL89,
 author ={Hans H{\"u}ttel and Kim Guldstrand Larsen},
 title ={The Use of Static Constructs in A Modal Process Logic},
 booktitle ={Logic at Botik},
 year ={1989},
 pages ={163-180},
 crossref ={DBLP:conf/ershov/1989},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/ershov/1989,
 editor ={Albert R. Meyer and Michael A. Taitslin},
 title ={Logic at Botik '89, Symposium on Logical Foundations of Computer Science, Pereslav-Zalessky, USSR, July 3-8, 1989, Proceedings},
 booktitle ={Logic at Botik},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={363},
 year ={1989},
 isbn ={3-540-51237-3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/popl/LarsenS89,
 author ={Kim Guldstrand Larsen and Arne Skou},
 title ={Bisimulation Through Probabilistic Testing},
 booktitle ={POPL},
 year ={1989},
 pages ={344-352},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/rex/Larsen89,
 author ={Kim Guldstrand Larsen},
 title ={Compositional Theories Based on an Operational Semantics of Contexts},
 booktitle ={REX Workshop},
 year ={1989},
 pages ={487-518},
 crossref ={DBLP:conf/rex/1989},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/rex/1989,
 editor ={J. W. de Bakker and Willem P. de Roever and Grzegorz Rozenberg},
 title ={Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands, May 29 - June 2, 1989, Proceedings},
 booktitle ={REX Workshop},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={430},
 year ={1990},
 isbn ={3-540-52559-9},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/caap/Larsen88,
 author ={Kim Guldstrand Larsen},
 title ={Proof System for Hennessy-Milner Logic with Recursion},
 booktitle ={CAAP},
 year ={1988},
 pages ={215-230},
 crossref ={DBLP:conf/caap/1988},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/caap/1988,
 editor ={Max Dauchet and Maurice Nivat},
 title ={CAAP '88, 13th Colloquium on Trees in Algebra and Programming, Nancy, France, March 21-24, 1988, Proceedings},
 booktitle ={CAAP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={299},
 year ={1988},
 isbn ={3-540-19021-X},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/lics/LarsenT88,
 author ={Kim Guldstrand Larsen and Bent Thomsen},
 title ={A Modal Process Logic},
 booktitle ={LICS},
 year ={1988},
 pages ={203-210},
 crossref ={DBLP:conf/lics/LICS3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/lics/LICS3,
 title ={Proceedings, Third Annual Symposium on Logic in Computer Science, 5-8 July 1988, Edinburgh, Scotland, UK},
 booktitle ={LICS},
 publisher ={IEEE Computer Society},
 year ={1988},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/mfcs/LarsenT88,
 author ={Kim Guldstrand Larsen and Bent Thomsen},
 title ={Compositional Proofs by Partial Specification of Processes},
 booktitle ={MFCS},
 year ={1988},
 pages ={414-423},
 crossref ={DBLP:conf/mfcs/1988},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/mfcs/1988,
 editor ={Michal Chytil and Ladislav Janiga and V{\'a}clav Koubek},
 title ={Mathematical Foundations of Computer Science 1988, MFCS'88, Carlsbad, Czechoslovakia, August 29 - September 2, 1988, Proceedings},
 booktitle ={MFCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={324},
 year ={1988},
 isbn ={3-540-50110-X},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/icalp/LarsenM87,
 author ={Kim Guldstrand Larsen and Robin Milner},
 title ={Verifying a Protocol Using Relativized Bisimulation},
 booktitle ={ICALP},
 year ={1987},
 pages ={126-135},
 crossref ={DBLP:conf/icalp/1987},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/icalp/1987,
 editor ={Thomas Ottmann},
 title ={Automata, Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987, Proceedings},
 booktitle ={ICALP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={267},
 year ={1987},
 isbn ={3-540-18088-5},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/Larsen87,
 author ={Kim Guldstrand Larsen},
 title ={A Context Dependent Equivalence Between Processes},
 journal ={Theor. Comput. Sci.},
 volume ={49},
 year ={1987},
 pages ={184-215},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/JensenL87,
 author ={Finn Verner Jensen and Kim Guldstrand Larsen},
 title ={Recursively Defined Doains and their Induction Principles},
 journal ={Theor. Comput. Sci.},
 volume ={54},
 year ={1987},
 pages ={29-51},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/fsttcs/JensenL85,
 author ={Finn Verner Jensen and Kim Guldstrand Larsen},
 title ={Recursively Defined Domains and Their Induction Principles},
 booktitle ={FSTTCS},
 year ={1985},
 pages ={225-245},
 crossref ={DBLP:conf/fsttcs/1985},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/fsttcs/1985,
 editor ={S. N. Maheshwari},
 title ={Foundations of Software Technology and Theoretical Computer Science, Fifth Conference, New Delhi, India, December 16-18, 1985, Proceedings},
 booktitle ={FSTTCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={206},
 year ={1985},
 isbn ={3-540-16042-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/icalp/Larsen85,
 author ={Kim Guldstrand Larsen},
 title ={A Context Dependent Equivalence between Processes},
 booktitle ={ICALP},
 year ={1985},
 pages ={373-382},
 crossref ={DBLP:conf/icalp/1985},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/icalp/1985,
 editor ={Wilfried Brauer},
 title ={Automata, Languages and Programming, 12th Colloquium, Nafplion, Greece, July 15-19, 1985, Proceedings},
 booktitle ={ICALP},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={194},
 year ={1985},
 isbn ={3-540-15650-X},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/sdt/WinskelL84,
 author ={Glynn Winskel and Kim Guldstrand Larsen},
 title ={Using Information Systems to Solve Recursive Domain Equations Effectively},
 booktitle ={Semantics of Data Types},
 year ={1984},
 pages ={109-129},
 crossref ={DBLP:conf/sdt/1984},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/sdt/1984,
 editor ={Gilles Kahn and David B. MacQueen and Gordon D. Plotkin},
 title ={Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings},
 booktitle ={Semantics of Data Types},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={173},
 year ={1984},
 isbn ={3-540-13346-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/atva/BenesKLMS11,
 author ={Nikola Benes and Jan Kret\'{\i}nsk{\'y} and Kim G. Larsen and Mikael H. M{\o}ller and Jir\'{\i} Srba},
 title ={Parametric Modal Transition Systems},
 booktitle ={ATVA},
 year ={2011},
 pages ={275-289},
 ee ={http://dx.doi.org/10.1007/978-3-642-24372-1_20},
 crossref ={DBLP:conf/atva/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/atva/2011,
 editor ={Tevfik Bultan and Pao-Ann Hsiung},
 title ={Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings},
 booktitle ={ATVA},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6996},
 year ={2011},
 isbn ={978-3-642-24371-4},
 ee ={http://dx.doi.org/10.1007/978-3-642-24372-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/cav/DavidLLMW11,
 author ={Alexandre David and Kim G. Larsen and Axel Legay and Marius Mikucionis and Zheng Wang},
 title ={Time for Statistical Model Checking of Real-Time Systems},
 booktitle ={CAV},
 year ={2011},
 pages ={349-355},
 ee ={http://dx.doi.org/10.1007/978-3-642-22110-1_27},
 crossref ={DBLP:conf/cav/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={CAV11.pdf},
}

@proceedings{DBLP:conf/cav/2011,
 editor ={Ganesh Gopalakrishnan and Shaz Qadeer},
 title ={Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
 booktitle ={CAV},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6806},
 year ={2011},
 isbn ={978-3-642-22109-5},
 ee ={http://dx.doi.org/10.1007/978-3-642-22110-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/concur/BouyerLMST11,
 author ={Patricia Bouyer and Kim G. Larsen and Nicolas Markey and Ocan Sankur and Claus R. Thrane},
 title ={Timed Automata Can Always Be Made Implementable},
 booktitle ={CONCUR},
 year ={2011},
 pages ={76-91},
 ee ={http://dx.doi.org/10.1007/978-3-642-23217-6_6},
 crossref ={DBLP:conf/concur/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/concur/2011,
 editor ={Joost-Pieter Katoen and Barbara K{\"o}nig},
 title ={CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings},
 booktitle ={CONCUR},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6901},
 year ={2011},
 isbn ={978-3-642-23216-9},
 ee ={http://dx.doi.org/10.1007/978-3-642-23217-6},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/csl/CardelliLM11,
 author ={Luca Cardelli and Kim G. Larsen and Radu Mardare},
 title ={Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas},
 booktitle ={CSL},
 year ={2011},
 pages ={144-158},
 ee ={http://dx.doi.org/10.4230/LIPIcs.CSL.2011.144},
 crossref ={DBLP:conf/csl/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/csl/2011,
 editor ={Marc Bezem},
 title ={Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings},
 booktitle ={CSL},
 publisher ={Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
 series ={LIPIcs},
 volume ={12},
 year ={2011},
 isbn ={978-3-939897-32-3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/formats/LarsenLTW11,
 author ={Kim G. Larsen and Axel Legay and Louis-Marie Traonouez and Andrzej Wasowski},
 title ={Robust Specification of Real Time Components},
 booktitle ={FORMATS},
 year ={2011},
 pages ={129-144},
 ee ={http://dx.doi.org/10.1007/978-3-642-24310-3_10},
 crossref ={DBLP:conf/formats/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/formats/2011,
 editor ={Uli Fahrenberg and Stavros Tripakis},
 title ={Formal Modeling and Analysis of Timed Systems - 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings},
 booktitle ={FORMATS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6919},
 year ={2011},
 isbn ={978-3-642-24309-7},
 ee ={http://dx.doi.org/10.1007/978-3-642-24310-3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/formats/DavidLLMPVW11,
 author ={Alexandre David and Kim G. Larsen and Axel Legay and Marius Mikucionis and Danny B{\o}gsted Poulsen and Jonas van Vliet and Zheng Wang},
 title ={Statistical Model Checking for Networks of Priced Timed Automata},
 booktitle ={FORMATS},
 year ={2011},
 pages ={80-96},
 ee ={http://dx.doi.org/10.1007/978-3-642-24310-3_7},
 crossref ={DBLP:conf/formats/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
 pdf ={formats11.pdf},
}

@proceedings{DBLP:conf/formats/2011,
 editor ={Uli Fahrenberg and Stavros Tripakis},
 title ={Formal Modeling and Analysis of Timed Systems - 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings},
 booktitle ={FORMATS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6919},
 year ={2011},
 isbn ={978-3-642-24309-7},
 ee ={http://dx.doi.org/10.1007/978-3-642-24310-3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/icalp/CardelliLM11,
 author ={Luca Cardelli and Kim G. Larsen and Radu Mardare},
 title ={Modular Markovian Logic},
 booktitle ={ICALP (2)},
 year ={2011},
 pages ={380-391},
 ee ={http://dx.doi.org/10.1007/978-3-642-22012-8_30},
 crossref ={DBLP:conf/icalp/2011-2},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/icalp/2011-2,
 editor ={Luca Aceto and Monika Henzinger and Jiri Sgall},
 title ={Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II},
 booktitle ={ICALP (2)},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6756},
 year ={2011},
 isbn ={978-3-642-22011-1},
 ee ={http://dx.doi.org/10.1007/978-3-642-22012-8},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/ictac/FahrenbergJLS11,
 author ={Uli Fahrenberg and Line Juhl and Kim G. Larsen and Jir\'{\i} Srba},
 title ={Energy Games in Multiweighted Automata},
 booktitle ={ICTAC},
 year ={2011},
 pages ={95-115},
 ee ={http://dx.doi.org/10.1007/978-3-642-23283-1_9},
 crossref ={DBLP:conf/ictac/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/ictac/2011,
 editor ={Antonio Cerone and Pekka Pihlajasaari},
 title ={Theoretical Aspects of Computing - ICTAC 2011 - 8th International Colloquium, Johannesburg, South Africa, August 31 - September 2, 2011. Proceedings},
 booktitle ={ICTAC},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6916},
 year ={2011},
 isbn ={978-3-642-23282-4},
 ee ={http://dx.doi.org/10.1007/978-3-642-23283-1},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/lata/DelahayeLLPW11,
 author ={Benoit Delahaye and Kim G. Larsen and Axel Legay and Mikkel L. Pedersen and Andrzej Wasowski},
 title ={Decision Problems for Interval Markov Chains},
 booktitle ={LATA},
 year ={2011},
 pages ={274-285},
 ee ={http://dx.doi.org/10.1007/978-3-642-21254-3_21},
 crossref ={DBLP:conf/lata/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/lata/2011,
 editor ={Adrian Horia Dediu and Shunsuke Inenaga and Carlos Mart\'{\i}n-Vide},
 title ={Language and Automata Theory and Applications - 5th International Conference, LATA 2011, Tarragona, Spain, May 26-31, 2011. Proceedings},
 booktitle ={LATA},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6638},
 year ={2011},
 isbn ={978-3-642-21253-6},
 ee ={http://dx.doi.org/10.1007/978-3-642-21254-3},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/mfcs/BauerFJLLT11,
 author ={Sebastian S. Bauer and Uli Fahrenberg and Line Juhl and Kim G. Larsen and Axel Legay and Claus R. Thrane},
 title ={Quantitative Refinement for Weighted Modal Transition Systems},
 booktitle ={MFCS},
 year ={2011},
 pages ={60-71},
 ee ={http://dx.doi.org/10.1007/978-3-642-22993-0_9},
 crossref ={DBLP:conf/mfcs/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/mfcs/2011,
 editor ={Filip Murlak and Piotr Sankowski},
 title ={Mathematical Foundations of Computer Science 2011 - 36th International Symposium, MFCS 2011, Warsaw, Poland, August 22-26, 2011. Proceedings},
 booktitle ={MFCS},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6907},
 year ={2011},
 isbn ={978-3-642-22992-3},
 ee ={http://dx.doi.org/10.1007/978-3-642-22993-0},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/nfm/DalsgaardHJLOOS11,
 author ={Andreas Engelbredt Dalsgaard and Ren{\'e} Rydhof Hansen and Kenneth Yrke J{\o}rgensen and Kim Guldstrand Larsen and Mads Chr. Olesen and Petur Olsen and Jir\'{\i} Srba},
 title ={opaal: A Lattice Model Checker},
 booktitle ={NASA Formal Methods},
 year ={2011},
 pages ={487-493},
 ee ={http://dx.doi.org/10.1007/978-3-642-20398-5_37},
 crossref ={DBLP:conf/nfm/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/nfm/2011,
 editor ={Mihaela Gheorghiu Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi},
 title ={NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings},
 booktitle ={NASA Formal Methods},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6617},
 year ={2011},
 isbn ={978-3-642-20397-8},
 ee ={http://dx.doi.org/10.1007/978-3-642-20398-5},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:journals/corr/abs-1111-0370,
 author ={Peter E. Bulychev and Alexandre David and Kim Guldstrand Larsen and Marius Mikucionis and Axel Legay},
 title ={Distributed Parametric and Statistical Model Checking},
 booktitle ={PDMC},
 year ={2011},
 pages ={30-42},
 ee ={http://dx.doi.org/10.4204/EPTCS.72.4},
 crossref ={DBLP:journals/corr/abs-1111-0064},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:journals/corr/abs-1111-0064,
 editor ={Jiri Barnat and Keijo Heljanko},
 title ={Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation},
 booktitle ={PDMC},
 series ={EPTCS},
 volume ={72},
 year ={2011},
 ee ={http://dx.doi.org/10.4204/EPTCS.72},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:journals/corr/abs-1107-1205,
 author ={Uli Fahrenberg and Claus R. Thrane and Kim G. Larsen},
 title ={Distances for Weighted Transition Systems: Games and Properties},
 booktitle ={QAPL},
 year ={2011},
 pages ={134-147},
 ee ={http://dx.doi.org/10.4204/EPTCS.57.10},
 crossref ={DBLP:journals/corr/abs-1107-0746},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:journals/corr/abs-1107-0746,
 editor ={Mieke Massink and Gethin Norman},
 title ={Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages},
 booktitle ={QAPL},
 series ={EPTCS},
 volume ={57},
 year ={2011},
 ee ={http://dx.doi.org/10.4204/EPTCS.57},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/qest/MaoCJNLN11,
 author ={Hua Mao and Yingke Chen and Manfred Jaeger and Thomas D. Nielsen and Kim G. Larsen and Brian Nielsen},
 title ={Learning Probabilistic Automata for Model Checking},
 booktitle ={QEST},
 year ={2011},
 pages ={111-120},
 ee ={http://doi.ieeecomputersociety.org/10.1109/QEST.2011.21},
 crossref ={DBLP:conf/qest/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/qest/2011,
 title ={Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 September, 2011},
 booktitle ={QEST},
 publisher ={IEEE Computer Society},
 year ={2011},
 isbn ={978-1-4577-0973-9},
 ee ={http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6041098},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/qest/DelahayeLLPW11,
 author ={Benoit Delahaye and Kim G. Larsen and Axel Legay and Mikkel L. Pedersen and Andrzej Wasowski},
 title ={APAC: A Tool for Reasoning about Abstract Probabilistic Automata},
 booktitle ={QEST},
 year ={2011},
 pages ={151-152},
 ee ={http://doi.ieeecomputersociety.org/10.1109/QEST.2011.28},
 crossref ={DBLP:conf/qest/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{DBLP:conf/vmcai/DelahayeKLLPSW11,
 author ={Benoit Delahaye and Joost-Pieter Katoen and Kim G. Larsen and Axel Legay and Mikkel L. Pedersen and Falak Sher and Andrzej Wasowski},
 title ={Abstract Probabilistic Automata},
 booktitle ={VMCAI},
 year ={2011},
 pages ={324-339},
 ee ={http://dx.doi.org/10.1007/978-3-642-18275-4_23},
 crossref ={DBLP:conf/vmcai/2011},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@proceedings{DBLP:conf/vmcai/2011,
 editor ={Ranjit Jhala and David A. Schmidt},
 title ={Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings},
 booktitle ={VMCAI},
 publisher ={Springer},
 series ={Lecture Notes in Computer Science},
 volume ={6538},
 year ={2011},
 isbn ={978-3-642-18274-7},
 ee ={http://dx.doi.org/10.1007/978-3-642-18275-4},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/cacm/BouyerFLM11,
 author ={Patricia Bouyer and Uli Fahrenberg and Kim G. Larsen and Nicolas Markey},
 title ={Quantitative analysis of real-time systems using priced timed automata},
 journal ={Commun. ACM},
 volume ={54},
 number ={9},
 year ={2011},
 pages ={78-87},
 ee ={http://doi.acm.org/10.1145/1995376.1995396},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/spe/BehrmannDLPY11,
 author ={Gerd Behrmann and Alexandre David and Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
 title ={Developing UPPAAL over 15 years},
 journal ={Softw., Pract. Exper.},
 volume ={41},
 number ={2},
 year ={2011},
 pages ={133-142},
 ee ={http://dx.doi.org/10.1002/spe.1006},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/LarsenFT11,
 author ={Kim G. Larsen and Uli Fahrenberg and Claus R. Thrane},
 title ={Metrics for weighted transition systems: Axiomatization and complexity},
 journal ={Theor. Comput. Sci.},
 volume ={412},
 number ={28},
 year ={2011},
 pages ={3358-3369},
 ee ={http://dx.doi.org/10.1016/j.tcs.2011.04.003},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@article{DBLP:journals/tcs/CaillaudDLLPW11,
 author ={Benoit Caillaud and Benoit Delahaye and Kim G. Larsen and Axel Legay and Mikkel L. Pedersen and Andrzej Wasowski},
 title ={Constraint Markov Chains},
 journal ={Theor. Comput. Sci.},
 volume ={412},
 number ={34},
 year ={2011},
 pages ={4373-4404},
 ee ={http://dx.doi.org/10.1016/j.tcs.2011.05.010},
 bibsource ={DBLP, http://dblp.uni-trier.de},
}

@inproceedings{nfm1,
 author ={Yingke Chen and Hua Mao and Manfred Jaeger and Thomas Dyhre Nielsen and Kim G. Larsen and Brian Nielsen},
 title ={Learning Markov models for stationary system behaviors},
 booktitle ={Proceedings of Fourth NASA Formal Methods Symposium},
 optpages ={},
 year ={2012},
 opteditor ={},
 optvolume ={},
 optnumber ={},
 series ={Lecture Notes in Computer Science},
 optaddress ={},
 optmonth ={},
 optorganization ={},
 publisher ={Springer},
 note ={To appear},
 optannote ={},
 pdf ={nfmLearning.pdf},
}

@inproceedings{nfm2,
 author ={Peter Bulychev and Alexandre David and Kim G. Larsen and Axel Legay and Marius Mikucionis and Danny Bogsted Poulsen},
 title ={Checking & Distributing Statistical Model Checking},
 optcrossref ={},
 optkey ={},
 booktitle ={Proceedings of Fourth NASA Formal Methods Symposium},
 optpages ={},
 year ={2012},
 opteditor ={},
 optvolume ={},
 optnumber ={},
 series ={Lecture Notes in Computer Science},
 optaddress ={},
 optmonth ={},
 optorganization ={},
 publisher ={Springer},
 note ={To appear},
 optannote ={},
 pdf ={nfmSMC.pdf},
}

@inproceedings{lata2012,
 author ={Miroslav Klimos and Kim Guldstrand Larsen and Filip Stefanak and Jeppe Thaarup},
 title ={Nash Equilibria in Concurrent Priced Games},
 optcrossref ={},
 optkey ={},
 booktitle ={LATA - Language and Autoamta Theory and Applications},
 optpages ={},
 year ={2012},
 volume ={7183},
 optnumber ={},
 series ={Lecture Notes in Computer Science},
 optaddress ={},
 optmonth ={},
 optorganization ={},
 publisher ={Springer},
 optnote ={},
 optannote ={},
 pdf ={lata2012.pdf},
}

@inproceedings{lpar1,
 author ={Peter Bulychev and Alexandre David and Kim Guldstrand Larsen and Axel Legay and Guangyuan Li and Danny Bøgsted Poulsen and Amelie Stainer},
 title ={Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic},
 optcrossref ={},
 optkey ={},
 optbooktitle ={},
 optpages ={},
 year ={2012},
 opteditor ={},
 optvolume ={},
 optnumber ={},
 optseries ={},
 optaddress ={},
 optmonth ={},
 optorganization ={},
 optpublisher ={},
 note ={To appear in Proceedings of 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)},
 optannote ={},
 pdf ={LPARSMC.pdf},
}

@inproceedings{lpar2,
 author ={Nikola Benes and Jan Kretinsky and Kim Guldstrand Larsen, Mikael H. Moller and Jiri Srba},
 title ={Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, Mikael H. M\oller and Jiri Srba},
 optcrossref ={},
 optkey ={},
 optbooktitle ={},
 optpages ={},
 year ={2012},
 opteditor ={},
 optvolume ={},
 optnumber ={},
 optseries ={},
 optaddress ={},
 optmonth ={},
 optorganization ={},
 optpublisher ={},
 note ={To appear in Proceedings of 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)},
 optannote ={},
 pdf ={LPARMTS.pdf},
}

@inproceedings{fase2012,
 author ={Sebastian Bauer and Alexandre David adn Rolf Hennicker, Kim Guldstrand Larsen and Axel Legay and Ulrik Nyman and Andrzej Wasowski},
 title ={Moving from Specifications to Contracts in Component-based Design},
 optcrossref ={},
 optkey ={},
 optbooktitle ={},
 year ={2012},
 opteditor ={},
 optvolume ={},
 optnumber ={},
 optseries ={},
 optaddress ={},
 optmonth ={},
 optorganization ={},
 optpublisher ={},
 note ={To appear in Proceedings of 15th International Conference on Fundamental Approaches to Software Engineering (FASE)},
 optannote ={},
 pdf ={fase2012.pdf},
}

@article{mscs2012,
 author ={Sebastian S. Bauer and Line Juhl and Kim G. Larsen and Axel Legay and Jiri Srba},
 title ={Extending Modal Transition Systems with Structured Labels},
 journal ={Mathematical Structures in Computer Science},
 year ={2012},
 optkey ={},
 optvolume ={},
 optnumber ={},
 optpages ={},
 optmonth ={},
 note ={To appear},
 optannote ={},
 pdf ={Milner.pdf},
}