Skip to content
2012
Extending Modal Transition Systems with Structured Labels by Sebastian S. Bauer , Line Juhl , Kim G. Larsen , Axel Legay , Jiri Srba , Mathematical Structures in Computer Science 2012 (To appear) , PDF , BibTex ,
Moving from Specifications to Contracts in Component-based Design by Sebastian Bauer , Alexandre David adn Rolf Hennicker, Kim Guldstrand Larsen , Axel Legay , Ulrik Nyman , Andrzej Wasowski , in , 2012 (To appear in Proceedings of 15th International Conference on Fundamental Approaches to Software Engineering (FASE)) , PDF , BibTex ,
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, Mikael H. Møller and Jiri Srba by Nikola Benes , Jan Kretinsky , Kim Guldstrand Larsen, Mikael H. Moller , Jiri Srba , in , 2012 (To appear in Proceedings of 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)) , PDF , BibTex ,
Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic by Peter Bulychev , Alexandre David , Kim Guldstrand Larsen , Axel Legay , Guangyuan Li , Danny Bøgsted Poulsen , Amelie Stainer , in , 2012 (To appear in Proceedings of 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)) , PDF , BibTex ,
Nash Equilibria in Concurrent Priced Games by Miroslav Klimos , Kim Guldstrand Larsen , Filip Stefanak , Jeppe Thaarup , in LATA – Language and Autoamta Theory and Applications, 2012PDF , BibTex ,
Checking & Distributing Statistical Model Checking by Peter Bulychev , Alexandre David , Kim G. Larsen , Axel Legay , Marius Mikucionis , Danny Bogsted Poulsen , in Proceedings of Fourth NASA Formal Methods Symposium, 2012 (To appear) , PDF , BibTex ,
Learning Markov models for stationary system behaviors by Yingke Chen , Hua Mao , Manfred Jaeger , Thomas Dyhre Nielsen , Kim G. Larsen , Brian Nielsen , in Proceedings of Fourth NASA Formal Methods Symposium, 2012 (To appear) , PDF , BibTex ,
2011
Constraint Markov Chains by Benoit Caillaud , Benoit Delahaye , Kim G. Larsen , Axel Legay , Mikkel L. Pedersen , Andrzej Wasowski , Theor. Comput. Sci. vol: 412 pages: 4373-4404, 2011EE , BibTex ,
Metrics for weighted transition systems: Axiomatization and complexity by Kim G. Larsen , Uli Fahrenberg , Claus R. Thrane , Theor. Comput. Sci. vol: 412 pages: 3358-3369, 2011EE , BibTex ,
Developing UPPAAL over 15 years by Gerd Behrmann , Alexandre David , Kim Guldstrand Larsen , Paul Pettersson , Wang Yi , Softw., Pract. Exper. vol: 41 pages: 133-142, 2011EE , BibTex ,
Quantitative analysis of real-time systems using priced timed automata by Patricia Bouyer , Uli Fahrenberg , Kim G. Larsen , Nicolas Markey , Commun. ACM vol: 54 pages: 78-87, 2011EE , BibTex ,
Abstract Probabilistic Automata by Benoit Delahaye , Joost-Pieter Katoen , Kim G. Larsen , Axel Legay , Mikkel L. Pedersen , Falak Sher , Andrzej Wasowski , in Verification, Model Checking, and Abstract Interpretation – 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings (VMCAI) Editor: Ranjit Jhala and David A. Schmidt of Lecture Notes in Computer Science, vol: 6538 ©Springer-Verlag , pages: 324-339, 2011EE , BibTex ,
APAC: A Tool for Reasoning about Abstract Probabilistic Automata by Benoit Delahaye , Kim G. Larsen , Axel Legay , Mikkel L. Pedersen , Andrzej Wasowski , in Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 September, 2011 (QEST) IEEE Computer Society , pages: 151-152, 2011EE , BibTex ,
Learning Probabilistic Automata for Model Checking by Hua Mao , Yingke Chen , Manfred Jaeger , Thomas D. Nielsen , Kim G. Larsen , Brian Nielsen , in Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 September, 2011 (QEST) IEEE Computer Society , pages: 111-120, 2011EE , BibTex ,
Distances for Weighted Transition Systems: Games and Properties by Uli Fahrenberg , Claus R. Thrane , Kim G. Larsen , in Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL) Editor: Mieke Massink and Gethin Norman of EPTCS, vol: 57 , pages: 134-147, 2011EE , BibTex ,
Distributed Parametric and Statistical Model Checking by Peter E. Bulychev , Alexandre David , Kim Guldstrand Larsen , Marius Mikucionis , Axel Legay , in Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC) Editor: Jiri Barnat and Keijo Heljanko of EPTCS, vol: 72 , pages: 30-42, 2011EE , BibTex ,
opaal: A Lattice Model Checker by Andreas Engelbredt Dalsgaard , Rene Rydhof Hansen , Kenneth Yrke Jørgensen , Kim Guldstrand Larsen , Mads Chr. Olesen , Petur Olsen , Jiri Srba , in NASA Formal Methods – Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings (NASA Formal Methods) Editor: Mihaela Gheorghiu Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi of Lecture Notes in Computer Science, vol: 6617 ©Springer-Verlag , pages: 487-493, 2011EE , BibTex ,
Quantitative Refinement for Weighted Modal Transition Systems by Sebastian S. Bauer , Uli Fahrenberg , Line Juhl , Kim G. Larsen , Axel Legay , Claus R. Thrane , in Mathematical Foundations of Computer Science 2011 – 36th International Symposium, MFCS 2011, Warsaw, Poland, August 22-26, 2011. Proceedings (MFCS) Editor: Filip Murlak and Piotr Sankowski of Lecture Notes in Computer Science, vol: 6907 ©Springer-Verlag , pages: 60-71, 2011EE , BibTex ,
Decision Problems for Interval Markov Chains by Benoit Delahaye , Kim G. Larsen , Axel Legay , Mikkel L. Pedersen , Andrzej Wasowski , in Language and Automata Theory and Applications – 5th International Conference, LATA 2011, Tarragona, Spain, May 26-31, 2011. Proceedings (LATA) Editor: Adrian Horia Dediu and Shunsuke Inenaga and Carlos Martin-Vide of Lecture Notes in Computer Science, vol: 6638 ©Springer-Verlag , pages: 274-285, 2011EE , BibTex ,
Energy Games in Multiweighted Automata by Uli Fahrenberg , Line Juhl , Kim G. Larsen , Jiri Srba , in Theoretical Aspects of Computing – ICTAC 2011 – 8th International Colloquium, Johannesburg, South Africa, August 31 – September 2, 2011. Proceedings (ICTAC) Editor: Antonio Cerone and Pekka Pihlajasaari of Lecture Notes in Computer Science, vol: 6916 ©Springer-Verlag , pages: 95-115, 2011EE , BibTex ,
Modular Markovian Logic by Luca Cardelli , Kim G. Larsen , Radu Mardare , in Automata, Languages and Programming – 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II (ICALP (2)) Editor: Luca Aceto and Monika Henzinger and Jiri Sgall of Lecture Notes in Computer Science, vol: 6756 ©Springer-Verlag , pages: 380-391, 2011EE , BibTex ,
Statistical Model Checking for Networks of Priced Timed Automata by Alexandre David , Kim G. Larsen , Axel Legay , Marius Mikucionis , Danny Bøgsted Poulsen , Jonas van Vliet , Zheng Wang , in Formal Modeling and Analysis of Timed Systems – 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings (FORMATS) Editor: Uli Fahrenberg and Stavros Tripakis of Lecture Notes in Computer Science, vol: 6919 ©Springer-Verlag Formal Modeling and Analysis of Timed Systems – 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings (FORMATS) Editor: Uli Fahrenberg and Stavros Tripakis of Lecture Notes in Computer Science, vol: 6919 ©Springer-Verlag , pages: 80-96, 2011EE , PDF , BibTex ,
Robust Specification of Real Time Components by Kim G. Larsen , Axel Legay , Louis-Marie Traonouez , Andrzej Wasowski , in Formal Modeling and Analysis of Timed Systems – 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings (FORMATS) Editor: Uli Fahrenberg and Stavros Tripakis of Lecture Notes in Computer Science, vol: 6919 ©Springer-Verlag Formal Modeling and Analysis of Timed Systems – 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings (FORMATS) Editor: Uli Fahrenberg and Stavros Tripakis of Lecture Notes in Computer Science, vol: 6919 ©Springer-Verlag , pages: 129-144, 2011EE , BibTex ,
Continuous Markovian Logic – From Complete Axiomatization to the Metric Space of Formulas by Luca Cardelli , Kim G. Larsen , Radu Mardare , in Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings (CSL) Editor: Marc Bezem of LIPIcs, vol: 12 Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik , pages: 144-158, 2011EE , BibTex ,
Timed Automata Can Always Be Made Implementable by Patricia Bouyer , Kim G. Larsen , Nicolas Markey , Ocan Sankur , Claus R. Thrane , in CONCUR 2011 – Concurrency Theory – 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings (CONCUR) Editor: Joost-Pieter Katoen and Barbara König of Lecture Notes in Computer Science, vol: 6901 ©Springer-Verlag , pages: 76-91, 2011EE , BibTex ,
Time for Statistical Model Checking of Real-Time Systems by Alexandre David , Kim G. Larsen , Axel Legay , Marius Mikucionis , Zheng Wang , in Computer Aided Verification – 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (CAV) Editor: Ganesh Gopalakrishnan and Shaz Qadeer of Lecture Notes in Computer Science, vol: 6806 ©Springer-Verlag , pages: 349-355, 2011EE , PDF , BibTex ,
Parametric Modal Transition Systems by Nikola Benes , Jan Kretinsky , Kim G. Larsen , Mikael H. Møller , Jiri Srba , in Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings (ATVA) Editor: Tevfik Bultan and Pao-Ann Hsiung of Lecture Notes in Computer Science, vol: 6996 ©Springer-Verlag , pages: 275-289, 2011EE , BibTex ,
2010
Quantitative Analysis of Weighted Transition Systems by Claus Thrane , Uli Fahrenberg , Kim Guldstrand Larsen , Journal of Logic and Algebraic Programming vol: 79 pages: 689-703, 2010PDF , BibTex , Show Abstract .
Timed I/O automata: a complete specification theory for real-time systems by Alexandre David , Kim G. Larsen , Axel Legay , Ulrik Nyman , Andrzej Wasowski , in Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 (HSCC) Editor: Karl Henrik Johansson and Wang YiACM ACM Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 (HSCC) Editor: Karl Henrik Johansson and Wang YiACM ACM , pages: 91-100, 2010EE , BibTex , Show Abstract .
Timed automata with observers under energy constraints by Patricia Bouyer , Uli Fahrenberg , Kim G. Larsen , Nicolas Markey , in Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 (HSCC) Editor: Karl Henrik Johansson and Wang YiACM ACM Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 (HSCC) Editor: Karl Henrik Johansson and Wang YiACM ACM , pages: 61-70, 2010EE , BibTex , Show Abstract .
Scenario-based analysis and synthesis of real-time systems using uppaal by Kim Guldstrand Larsen , Shuhao Li , Brian Nielsen , Saulius Pusinskas , in DATE: Design, Automation and Test in Europe, DATE 2010, Dresden, Germany, March 8-12, pages: 447-452, 2010EE , BibTex , Show Abstract .
METAMOC: Modular Execution Tiem Analysis using Model Checking by Andreas E. Dalsgaard , Mads Chr. Olesen , Martin Toft , Rene R. Hansen , Kim G. Larsen , in Proceedings of 10th International Workshop on Worst-Case Execution Time Analysis, 2010 (To appear.) , BibTex , Show Abstract .
Compositional Design Methodology with Constraint Markov Chains by Benoit Caillaud , Benoit Delahaye , Kim G. Larsen , Axel Legay , Mikkel Larsen Pedersen , Andrzej Wasowski , in Proceedings of 7th International Conference on Quantitative Evaluation of SysTems (QEST), 2010 (To appear) , BibTex , Show Abstract .
ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems by Alexandre David , Kim G. Larsen , Axel Legay , Ulrik Nyman , Andrzej Wasowski , in Proceedings of 8th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2010 (To appear) , BibTex , Show Abstract .
Developing UPPAAL over 15 Years by Gerd Behrmann , Alexandere David , Kim G. Larsen , Paul Pettersson , Wang Yi , Software – Practice and Experience 2010 (To appear) , BibTex , Show Abstract .
An Interface Theory for Timed Systems by Alexandre David , Kim G. Larsen , Axel Legay , Ulrik Nyman , Andrzej Wasowski , in Proceedings of 20th International Workshop on Algebraic Development Techniques WADT, 2010 (To appear) , BibTex , Show Abstract .
Present and Absent Sets: Abstraction for Testing of Reactive Systems with Databases by Petur Olsen , Kim G. Larsen , Arne Skou , in Proceedings of 6th Workshop on Model-Based Testing, 2010BibTex , Show Abstract .
A Quantitatve Characterization of Weighted Kripke Structures in Temporal Logic by Uli Fahrenberg , Kim G. Larsen , Claus Thrane , Journal of Computing and Informatics 2010 (to appear) , BibTex , Show Abstract .
Symbolic and Compositional Reachability for Timed Automata by Kim Guldstrand Larsen , in Reachability Problems, 4th International Workshop, RP 2010, Brno, Czech Republic, August 28-29, 2010. Proceedings (RP) Editor: Antonin Kucera and Igor Potapov of Lecture Notes in Computer Science, vol: 6227 ©Springer-Verlag , pages: 24-28, 2010EE , BibTex , Show Abstract .
Schedulability Analysis Using Uppaal: Herscehl-Planck Case Study by M. Mikucionis , K.G. Larsen , B. Nielsen , J. Illum , A. Skou , S.U. Palm , J.S. Pedersen , P. Hougaard , in Proceedings of 4th International Symposiumo on Leveraging Applications of Formal Methods, Verification and Validation; track: Quantitative Verification in Practice, 2010BibTex , Show Abstract .
On Zone-Based Analysis of Duration Probabilistic Automata by O. Maler , K.G. Larsen , B. Krogh , in Proceedings of INFINITY, International Workshop on Verification of Infinite-State Systems, 2010BibTex , Show Abstract .
Modal and mixed specifications: key decision problems and their complexities by Adam Antonik , Michael Huth , Kim G. Larsen , Ulrik Nyman , Andrzej Wasowski , Mathematical Structures in Computer Science vol: 20 pages: 75-103, 2010BibTex , Show Abstract .
2009
EXPTIME-complete Decision Problems for Modal and Mixed Specifications by Adam Antonik , Michael Huth , Kim Guldstrand Larsen , Ulrik Nyman , Andrzej Wasowski , Electr. Notes Theor. Comput. Sci. vol: 242 pages: 19-33, 2009EE , PDF , BibTex ,
Discount-Optimal Infinite Runs in Priced Timed Automata by Ulrich Fahrenberg , Kim Guldstrand Larsen , Electr. Notes Theor. Comput. Sci. vol: 239 pages: 179-191, 2009EE , PDF , BibTex ,
Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete by Nikola Benes , Jan Kretinsky , Kim Guldstrand Larsen , Jiri Srba , in Theoretical Aspects of Computing – ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings (ICTAC) Editor: Martin Leucker and Carroll Morgan of Lecture Notes in Computer Science, vol: 5684 ©Springer-Verlag , pages: 112-126, 2009EE , PDF , BibTex ,
Automatic Synthesis of Robust and Optimal Controllers – An Industrial Case Study by Franck Cassez , Jan Jakob Jessen , Kim Guldstrand Larsen , Jean-Franccois Raskin , Pierre-Alain Reynier , in Hybrid Systems: Computation and Control, 12th International Conference, HSCC 2009, San Francisco, CA, USA, April 13-15, 2009. Proceedings (HSCC) Editor: Rupak Majumdar and Paulo Tabuada of Lecture Notes in Computer Science, vol: 5469 ©Springer-Verlag , pages: 90-104, 2009EE , PDF , BibTex ,
Verification, Performance Analysis and Controller Synthesis for Real-Time Systems by Uli Fahrenberg , Kim Guldstrand Larsen , Claus Thrane , in Proceedings of 3rd International Conference on Fundamentals of Software Engineering, 15 – 17 April, Kish Island, Persian Gulf, Iran (FSEN 09) ©Springer-Verlag , 2009 (to appear) , BibTex , Show Abstract .
Quantitative Modeling and Analysis of Embedded Systems by Patricia Bouyer , Ulrich Fahrenberg , Kim Guldstrand Larsen , Nicolas Markey , Communications of the ACM 2009 (Invited paper, to appear) , BibTex ,
On Determinism in Modal Transition Systems by Nikola Benes , Jan Kretinsky , Kim Guldstrand Larsen , Jiri Srba , Special Issue of Theoretical Computer Science 2009 (to appear) , BibTex ,
UPPAAL TIGA 2009 – towards realizable strategies by Alexandre David , Kim Guldstrand Larsen , Didier Lime , in Proceedings of Workshop on Games for Design, Verification and Synthesis, GASICS, 2009 (to appear) , BibTex ,
Quantitative and Compositional Model Checking by Kim Guldstrand Larsen , in Proceedings of Seventh International Andrei Ershov Memorial Conference (PSI), Novosibirsk, Russia, 2009 (to appear) , BibTex ,
Quantitative Verification and Validation of Embedded Systems by Kim Guldstrand Larsen , in Proceedings of of 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE09, Tianjin, China, 2009 (to appear) , BibTex ,
Discounting in Time by Ulrich Fahrenberg , Kim Guldstrand Larsen , in proceedings of 7th Workshop on Quantitative Aspects of Programming Languages, 2009 (to appear) , BibTex ,
Timed Testing under Partial Observability by Alexandre David , Kim Guldstrand Larsen , Shuhao Li , Brian Nielsen , Software Testing, Verification, and Validation, 2008 International Conference on vol: 0 IEEE Computer Society pages: 61-70, 2009EE , BibTex , Show Abstract .
UPPAAL PRO: Tool for Performance Analysis of Probabilistic Timed Automata by Alexandre David , Arild Haugstad , Kim G. Larsen , 2009 (Under submission) , BibTex ,
Teaching Concurrency: Theory in Practice by Luca Aceto , Anna Ingolfsdottir , Kim Guldstrand Larsen , Jiri Srba , 2009 (Under submission) , BibTex ,
Verifying Real-Time Systems against Scenario-Based Requirements by Kim Guldstrand Larsen , Shuhao Li , Brian Nielsen , Saulius Pusinskas , in FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings (FM) Editor: Ana Cavalcanti and Dennis Dams of Lecture Notes in Computer Science, vol: 5850 ©Springer-Verlag , pages: 676-691, 2009EE , PDF , BibTex , Show Abstract .
A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic by Uli Fahrenberg , Kim G. Larsen , Claus Thrane , in Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMIC09), 2009 (Best paper award) , BibTex ,
2008
Optimal reachability for multi-priced timed automata by Kim Guldstrand Larsen , Jacob Illum Rasmussen , Theor. Comput. Sci. vol: 390 pages: 197-213, 2008EE , PDF , BibTex ,
Model Checking One-Clock Priced Timed Automata by Patricia Bouyer , Kim Guldstrand Larsen , Nicolas Markey , Logical Methods in Computer Science vol: 4 2008EE , BibTex ,
Optimal infinite scheduling for multi-priced timed automata by Patricia Bouyer , Ed Brinksma , Kim Guldstrand Larsen , Formal Methods in System Design vol: 32 pages: 3-23, 2008EE , PDF , BibTex , Show Abstract .
Cooperative Testing of Timed Systems by Alexandre David , Kim Guldstrand Larsen , Shuhao Li , Brian Nielsen , Electr. Notes Theor. Comput. Sci. vol: 220 pages: 79-92, 2008EE , PDF , BibTex ,
Model Checking One-clock Priced Timed Automata by Patricia Bouyer , Kim Guldstrand Larsen , Nicolas Markey , CoRR vol: abs/0805.1457 2008EE , BibTex ,
Fast Directed Model Checking Via Russian Doll Abstraction by Sebastian Kupferschmid , Jörg Hoffmann , Kim Guldstrand Larsen , in 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 (TACAS) Editor: C. R. Ramakrishnan and Jakob Rehof of Lecture Notes in Computer Science, vol: 4963 ©Springer-Verlag , pages: 203-217, 2008EE , PDF , BibTex ,
Model-based schedulability analysis of safety critical hard real-time Java programs by Thomas Bøgholm , Henrik Kragh-Hansen , Petur Olsen , Bent Thomsen , Kim Guldstrand Larsen , in 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 (JTRES) Editor: Gregory Bollella and C. Douglas Locke of ACM International Conference Proceeding Series, vol: 343 ACM , pages: 106-114, 2008EE , PDF , BibTex ,
Testing Real-Time Systems Using UPPAAL by Anders Hessel , Kim Guldstrand Larsen , Marius Mikucionis , Brian Nielsen , Paul Pettersson , Arne Skou , in Formal Methods and Testing, An Outcome of the FORTEST Network, Revised Selected Papers (Formal Methods and Testing) Editor: Robert M. Hierons and Jonathan P. Bowen and Mark Harman of Lecture Notes in Computer Science, vol: 4949 ©Springer-Verlag , pages: 77-117, 2008EE , PDF , BibTex , Show Abstract .
Complexity of Decision Problems for Mixed and Modal Specifications by Adam Antonik , Michael Huth , Kim Guldstrand Larsen , Ulrik Nyman , Andrzej Wasowski , in 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 (FoSSaCS) Editor: Roberto M. Amadio of Lecture Notes in Computer Science, vol: 4962 ©Springer-Verlag , pages: 112-126, 2008EE , PDF , BibTex , Show Abstract .
Infinite Runs in Weighted Timed Automata with Energy Constraints by Patricia Bouyer , Ulrich Fahrenberg , Kim Guldstrand Larsen , Nicolas Markey , Jiri Srba , in Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings (FORMATS) Editor: Franck Cassez and Claude Jard of Lecture Notes in Computer Science, vol: 5215 ©Springer-Verlag , pages: 33-47, 2008EE , PDF , BibTex , Show Abstract .
A Game-Theoretic Approach to Real-Time System Testing by Alexandre David , Kim Guldstrand Larsen , Shuhao Li , Brian Nielsen , in Design, Automation and Test in Europe, DATE 2008, Munich, Germany, March 10-14, 2008 (DATE) IEEE , pages: 486-491, 2008EE , PDF , BibTex , Show Abstract .
Optimal infinite scheduling for multi-priced timed automata by Patricia Bouyer , Ed Brinksma , Kim Guldstrand Larsen , Form. Methods Syst. Des. vol: 32 ©Kluwer pages: 3–23, 2008EE , PDF , BibTex , Show Abstract .
Verification, Performance Analysis and Controller Synthesis for Real-Time Systems by Uli Fahrenberg , Kim Guldstrand Larsen , Claus Thrane , in Proceedings of the NATO Advanced Study Institute on Engineering Methods and Tools for Software Safety and Security Marktoberdorf, Germany 5-17 August 2008 (ASI 08) Editor: Manfred Broy , Wassiou Sitou and Tony Hoare of NATO Science for Peace and Security Series – D: Information and Communication Security, vol: 22 IOS Press BV , 2008BibTex , Show Abstract .
Quantitative Simulations of Weighted Transition Systems by Claus Thrane , Uli Fahrenberg , Kim Guldstrand Larsen , in Proceedings of 20th Nordic Workshop of Programming Theory (NWPT) Editor: Tarmo Uustalu, Jüri Vain and Juhan Ernits, pages: 97-100, 2008 (Extended version invited for publication in Special Issue of Journal of Logic and Algebraic Programming, 2009) , BibTex , Show Abstract .
Slicing for Uppaal by Claus Thrane , Uffe Sørensen , Kim Guldstrand Larsen , in Proceedings of 20th Nordic Workshop of Programming Theory (NWPT) Editor: Tarmo Uustalu, Jüri Vain and Juhan Ernits, pages: 100-103, 2008BibTex , Show Abstract .
Cooperative Testing of Timed Systems by Alexandre David , Kim Guldstrand Larsen , Shuhao Li , Brian Nielsen , in Proceedings of the 4th Workshop on Model-based Testing (MBT), pages: 79-92, 2008EE , BibTex , Show Abstract .
Approches formelles des syst`emes embarques communicant by Gerd Behrmann , Beatrice Berard , Franck Cassez , Thao Dang , Alexandre David , Susanna Donatelli , Jean-Pierre Elloy , Goran Frehse , Antoine Girard , Serge Haddad , Claude Jard , Kim Guldstrand Larsen , Colas Le Guernic , Didier Lime , Morgan Magnin , Nicolas Markey , Paul Pettersson , Jacob Illum Rasmussen , Olivier H. Roux , Stavros Tripakis , Wang Yi , Hermes Lavoisier, serie Informatique et syst`emes dinformation 2008BibTex ,
2007
Modeling software product lines using color-blind transition systems by Kim Guldstrand Larsen , Ulrik Nyman , Andrzej Wasowski , STTT vol: 9 pages: 471-487, 2007EE , BibTex ,
Complexity in Simplicity: Flexible Agent-Based State Space Exploration by Jacob Illum Rasmussen , Gerd Behrmann , Kim Guldstrand Larsen , in 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 (TACAS) Editor: Orna Grumberg and Michael Huth of Lecture Notes in Computer Science, vol: 4424 ©Springer-Verlag , pages: 231-245, 2007EE , BibTex ,
Model-Checking One-Clock Priced Timed Automata by Patricia Bouyer , Kim Guldstrand Larsen , Nicolas Markey , in 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 (FoSSaCS) Editor: Helmut Seidl of Lecture Notes in Computer Science, vol: 4423 ©Springer-Verlag , pages: 108-122, 2007EE , PDF , BibTex ,
Guided Controller Synthesis for Climate Controller Using Uppaal Tiga by Jan Jakob Jessen , Jacob Illum Rasmussen , Kim Guldstrand Larsen , Alexandre David , in Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings (FORMATS) Editor: Jean-Franccois Raskin and P. S. Thiagarajan of Lecture Notes in Computer Science, vol: 4763 ©Springer-Verlag , pages: 227-240, 2007EE , BibTex ,
Automatic Abstraction Refinement for Timed Automata by Henning Dierks , Sebastian Kupferschmid , Kim Guldstrand Larsen , in Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings (FORMATS) Editor: Jean-Franccois Raskin and P. S. Thiagarajan of Lecture Notes in Computer Science, vol: 4763 ©Springer-Verlag , pages: 114-129, 2007EE , BibTex ,
Modal I/O Automata for Interface and Product Line Theories by Kim Guldstrand Larsen , Ulrik Nyman , Andrzej Wasowski , in 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 (ESOP) Editor: Rocco De Nicola of Lecture Notes in Computer Science, vol: 4421 ©Springer-Verlag , pages: 64-79, 2007EE , BibTex ,
On Modal Refinement and Consistency by Kim Guldstrand Larsen , Ulrik Nyman , Andrzej Wasowski , in CONCUR 2007 – Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings (CONCUR) Editor: Luis Caires and Vasco Thudichum Vasconcelos of Lecture Notes in Computer Science, vol: 4703 ©Springer-Verlag , pages: 105-119, 2007EE , BibTex ,
UPPAAL-Tiga: Time for Playing Games! by Gerd Behrmann , Agn`es Cougnard , Alexandre David , Emmanuel Fleury , Kim Guldstrand Larsen , Didier Lime , in Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings (CAV) Editor: Werner Damm and Holger Hermanns of Lecture Notes in Computer Science, vol: 4590 ©Springer-Verlag , pages: 121-125, 2007EE , BibTex ,
Timed Control with Observation Based and Stuttering Invariant Strategies by Franck Cassez , Alexandre David , Kim Guldstrand Larsen , Didier Lime , Jean-Franccois Raskin , in Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings (ATVA) Editor: Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura of Lecture Notes in Computer Science, vol: 4762 ©Springer-Verlag , pages: 192-206, 2007EE , BibTex ,
Automatic Abstraction Refinement for Timed Automata by Henning Dierks , Sebastian Kupferschmid , Kim Guldstrand Larsen , in Proceedings of Formal Modeling and Analysis of Timed Systems, 5th International Conference, (FORMATS), pages: 114-129, 2007BibTex , Show Abstract .
Reactive Systems: Modelling, Specification and Verification by Luca Aceto , Anna Ingolfsdottir , Kim Guldstrand Larsen , Jiri Srba , Cambridge University Press 2007BibTex ,
2006
Lower and upper bounds in zone-based abstractions of timed automata by Gerd Behrmann , Patricia Bouyer , Kim Guldstrand Larsen , Radek Pelanek , STTT vol: 8 pages: 204-215, 2006EE , BibTex ,
CyNC: A method for real time analysis of systems with cyclic data flows by Henrik Schiøler , Jens Dalsgaard Nielsen , Kim Guldstrand Larsen , Jan Jakob Jessen , J. Embedded Computing vol: 2 pages: 347-360, 2006EE , BibTex ,
On using priced timed automata to achieve optimal scheduling by Jacob Illum Rasmussen , Kim Guldstrand Larsen , K. Subramani , Formal Methods in System Design vol: 29 pages: 97-114, 2006EE , BibTex ,
UPPAAL 4.0 by Gerd Behrmann , Alexandre David , Kim Guldstrand Larsen , John Haakansson , Paul Pettersson , Wang Yi , Martijn Hendriks , in Third International Conference on the Quantitative Evaluaiton of Systems (QEST 2006), 11-14 September 2006, Riverside, California, USA (QEST) IEEE Computer Society , pages: 125-126, 2006EE , BibTex ,
Almost Optimal Strategies in One Clock Priced Timed Games by Patricia Bouyer , Kim Guldstrand Larsen , Nicolas Markey , Jacob Illum Rasmussen , in FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings (FSTTCS) Editor: S. Arun-Kumar and Naveen Garg of Lecture Notes in Computer Science, vol: 4337 ©Springer-Verlag , pages: 345-356, 2006EE , BibTex ,
Model Checking Timed Automata with Priorities Using DBM Subtraction by Alexandre David , John Haakansson , Kim Guldstrand Larsen , Paul Pettersson , in Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, September 25-27, 2006, Proceedings (FORMATS) Editor: Eugene Asarin and Patricia Bouyer of Lecture Notes in Computer Science, vol: 4202 ©Springer-Verlag , pages: 128-142, 2006EE , BibTex ,
Interface Input/Output Automata by Kim Guldstrand Larsen , Ulrik Nyman , Andrzej Wasowski , in FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings (FM) Editor: Jayadev Misra and Tobias Nipkow and Emil Sekerinski of Lecture Notes in Computer Science, vol: 4085 ©Springer-Verlag , pages: 82-97, 2006EE , BibTex ,
Introducing synchronisation in deterministic network models by Henrik Schiøler , Jan Jakob Jessen , Jens Dalsgaard , Kim Guldstrand Larsen , in Proceedings of the ISCA 19th International Conference on Computer Applications in Industry and Engineering, CAINE 2006, November 13-15, 2006, Las Vegas, Nevada, USA (CAINE) Editor: Thomas PhilipISCA , pages: 236-243, 2006BibTex ,
2005
Optimal scheduling using priced timed automata by Gerd Behrmann , Kim Guldstrand Larsen , Jacob Illum Rasmussen , SIGMETRICS Performance Evaluation Review vol: 32 pages: 34-40, 2005EE , BibTex ,
Synthesis of Optimal Strategies Using HyTech by Patricia Bouyer , Franck Cassez , Emmanuel Fleury , Kim Guldstrand Larsen , Electr. Notes Theor. Comput. Sci. vol: 119 pages: 11-31, 2005EE , BibTex ,
An approach to handle real time and probabilistic behaviors in e-commerce: validating the SET protocol by Gregorio Diaz , Kim Guldstrand Larsen , Juan Jose Pardo , Fernando Cuartero , Valentin Valero , in Proceedings of the 2005 ACM Symposium on Applied Computing (SAC), Santa Fe, New Mexico, USA, March 13-17, 2005 (SAC) Editor: Hisham Haddad and Lorie M. Liebrock and Andrea Omicini and Roger L. WainwrightACM , pages: 815-820, 2005EE , BibTex ,
Optimal Conditional Reachability for Multi-priced Timed Automata by Kim Guldstrand Larsen , Jacob Illum Rasmussen , in 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 (FoSSaCS) Editor: Vladimiro Sassone of Lecture Notes in Computer Science, vol: 3441 ©Springer-Verlag , pages: 234-249, 2005EE , BibTex ,
Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness by Gerd Behrmann , Kim Guldstrand Larsen , Jacob Illum Rasmussen , in Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings (FORMATS) Editor: Paul Pettersson and Wang Yi of Lecture Notes in Computer Science, vol: 3829 ©Springer-Verlag , pages: 81-94, 2005EE , BibTex ,
Color-Blind Specifications for Transformations of Reactive Synchronous Programs by Kim Guldstrand Larsen , Ulrik Larsen , Andrzej Wasowski , in 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 (FASE) Editor: Maura Cerioli of Lecture Notes in Computer Science, vol: 3442 ©Springer-Verlag , pages: 160-174, 2005EE , BibTex ,
Testing real-time embedded software using UPPAAL-TRON: an industrial case study by Kim Guldstrand Larsen , Marius Mikucionis , Brian Nielsen , Arne Skou , in EMSOFT 2005, September 18-22, 2005, Jersey City, NJ, USA, 5th ACM International Conference On Embedded Software, Proceedings (EMSOFT) Editor: Wayne WolfACM , pages: 299-306, 2005EE , BibTex ,
Network Calculus for Real Time Analysis of Embedded Systems with Cyclic Task Dependencies by Henrik Schiøler , Jan Jakob Jessen , Jens Dalsgaard , Kim Guldstrand Larsen , in 20th International Conference on Computers and Their Applications, CATA 2005, March 16-18, 2005, Holiday Inn Downtown-Superdome Hotel, New Orleans, Louisiana, USA, Proceedings (Computers and Their Applications) Editor: Gongzhu HuISCA , pages: 326-332, 2005BibTex ,
Efficient On-the-Fly Algorithms for the Analysis of Timed Games by Franck Cassez , Alexandre David , Emmanuel Fleury , Kim Guldstrand Larsen , Didier Lime , in CONCUR 2005 – Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings (CONCUR) Editor: Martin Abadi and Luca de Alfaro of Lecture Notes in Computer Science, vol: 3653 ©Springer-Verlag , pages: 66-80, 2005EE , BibTex ,
CyNC – towards a General Tool for Performance Analysis of Complex Distributed Real Time Systems by Henrik Schiøler , Jan Jakob Jessen , Jens F. Dalsgaard Nielsen , Kim Guldstrand Larsen , in Proccedings of 17th Euromicro Conference on Real-Time Systems (ECRTS 05), 2005BibTex ,
CyNC – a method for Real Time Analysis of Systems with Cyclic Data Flows by Henrik Schiøler , Jens Dalsgaard Nielsen , Kim Guldstrand Larsen , Jan Jakob Jessen , in Proceedings of 13 th. RTS Conference on Embedded Systems, 2005BibTex ,
Interface Input/Output Automata: Splitting Assumptions from Guarantees by Kim Guldstrand Larsen , Ulrik Nyman , Andrzej Wasowski , in Foundations of Interface Technologies (FIT 2005), 2005 (affiliated workshop of CONCUR 2005. San Francisco, CA, USA, August 20, 2005. Preliminary Proceedings. To be published in ENTCS.) , BibTex ,
Formal Methods and Testing by Anders Hessel , Kim Guldstrand Larsen , Marius Mikucionis , Brian Nielsen , Paul Pettersson , Arne Skou , ©Springer-Verlag pages: 39, 2005 (to appear) , BibTex ,
Embedded Systems Design The ARTIST Roadmap for Research and Development Series by Kim Guldstrand Larsen , Brian Nielsen , ©Springer-Verlag 2005BibTex ,
2004
Lower and Upper Bounds in Zone Based Abstractions of Timed Automata by Gerd Behrmann , Patricia Bouyer , Kim Guldstrand Larsen , Radek Pelanek , in 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 (TACAS) Editor: Kurt Jensen and Andreas Podelski of Lecture Notes in Computer Science, vol: 2988 ©Springer-Verlag , pages: 312-326, 2004EE , BibTex ,
Resource-Optimal Scheduling Using Priced Timed Automata by Jacob Illum Rasmussen , Kim Guldstrand Larsen , K. Subramani , in 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 (TACAS) Editor: Kurt Jensen and Andreas Podelski of Lecture Notes in Computer Science, vol: 2988 ©Springer-Verlag , pages: 220-235, 2004EE , BibTex ,
A Tutorial on Uppaal by Gerd Behrmann , Alexandre David , Kim Guldstrand Larsen , in 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 (SFM) Editor: Marco Bernardo and Flavio Corradini of Lecture Notes in Computer Science, vol: 3185 ©Springer-Verlag , pages: 200-236, 2004EE , BibTex ,
Online Testing of Real-Time Systems Using UPPAAL: Status and Future Work by Kim Guldstrand Larsen , Marius Mikucionis , Brian Nielsen , in Perspectives of Model-Based Testing, 5.-10. September 2004 (Perspectives of Model-Based Testing) Editor: Ed Brinksma and Wolfgang Grieskamp and Jan Tretmans of Dagstuhl Seminar Proceedings, vol: 04371 IBFI, Schloss Dagstuhl, Germany , 2004EE , BibTex ,
Staying Alive as Cheaply as Possible by Patricia Bouyer , Ed Brinksma , Kim Guldstrand Larsen , in Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings (HSCC) Editor: Rajeev Alur and George J. Pappas of Lecture Notes in Computer Science, vol: 2993 ©Springer-Verlag , pages: 203-218, 2004EE , BibTex ,
Optimal Strategies in Priced Timed Game Automata by Patricia Bouyer , Franck Cassez , Emmanuel Fleury , Kim Guldstrand Larsen , in FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings (FSTTCS) Editor: Kamal Lodaya and Meena Mahajan of Lecture Notes in Computer Science, vol: 3328 ©Springer-Verlag , pages: 148-160, 2004EE , BibTex ,
Priced Timed Automata: Algorithms and Applications by Gerd Behrmann , Kim Guldstrand Larsen , Jacob Illum Rasmussen , in Formal Methods for Components and Objects, Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2 – 5, 2004, Revised Lectures (FMCO) Editor: Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever of Lecture Notes in Computer Science, vol: 3657 ©Springer-Verlag , pages: 162-182, 2004EE , BibTex ,
Online Testing of Real-time Systems Using Uppaal by Kim Guldstrand Larsen , Marius Mikucionis , Brian Nielsen , in Formal Approaches to Software Testing, 4th International Workshop, FATES 2004, Linz, Austria, September 21, 2004, Revised Selected Papers (FATES) Editor: Jens Grabowski and Brian Nielsen of Lecture Notes in Computer Science, vol: 3395 ©Springer-Verlag , pages: 79-94, 2004EE , BibTex ,
T-UPPAAL: Online Model-based Testing of Real-Time Systems by Marius Mikucionis , Kim Guldstrand Larsen , Brian Nielsen , in 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 20-25 September 2004, Linz, Austria (ASE) IEEE Computer Society , pages: 396-397, 2004EE , BibTex ,
T-UPPAAL: online model-based testing of real-time systems by Mikucionis, M. , Larsen, Kim Guldstrand , Nielsen, B. , in Automated Software Engineering, 2004. Proceedings. 19th International Conference on, pages: 396-397, 2004EE , BibTex , Show Abstract .
2003
The power of reachability testing for timed automata by Luca Aceto , Patricia Bouyer , Augusto Burgue no , Kim Guldstrand Larsen , Theor. Comput. Sci. vol: 300 pages: 411-475, 2003EE , BibTex ,
Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems by Kim Guldstrand Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi , Real-Time Systems vol: 25 pages: 255-275, 2003EE , BibTex ,
Regular languages definable by Lindström quantifiers by Zoltan Esik , Kim Guldstrand Larsen , ITA vol: 37 pages: 179-241, 2003EE , BibTex ,
Static Guard Analysis in Timed Automata Verification by Gerd Behrmann , Patricia Bouyer , Emmanuel Fleury , Kim Guldstrand Larsen , in 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 (TACAS) Editor: Hubert Garavel and John Hatcliff of Lecture Notes in Computer Science, vol: 2619 ©Springer-Verlag , pages: 254-277, 2003EE , BibTex ,
Unification & Sharing in Timed Automata Verification by Alexandre David , Gerd Behrmann , Kim Guldstrand Larsen , Wang Yi , in Model Checking Software, 10th International SPIN Workshop. Portland, OR, USA, May 9-10, 2003, Proceedings (SPIN) Editor: Thomas Ball and Sriram K. Rajamani of Lecture Notes in Computer Science, vol: 2648 ©Springer-Verlag , pages: 225-229, 2003EE , BibTex ,
Adding Symmetry Reduction to Uppaal by Martijn Hendriks , Gerd Behrmann , Kim Guldstrand Larsen , Peter Niebert , Frits W. Vaandrager , in Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003. Revised Papers (FORMATS) Editor: Kim Guldstrand Larsen and Peter Niebert of Lecture Notes in Computer Science, vol: 2791 ©Springer-Verlag , pages: 46-59, 2003EE , BibTex ,
Time-Optimal Test Cases for Real-Time Systems by Anders Hessel , Kim Guldstrand Larsen , Brian Nielsen , Paul Pettersson , Arne Skou , in Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003. Revised Papers (FORMATS) Editor: Kim Guldstrand Larsen and Peter Niebert of Lecture Notes in Computer Science, vol: 2791 ©Springer-Verlag , pages: 234-245, 2003EE , BibTex ,
Time-Optimal Real-Time Test Case Generation Using Uppaal by Anders Hessel , Kim Guldstrand Larsen , Brian Nielsen , Paul Pettersson , Arne Skou , in Formal Approaches to Software Testing, Third International Workshop on Formal Approaches to Testing of Software, FATES 2003, Montreal, Quebec, Canada, October 6th, 2003 (FATES) Editor: Alexandre Petrenko and Andreas Ulrich of Lecture Notes in Computer Science, vol: 2931 ©Springer-Verlag , pages: 114-130, 2003EE , BibTex ,
Resource-Efficient Scheduling for Real Time Systems by Kim Guldstrand Larsen , in Embedded Software, Third International Conference, EMSOFT 2003, Philadelphia, PA, USA, October 13-15, 2003, Proceedings (EMSOFT) Editor: Rajeev Alur and Insup Lee of Lecture Notes in Computer Science, vol: 2855 ©Springer-Verlag , pages: 16-19, 2003EE , BibTex ,
To Store or Not to Store by Gerd Behrmann , Kim Guldstrand Larsen , Radek Pelanek , in Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings (CAV) Editor: Warren A. Hunt Jr. and Fabio Somenzi of Lecture Notes in Computer Science, vol: 2725 ©Springer-Verlag , pages: 433-445, 2003EE , BibTex ,
2002
Automated verification of an audio-control protocol using UPPAAL by Johan Bengtsson , W. O. David Griffioen , Kaare J. Kristoffersen , Kim Guldstrand Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi , J. Log. Algebr. Program. vol: 52-53 pages: 163-181, 2002EE , BibTex ,
Verification of Hierarchical State/Event Systems using Reusability and Compositionality by Gerd Behrmann , Kim Guldstrand Larsen , Henrik Reif Andersen , Henrik Hulgaard , Jørn Lind-Nielsen , Formal Methods in System Design vol: 21 pages: 225-244, 2002BibTex ,
Exact Acceleration of Real-Time Model Checking by Martijn Hendriks , Kim Guldstrand Larsen , Electr. Notes Theor. Comput. Sci. vol: 65 2002EE , BibTex ,
Reduction and Refinement Strategies for Probabilistic Analysis by Pedro R. DArgenio , Bertrand Jeannet , Henrik Ejersbo Jensen , Kim Guldstrand Larsen , in Process Algebra and Probabilistic Methods, Performance Modeling and Verification, Second Joint International Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002, Proceedings (PAPM-PROBMIV) Editor: Holger Hermanns and Roberto Segala of Lecture Notes in Computer Science, vol: 2399 ©Springer-Verlag , pages: 57-76, 2002EE , BibTex ,
UPPAAL Implementation Secrets by Gerd Behrmann , Johan Bengtsson , Alexandre David , Kim Guldstrand Larsen , Paul Pettersson , Wang Yi , in 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 (FTRTFT) Editor: Werner Damm and Ernst-Rüdiger Olderog of Lecture Notes in Computer Science, vol: 2469 ©Springer-Verlag , pages: 3-22, 2002EE , BibTex ,
A Tool Architecture for the Next Generation of Uppaal by Alexandre David , Gerd Behrmann , Kim Guldstrand Larsen , Wang Yi , in 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 (10th Anniversary Colloquium of UNU/IIST) Editor: Bernhard K. Aichernig and T. S. E. Maibaum of Lecture Notes in Computer Science, vol: 2757 ©Springer-Verlag , pages: 352-366, 2002EE , BibTex ,
Solving Planning Problems Using Real-Time Model Checking by Henning Dierks , Gerd Behrmann , Kim Guldstrand Larsen , in AIPS-Workshop Planning via Model-Checking, pages: 30–39, 2002BibTex ,
2001
Guided Synthesis of Control Programs Using UPPAAL by Thomas Hune , Kim Guldstrand Larsen , Paul Pettersson , Nord. J. Comput. vol: 8 pages: 43-64, 2001BibTex ,
Verification of Large State/Event Systems Using Compositionality and Dependency Analysis by Jørn Lind-Nielsen , Henrik Reif Andersen , Henrik Hulgaard , Gerd Behrmann , Kaare J. Kristoffersen , Kim Guldstrand Larsen , Formal Methods in System Design vol: 18 pages: 5-23, 2001BibTex ,
Reachability Analysis of Probabilistic Systems by Successive Refinements by Pedro R. DArgenio , Bertrand Jeannet , Henrik Ejersbo Jensen , Kim Guldstrand Larsen , in Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001, Aachen, Germany, September 12-14, 2001, Proceedings (PAPM-PROBMIV) Editor: Luca de Alfaro and Stephen Gilmore of Lecture Notes in Computer Science, vol: 2165 ©Springer-Verlag , pages: 39-56, 2001EE , BibTex ,
Minimum-Cost Reachability for Priced Timed Automata by Gerd Behrmann , Ansgar Fehnker , Thomas Hune , Kim Guldstrand Larsen , Paul Pettersson , Judi Romijn , Frits W. Vaandrager , in Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings (HSCC) Editor: Maria Domenica Di Benedetto and Alberto L. Sangiovanni-Vincentelli of Lecture Notes in Computer Science, vol: 2034 ©Springer-Verlag , pages: 147-161, 2001EE , BibTex ,
As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata by Kim Guldstrand Larsen , Gerd Behrmann , Ed Brinksma , Ansgar Fehnker , Thomas Hune , Paul Pettersson , Judi Romijn , in Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings (CAV) Editor: Gerard Berry and Hubert Comon and Alain Finkel of Lecture Notes in Computer Science, vol: 2102 ©Springer-Verlag , pages: 493-505, 2001EE , BibTex ,
Reachability Analysis of Probabilistic Systems by Successive Refinements by Pedro R. DArgenio , Bertrand Jeannet , Henrik E. Jensen , Kim Guldstrand Larsen , in Process Algebra and Probabilistic Methods. Performance Modelling and Verification, pages: 39-56, 2001EE , BibTex ,
UPPAAL – present and future by Behrmann, G. , Kim Guldstrand Larsen , Moller, O. , David, A. , Pettersson, P. , Wang Yi , in Decision and Control, 2001. Proceedings of the 40th IEEE Conference on, pages: 2881-2886 vol.3, 2001EE , BibTex , Show Abstract .
Probabilistic Extensions of Process Algebras by Bengt Jonsson , Kim Guldstrand Larsen , Wang Yi , in Handbook of Process Algebra, pages: 685–710, 2001EE , BibTex , Show Abstract .
2000
Practical Verification of Embedded Software by Jørgen Staunstrup , Henrik Reif Andersen , Henrik Hulgaard , Jørn Lind-Nielsen , Kim Guldstrand Larsen , Gerd Behrmann , Kaare J. Kristoffersen , Arne Skou , Henrik Leerberg , Niels Bo Theilgaard , IEEE Computer vol: 33 pages: 68-75, 2000EE , BibTex ,
UPPAAL – Now, Next, and Future by Tobias Amnell , Gerd Behrmann , Johan Bengtsson , Pedro R. DArgenio , Alexandre David , Ansgar Fehnker , Thomas Hune , Bertrand Jeannet , Kim Guldstrand Larsen , M. Oliver Möller , Paul Pettersson , Carsten Weise , Wang Yi , in Modeling and Verification of Parallel Processes, 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000 (MOVEP) Editor: Franck Cassez and Claude Jard and Brigitte Rozoy and Mark Dermot Ryan of Lecture Notes in Computer Science, vol: 2067 ©Springer-Verlag , pages: 99-124, 2000EE , BibTex ,
Guided Synthesis of Control Programs Using UPPAAL by Thomas Hune , Kim Guldstrand Larsen , Paul Pettersson , in Proceedings of the 2000 ICDCS Workshops, April 10, 2000, Taipei, Taiwan, ROC (ICDCS Workshops) Editor: Ten-Hwang Lai, pages: E15-E22, 2000BibTex ,
Verification of Timed and Hybrid Systems by Kim Guldstrand Larsen , in ICATPN, pages: 39-42, 2000EE , BibTex ,
Scaling up Uppaal Automatic Verification of Real-Time Systems Using Compositionality and Abstraction by Henrik Ejersbo Jensen , Kim Guldstrand Larsen , Arne Skou , in Formal Techniques in Real-Time and Fault-Tolerant Systems, 6th International Symposium, FTRTFT 2000, Pune, India, September 20-22, 2000, Proceedings (FTRTFT) Editor: Mathai Joseph of Lecture Notes in Computer Science, vol: 1926 ©Springer-Verlag , pages: 19-30, 2000EE , BibTex ,
Model-checking real-time control programs: verifying Lego(R) Mindstorms$^mboxTM$ systems using UPPAAL by Torsten K. Iversen , Kaare J. Kristoffersen , Kim Guldstrand Larsen , Morten Laursen , Rune G. Madsen , Steffen K. Mortensen , Paul Pettersson , Chris B. Thomasen , in 12th Euromicro Conference on Real-Time Systems (ECRTS 2000), 19-21 June 2000, Stockholm, Sweden, Proceedings (ECRTS) IEEE Computer Society , pages: 147-155, 2000EE , BibTex ,
The Impressive Power of Stopwatches by Franck Cassez , Kim Guldstrand Larsen , in CONCUR 2000 – Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings (CONCUR) Editor: Catuscia Palamidessi of Lecture Notes in Computer Science, vol: 1877 ©Springer-Verlag , pages: 138-152, 2000EE , BibTex ,
1999
Clock Difference Diagrams by Kim Guldstrand Larsen , Justin Pearson , Carsten Weise , Wang Yi , Nord. J. Comput. vol: 6 pages: 271-298, 1999BibTex ,
Verification of Hierarchical State/Event Systems Using Reusability and Compositionality by Gerd Behrmann , Kim Guldstrand Larsen , Henrik Reif Andersen , Henrik Hulgaard , Jørn Lind-Nielsen , in 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, ETAPS99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings (TACAS) Editor: Rance Cleaveland of Lecture Notes in Computer Science, vol: 1579 ©Springer-Verlag , pages: 163-177, 1999EE , BibTex ,
Efficient Timed Reachability Analysis Using Clock Difference Diagrams by Gerd Behrmann , Kim Guldstrand Larsen , Justin Pearson , Carsten Weise , Wang Yi , in Computer Aided Verification, 11th International Conference, CAV 99, Trento, Italy, July 6-10, 1999, Proceedings (CAV) Editor: Nicolas Halbwachs and Doron Peled of Lecture Notes in Computer Science, vol: 1633 ©Springer-Verlag , pages: 341-353, 1999EE , BibTex ,
Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL by Klaus Havelund , Kim Guldstrand Larsen , Arne Skou , in Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, ARTS99, Bamberg, Germany, May 26-28, 1999. Proceedings (ARTS) Editor: Joost-Pieter Katoen of Lecture Notes in Computer Science, vol: 1601 ©Springer-Verlag , pages: 277-298, 1999EE , BibTex ,
Verification of State/Event Systems by Quotienting by Nicky Oliver Bodentien , Jacob Vestergaard , Jakob Friis , Nicky Oliver , Bodentien Jacob , Vestergaard Jakob Friis , KÃ¥re Jelling Kristoffersen , Kristoffersen Kim , Kim Guldstrand Larsen , in Proceedings of Nordic Workshop of Programming Theory, 1999BibTex , Show Abstract .
Clock Difference Diagrams by Kim Guldstrand Larsen , Justin Pearson , Carsten Weise , Wang Yi , in Proceedings of Nordic Workshop of Programming Theory, 1999BibTex ,
UPPAAL2k by Kim Guldstrand Larsen , P. Pettersson , 1999BibTex ,
1998
Model Checking via Reachability Testing for Timed Automata by Luca Aceto , Augusto Burgue no , Kim Guldstrand Larsen , in 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, ETAPS98, Lisbon, Portugal, March 28 – April 4, 1998, Proceedings (TACAS) Editor: Bernhard Steffen of Lecture Notes in Computer Science, vol: 1384 ©Springer-Verlag , pages: 263-280, 1998EE , BibTex ,
Verification of Large State/Event Systems Using Compositionality and Dependency Analysis by Jørn Lind-Nielsen , Henrik Reif Andersen , Gerd Behrmann , Henrik Hulgaard , Kaare J. Kristoffersen , Kim Guldstrand Larsen , in 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, ETAPS98, Lisbon, Portugal, March 28 – April 4, 1998, Proceedings (TACAS) Editor: Bernhard Steffen of Lecture Notes in Computer Science, vol: 1384 ©Springer-Verlag , pages: 201-216, 1998EE , BibTex ,
The Power of Reachability Testing for Timed Automata by Luca Aceto , Patricia Bouyer , Augusto Burgue no , Kim Guldstrand Larsen , in Foundations of Software Technology and Theoretical Computer Science, 18th Conference, Chennai, India, December 17-19, 1998, Proceedings (FSTTCS) Editor: Vikraman Arvind and Ramaswamy Ramanujam of Lecture Notes in Computer Science, vol: 1530 ©Springer-Verlag , pages: 245-256, 1998BibTex ,
CMC: A Tool for Compositional Model-Checking of Real-Time Systems by Franccois Laroussinie , Kim Guldstrand Larsen , in Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE XI / PSTV XVIII98, 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 (FORTE) Editor: Stanislaw Budkowski and Ana R. Cavalli and Elie Najm of IFIP Conference Proceedings, vol: 135 Kluwer , pages: 439-456, 1998BibTex ,
The Limit of Testing for Timed Automata by L. Aceto , P. Bouyer , A. Burgueno , Kim Guldstrand Larsen , in Proceedings of Foundations of Software Technology and Theoretical Computer Science, India, 1998., 1998BibTex ,
New Generation of UPPAAL by Johan Bengtsson , Kim Larsen , Fredrik Larsson , Paul Pettersson , Yi Wang , Carsten Weise , in proceedings of the International Workshop on Software Tools for Technology Transfer, 1998BibTex , Show Abstract .
1997
Continuous Modeling of Real-Time and Hybrid Systems: From Concepts to Tools by Kim Guldstrand Larsen , Bernhard Steffen , Carsten Weise , STTT vol: 1 pages: 64-85, 1997EE , BibTex ,
UPPAAL in a Nutshell by Kim Guldstrand Larsen , Paul Pettersson , Wang Yi , STTT vol: 1 pages: 134-152, 1997EE , BibTex ,
Time-abstracted Bisimulation: Implicit Specifications and Decidability by Kim Guldstrand Larsen , Wang Yi , Inf. Comput. vol: 134 pages: 75-101, 1997BibTex ,
A Compositional Proof of a Real-Time Mutual Exclusion Protocol by Kaare J. Kristoffersen , Franccois Laroussinie , Kim Guldstrand Larsen , Paul Pettersson , Wang Yi , in TAPSOFT97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, April 14-18, 1997, Proceedings (TAPSOFT) Editor: Michel Bidoit and Max Dauchet of Lecture Notes in Computer Science, vol: 1214 ©Springer-Verlag , pages: 565-579, 1997BibTex ,
Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAA by Klaus Havelund , Arne Skou , Kim Guldstrand Larsen , K. Lund , in Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 97), December 3-5, 1997, San Francisco, CA, USA (IEEE Real-Time Systems Symposium) IEEE Computer Society , pages: 2-13, 1997EE , BibTex ,
Efficient verification of real-time systems: compact data structure and state-space reduction by Kim Guldstrand Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi , in Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 97), December 3-5, 1997, San Francisco, CA, USA (IEEE Real-Time Systems Symposium) IEEE Computer Society , pages: 14-24, 1997EE , BibTex ,
UPPAAL: Status & Developments by Kim Guldstrand Larsen , Paul Pettersson , Wang Yi , in Computer Aided Verification, 9th International Conference, CAV 97, Haifa, Israel, June 22-25, 1997, Proceedings (CAV) Editor: Orna Grumberg of Lecture Notes in Computer Science, vol: 1254 ©Springer-Verlag , pages: 456-459, 1997BibTex ,
Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL by Klaus Havelund , Arne Skou , Kim Guldstrand Larsen , Kristian Lund , in Proceedings of the 18th IEEE Real-Time Systems Symposium (December 03 – 05, 1997), pages: 2, 1997EE , BibTex , Show Abstract .
Efficient verification of real-time systems: compact data structure and state-space reduction by Kim Guldstrand Larsen , F. Larsson , P. Pettersson , W. Yi , Real-Time Systems Symposium, IEEE International vol: 0 IEEE Computer Society pages: 14, 1997EE , BibTex , Show Abstract .
Context Dependent Minimization of State/Event Systems by Gerd Behrmann , KÃ¥re Kristoffersen , Kim Larsen , in Proceedings of Nordic Workshop of Programming Correctness, 1997BibTex , Show Abstract .
Time Abstracted Bisimulation: Implicit Specifications and Decidability by Kim Guldstrand Larsen , Yi Wang , in Information and Computation, 1997BibTex ,
1996
UPPAAL in 1995 by Johan Bengtsson , Kim Guldstrand Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi , in Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS 96, Passau, Germany, March 27-29, 1996, Proceedings (TACAS) Editor: Tiziana Margaria and Bernhard Steffen of Lecture Notes in Computer Science, vol: 1055 ©Springer-Verlag , pages: 431-434, 1996BibTex ,
Verification of an Audio Protocol with Bus Collision Using UPPAAL by Johan Bengtsson , W. O. David Griffioen , Kaare J. Kristoffersen , Kim Guldstrand Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi , in Computer Aided Verification, 8th International Conference, CAV 96, New Brunswick, NJ, USA, July 31 – August 3, 1996, Proceedings (CAV) Editor: Rajeev Alur and Thomas A. Henzinger of Lecture Notes in Computer Science, vol: 1102 ©Springer-Verlag , pages: 244-256, 1996BibTex ,
Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL by Henrik Ejersbo Jensen , Jensen Kim , Kim Guldstrand Larsen , Arne Skou , in Proceedings of the 2nd International Workshop on the SPIN Verification System, 1996BibTex , Show Abstract .
1995
Synthesizing Distinguishing Formulae for Real Time Systems by Jens Chr. Godskesen , Kim Guldstrand Larsen , Nord. J. Comput. vol: 2 pages: 338-357, 1995BibTex ,
Generality in Design and Compositional Verification Using TAV by Anders Børjesson , Kim Guldstrand Larsen , Arne Skou , Formal Methods in System Design vol: 6 pages: 239-258, 1995BibTex ,
A Constraint Oriented Proof Methodology Based on Modal Transition Systems by Kim Guldstrand Larsen , Bernhard Steffen , Carsten Weise , in Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS 95, Aarhus, Denmark, May 19-20, 1995, Proceedings (TACAS) Editor: Ed Brinksma and Rance Cleaveland and Kim Guldstrand Larsen and Tiziana Margaria and Bernhard Steffen of Lecture Notes in Computer Science, vol: 1019 ©Springer-Verlag , pages: 17-40, 1995BibTex ,
From Timed Automata to Logic – and Back by Franccois Laroussinie , Kim Guldstrand Larsen , Carsten Weise , in Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS95, Prague, Czech Republic, August 28 – September 1, 1995, Proceedings (MFCS) Editor: Jiri Wiedermann and Petr Hajek of Lecture Notes in Computer Science, vol: 969 ©Springer-Verlag , pages: 529-539, 1995BibTex ,
Synthesizing Distinguishing Formulae for Real Time Systems (Extended Abstract) by Jens Chr. Godskesen , Kim Guldstrand Larsen , in Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS95, Prague, Czech Republic, August 28 – September 1, 1995, Proceedings (MFCS) Editor: Jiri Wiedermann and Petr Hajek of Lecture Notes in Computer Science, vol: 969 ©Springer-Verlag , pages: 519-528, 1995BibTex ,
Compositional and Symbolic Model-Checking of Real-Time Systems by Kim Guldstrand Larsen , Paul Pettersson , Wang Yi , in IEEE Real-Time Systems Symposium, pages: 76-89, 1995BibTex ,
Automatic Synthesis of Real Time Systems by Jørgen H. Andersen , Kaare J. Kristoffersen , Kim Guldstrand Larsen , Jesper Niedermann , in Automata, Languages and Programming, 22nd International Colloquium, ICALP95, Szeged, Hungary, July 10-14, 1995, Proceedings (ICALP) Editor: Zoltan Fülöp and Ferenc Gecseg of Lecture Notes in Computer Science, vol: 944 ©Springer-Verlag , pages: 535-546, 1995BibTex ,
Fischers Protocol Revisited: A Simple Proof Using Modal Constraints by Kim Guldstrand Larsen , Bernhard Steffen , Carsten Weise , in Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA (Hybrid Systems) Editor: Rajeev Alur and Thomas A. Henzinger and Eduardo D. Sontag of Lecture Notes in Computer Science, vol: 1066 ©Springer-Verlag , pages: 604-615, 1995BibTex ,
Diagnostic Model-Checking for Real-Time Systems by Kim Guldstrand Larsen , Paul Pettersson , Wang Yi , in Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA (Hybrid Systems) Editor: Rajeev Alur and Thomas A. Henzinger and Eduardo D. Sontag of Lecture Notes in Computer Science, vol: 1066 ©Springer-Verlag , pages: 575-586, 1995BibTex ,
UPPAAL – a Tool Suite for Automatic Verification of Real-Time Systems by Johan Bengtsson , Kim Guldstrand Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi , in Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA (Hybrid Systems) Editor: Rajeev Alur and Thomas A. Henzinger and Eduardo D. Sontag of Lecture Notes in Computer Science, vol: 1066 ©Springer-Verlag , pages: 232-243, 1995BibTex ,
Model-Checking for Real-Time Systems by Kim Guldstrand Larsen , Paul Pettersson , Wang Yi , in Fundamentals of Computation Theory, 10th International Symposium, FCT 95, Dresden, Germany, August 22-25, 1995, Proceedings (FCT) Editor: Horst Reichel of Lecture Notes in Computer Science, vol: 965 ©Springer-Verlag , pages: 62-88, 1995BibTex ,
Compositional Model Checking of Real Time Systems by Franccois Laroussinie , Kim Guldstrand Larsen , in CONCUR 95: Concurrency Theory, 6th International Conference, Philadelphia, PA, USA, August 21-24, 1995, Proceedings (CONCUR) Editor: Insup Lee and Scott A. Smolka of Lecture Notes in Computer Science, vol: 962 ©Springer-Verlag , pages: 27-41, 1995BibTex ,
A refinement logic for the Fork Calculus by Havelund, Klaus , Larsen, Kim Guldstrand , in PSTV 94: Proceedings of the fourteenth of a series of annual meetings on Protocol specification, testing and verification XIV, pages: 5–20, 1995BibTex ,
1994
The Fork Calculus by Klaus Havelund , Kim Guldstrand Larsen , Nord. J. Comput. vol: 1 pages: 346-363, 1994BibTex ,
A refinement logic for the fork calculus by Klaus Havelund , Kim Guldstrand Larsen , in 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 (PSTV) Editor: Son T. Vuong and Samuel T. Chanson of IFIP Conference Proceedings, vol: 1 Chapman & Hall , pages: 5-20, 1994BibTex ,
Automatic verification of real-tim systems using epsilon by Jens Chr. Godskesen , Kim Guldstrand Larsen , Arne Skou , in 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 (PSTV) Editor: Son T. Vuong and Samuel T. Chanson of IFIP Conference Proceedings, vol: 1 Chapman & Hall , pages: 323-330, 1994BibTex ,
The Methodology of Modal Constraints by Kim Guldstrand Larsen , Bernhard Steffen , Carsten Weise , in Formal Systems Specification, The RPC-Memory Specification Case Study (the book grow out of a Dagstuhl Seminar, September 1994) (Formal Systems Specification) Editor: Manfred Broy and Stephan Merz and Katharina Spies of Lecture Notes in Computer Science, vol: 1169 ©Springer-Verlag , pages: 405-435, 1994BibTex ,
1993
The Expressive Power of Implicit Specifications by Kim Guldstrand Larsen , Theor. Comput. Sci. vol: 114 pages: 119-147, 1993BibTex ,
Time Abstracted Bisimiulation: Implicit Specifications and Decidability by Kim Guldstrand Larsen , Wang Yi , in Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings (MFPS) Editor: Stephen D. Brookes and Michael G. Main and Austin Melton and Michael W. Mislove and David A. Schmidt of Lecture Notes in Computer Science, vol: 802 ©Springer-Verlag , pages: 160-176, 1993BibTex ,
The Fork Calculus by Klaus Havelund , Kim Guldstrand Larsen , in Automata, Languages and Programming, 20nd International Colloquium, ICALP93, Lund, Sweden, July 5-9, 1993, Proceedings (ICALP) Editor: Andrzej Lingas and Rolf G. Karlsson and Svante Carlsson of Lecture Notes in Computer Science, vol: 700 ©Springer-Verlag , pages: 544-557, 1993BibTex ,
Model Construction for Implicit Specifications in Model Logic by Ole Høgh Jensen , Jarl Tuxen Lang , Christian Jeppesen , Kim Guldstrand Larsen , in CONCUR 93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings (CONCUR) Editor: Eike Best of Lecture Notes in Computer Science, vol: 715 ©Springer-Verlag , pages: 247-261, 1993BibTex ,
Timed Modal Specification – Theory and Tools by Karlis Cerans , Jens Chr. Godskesen , Kim Guldstrand Larsen , in Computer Aided Verification, 5th International Conference, CAV 93, Elounda, Greece, June 28 – July 1, 1993, Proceedings (CAV) Editor: Costas Courcoubetis of Lecture Notes in Computer Science, vol: 697 ©Springer-Verlag , pages: 253-267, 1993BibTex ,
1992
Graphical Versus Logical Specifications by Gerard Boudol , Kim Guldstrand Larsen , Theor. Comput. Sci. vol: 106 pages: 3-20, 1992BibTex ,
A Compositional Protocol Verification Using Relativized Bisimulation by Kim Guldstrand Larsen , Robin Milner , Inf. Comput. vol: 99 pages: 80-108, 1992BibTex ,
Testing Probabilistic and Nondeterministic Processes by Wang Yi , Kim Guldstrand Larsen , in 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 (PSTV) Editor: Richard J. Linn Jr. and M. “Umit Uyar of IFIP Transactions, vol: C-8 North-Holland , pages: 47-61, 1992BibTex ,
Real-Time Calculi and Expansion Theorems by Jens Chr. Godskesen , Kim Guldstrand Larsen , in NAPAW 92, Proceedings of the First North American Process Algebra Workshop, Stony Brook, New York, USA, 28 Agust 1992 (NAPAW) Editor: S. Purushothaman and Amy E. Zwarico of Workshops in Computing, ©Springer-Verlag , pages: 3-12, 1992BibTex ,
Real-Time Calculi and Expansion Theorems by Jens Chr. Godskesen , Kim Guldstrand Larsen , in Foundations of Software Technology and Theoretical Computer Science, 12th Conference, New Delhi, India, December 18-20, 1992, Proceedings (FSTTCS) Editor: R. K. Shyamasundar of Lecture Notes in Computer Science, vol: 652 ©Springer-Verlag , pages: 302-315, 1992BibTex ,
Generality in design and compositional verification using TAV by Anders Børjesson , Kim Guldstrand Larsen , Arne Skou , in 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 (FORTE) Editor: Michel Diaz and Roland Groz of IFIP Transactions, vol: C-10 North-Holland , pages: 449-464, 1992BibTex ,
Compositional Verification of Probabilistic Processes by Kim Guldstrand Larsen , Arne Skou , in CONCUR 92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings (CONCUR) Editor: Rance Cleaveland of Lecture Notes in Computer Science, vol: 630 ©Springer-Verlag , pages: 456-471, 1992BibTex ,
Efficient Local Correctness Checking by Kim Guldstrand Larsen , in Computer Aided Verification, Fourth International Workshop, CAV 92, Montreal, Canada, June 29 – July 1, 1992, Proceedings (CAV) Editor: Gregor von Bochmann and David K. Probst of Lecture Notes in Computer Science, vol: 663 ©Springer-Verlag , pages: 30-43, 1992BibTex ,
1991
Partial Specifications and Compositional Verification by Kim Guldstrand Larsen , Bent Thomsen , Theor. Comput. Sci. vol: 88 pages: 15-32, 1991BibTex ,
Compositionality through an Operational Semantics of Contexts by Kim Guldstrand Larsen , Liu Xinxin , J. Log. Comput. vol: 1 pages: 761-795, 1991BibTex ,
Bisimulation through Probabilistic Testing by Kim Guldstrand Larsen , Arne Skou , Inf. Comput. vol: 94 pages: 1-28, 1991BibTex ,
Using Information Systems to Solve Recursive Domain Equations by Kim Guldstrand Larsen , Glynn Winskel , Inf. Comput. vol: 91 pages: 232-258, 1991BibTex ,
On the Complexity of Equation Solving in Process Algebra by Bengt Jonsson , Kim Guldstrand Larsen , in TAPSOFT91: 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 (CAAP91) (TAPSOFT, Vol.1) Editor: Samson Abramsky and T. S. E. Maibaum of Lecture Notes in Computer Science, vol: 493 ©Springer-Verlag , pages: 381-396, 1991BibTex ,
Specification and Refinement of Probabilistic Processes by Bengt Jonsson , Kim Guldstrand Larsen , in Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, 15-18 July, 1991, Amsterdam, The Netherlands (LICS) IEEE Computer Society , pages: 266-277, 1991BibTex ,
The Expressive Power of Implicit Specifications by Kim Guldstrand Larsen , in Automata, Languages and Programming, 18th International Colloquium, ICALP91, Madrid, Spain, July 8-12, 1991, Proceedings (ICALP) Editor: Javier Leach Albert and Burkhard Monien and Mario Rodriguez-Artalejo of Lecture Notes in Computer Science, vol: 510 ©Springer-Verlag , pages: 204-216, 1991BibTex ,
Deciding Properties of Regular Real Time Processes by Uno Holmer , Kim Guldstrand Larsen , Wang Yi , in Computer Aided Verification, 3rd International Workshop, CAV 91, Aalborg, Denmark, July, 1-4, 1991, Proceedings (CAV) Editor: Kim Guldstrand Larsen and Arne Skou of Lecture Notes in Computer Science, vol: 575 ©Springer-Verlag , pages: 443-453, 1991BibTex ,
Bisimulation Through Probabilistic Testing by Kim Guldstrand Larsen , Arne Skou , in Information and Control (IC91), 1991BibTex ,
1990
Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion by Kim Guldstrand Larsen , Theor. Comput. Sci. vol: 72 pages: 265-288, 1990BibTex ,
Equation Solving Using Modal Transition Systems by Kim Guldstrand Larsen , Liu Xinxin , in Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, 4-7 June 1990, Philadelphia, Pennsylvania, USA (LICS) IEEE Computer Society , pages: 108-117, 1990BibTex ,
Compositionality Through an Operational Semantics of Contexts by Kim Guldstrand Larsen , Liu Xinxin , in Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, July 16-20, 1990, Proceedings (ICALP) Editor: Mike Paterson of Lecture Notes in Computer Science, vol: 443 ©Springer-Verlag , pages: 526-539, 1990BibTex ,
Ideal Specification Formalism + Expressivity + Compositionality + Decidability + Testability + .. by Kim Guldstrand Larsen , in CONCUR 90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings (CONCUR) Editor: Jos C. M. Baeten and Jan Willem Klop of Lecture Notes in Computer Science, vol: 458 ©Springer-Verlag , pages: 33-56, 1990BibTex ,
Graphical versus Logical Specifications by Gerard Boudol , Kim Guldstrand Larsen , in CAAP 90, 15th Colloquium on Trees in Algebra and Programming, Copenhagen, Denmark, May 15-18, 1990, Proceedings (CAAP) Editor: Andre Arnold of Lecture Notes in Computer Science, vol: 431 ©Springer-Verlag , pages: 57-71, 1990BibTex ,
1989
Compositional Theories Based on an Operational Semantics of Contexts by Kim Guldstrand Larsen , in Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands, May 29 – June 2, 1989, Proceedings (REX Workshop) Editor: J. W. de Bakker and Willem P. de Roever and Grzegorz Rozenberg of Lecture Notes in Computer Science, vol: 430 ©Springer-Verlag , pages: 487-518, 1989BibTex ,
Bisimulation Through Probabilistic Testing by Kim Guldstrand Larsen , Arne Skou , in POPL, pages: 344-352, 1989BibTex ,
The Use of Static Constructs in A Modal Process Logic by Hans Hüttel , Kim Guldstrand Larsen , in Logic at Botik 89, Symposium on Logical Foundations of Computer Science, Pereslav-Zalessky, USSR, July 3-8, 1989, Proceedings (Logic at Botik) Editor: Albert R. Meyer and Michael A. Taitslin of Lecture Notes in Computer Science, vol: 363 ©Springer-Verlag , pages: 163-180, 1989BibTex ,
Modal Specifications by Kim Guldstrand Larsen , in Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings (Automatic Verification Methods for Finite State Systems) Editor: Joseph Sifakis of Lecture Notes in Computer Science, vol: 407 ©Springer-Verlag , pages: 232-246, 1989BibTex ,
TAV — tools for automatic verification — Users Manual by Jens Godskesen , Kim Guldstrand Larsen , Michael Zeeberg , 1989BibTex ,
1988
Compositional Proofs by Partial Specification of Processes by Kim Guldstrand Larsen , Bent Thomsen , in Mathematical Foundations of Computer Science 1988, MFCS88, Carlsbad, Czechoslovakia, August 29 – September 2, 1988, Proceedings (MFCS) Editor: Michal Chytil and Ladislav Janiga and Vaclav Koubek of Lecture Notes in Computer Science, vol: 324 ©Springer-Verlag , pages: 414-423, 1988BibTex ,
A Modal Process Logic by Kim Guldstrand Larsen , Bent Thomsen , in Proceedings, Third Annual Symposium on Logic in Computer Science, 5-8 July 1988, Edinburgh, Scotland, UK (LICS) IEEE Computer Society , pages: 203-210, 1988BibTex ,
Proof System for Hennessy-Milner Logic with Recursion by Kim Guldstrand Larsen , in CAAP 88, 13th Colloquium on Trees in Algebra and Programming, Nancy, France, March 21-24, 1988, Proceedings (CAAP) Editor: Max Dauchet and Maurice Nivat of Lecture Notes in Computer Science, vol: 299 ©Springer-Verlag , pages: 215-230, 1988BibTex ,
1987
Recursively Defined Doains and their Induction Principles by Finn Verner Jensen , Kim Guldstrand Larsen , Theor. Comput. Sci. vol: 54 pages: 29-51, 1987BibTex ,
A Context Dependent Equivalence Between Processes by Kim Guldstrand Larsen , Theor. Comput. Sci. vol: 49 pages: 184-215, 1987BibTex ,
Verifying a Protocol Using Relativized Bisimulation by Kim Guldstrand Larsen , Robin Milner , in Automata, Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987, Proceedings (ICALP) Editor: Thomas Ottmann of Lecture Notes in Computer Science, vol: 267 ©Springer-Verlag , pages: 126-135, 1987BibTex ,
1986
1985
A Context Dependent Equivalence between Processes by Kim Guldstrand Larsen , in Automata, Languages and Programming, 12th Colloquium, Nafplion, Greece, July 15-19, 1985, Proceedings (ICALP) Editor: Wilfried Brauer of Lecture Notes in Computer Science, vol: 194 ©Springer-Verlag , pages: 373-382, 1985BibTex ,
Recursively Defined Domains and Their Induction Principles by Finn Verner Jensen , Kim Guldstrand Larsen , in Foundations of Software Technology and Theoretical Computer Science, Fifth Conference, New Delhi, India, December 16-18, 1985, Proceedings (FSTTCS) Editor: S. N. Maheshwari of Lecture Notes in Computer Science, vol: 206 ©Springer-Verlag , pages: 225-245, 1985BibTex ,
1984
Using Information Systems to Solve Recursive Domain Equations Effectively by Glynn Winskel , Kim Guldstrand Larsen , in Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings (Semantics of Data Types) Editor: Gilles Kahn and David B. MacQueen and Gordon D. Plotkin of Lecture Notes in Computer Science, vol: 173 ©Springer-Verlag , pages: 109-129, 1984BibTex ,