Kim Guldstrand Larsen

Kim Guldstrand Larsen
Kim Guldstrand Larsen i 2021 (Foto: Lars Horn / Baghuset)
Personlig information
Født	23. december 1957 (66 år)
Nationalitet	Dansk
Uddannelse og virke
Uddannelses­sted	Aalborg Universitet
Tilknyttet	Institut for Datalogi, Aalborg Universitet
Medlem af	Videnskabernes Selskab, Academia Europaea (fra 2012)
Beskæftigelse	Professor
Arbejdsgiver	Aalborg Universitet
Kendt for	UPPAAL (værktøj til verifikation af realtidsmodeller)
Nomineringer og priser
Udmærkelser	Medlem af Videnskabernes Selskab Ridder af Dannebrog
Eksterne henvisninger
https://vbn.aau.dk/en/persons/103881
Information med symbolet hentes fra Wikidata. Kildehenvisninger foreligger sammesteds.  [ redigér på Wikidata ]

Kim Guldstrand Larsen (født 23. december 1957)^[1] er professor ved Institut for Datalogi ved Aalborg Universitet. Hans forskningsområde inkluderer modellering, verifikation, performanceanalyse og syntese af realtids-, indlejrede systemer og cyber-fysiske systemer med anvendelse af og bidrag til concurrency teori og model checking.

Kim Guldstrand Larsen er uddannet cand.scient. i matematik ved Aalborg Universitet i 1982. I 1986 modtog han sin ph.d. i computer science ved University of Edinburgh.

Siden 1993 har Kim Guldstrand Larsen været professor i Computer Science ved Aalborg Universitet.^[2]Han har også været gæsteprofessor et antal steder i verden, bl.a. Det nationale center for IT-forskning i Frankrig (INRIA) (2016-2020) (i form af international chair).^[3][4]

Kim Guldstrand Larsen leder Center for Embedded Software Systems (CISS).^[5] Fra 2007-2011 var han leder af universitets-industri konsortiet Danish Network of Embedded Systems (DaNES), og fra 2011-2017 var han leder af Dansk-Kinesisk Center for IDEA4CPS: Foundations for Cyber-Physical Systems, etableret af Danmarks Grundforskningsfond og Natural Science Foundation of China (NSFC).^[6][7][8]

Derudover var han fra 2009-2020 leder af ICT Innovation Network (InfinIT), fra 2015-2021 var han leder af Innovationsfodens Center for Data-Intensive Cyber-Physical Systems (DiCyPS) og fra 2015-2020 var han leder af Learning, Analysis, SynthesiS and Optimization of Cyber-Physical Systems (LASSO) finansieret af et ERC Advanced Grant.^{[9][10][11][12]}

Kim Guldstrand Larsen er hovedaktør bag det prisvindende værktøj UPPAAL, der er et af de mest udbredte værktøjer til verifikation af realtidsmodeller.^[13][14] "UPPAAL in a Nutshell" skrevet af Kim Guldstrand Larsen og kollegaer er et af de mest citerede papers i The Journal Software Tools for Technology Transfer udgivet af Springer (i den 99. percentil ift. antal citationer).^[15][16]

Han er medlem af Det Kongelige Danske Videnskabernes Selskab og digital vismand i Akademiet for de Tekniske Videnskaber, og han har fungeret som national ekspert for informations- og kommunikationsteknologi temaet under EUs 7. rammeprogram (FP7-ICT), og er i dag medlem af Uddannelses- og Forskningsministeriets referencegruppe for Det digitale område, industrien og rummet under EUs Horizon Europe program.^{[17][18] [19][20]}

Kim Guldstrand Larsen har modtaget en række hædersbevisninger og priser bl.a.:

• Æresdoktor (Honoris causa), Uppsala Uniersitet, 1999^[21]
• Æresdoktor (Honoris causa), Ecole Normal Superieure De Cachan, Paris, 2007^[22]
• Thomson Scientific Award som den mest citerede danske datalog 1990-2004^[23]
• Ridder af Dannebrog, 2007^[24]
• Medlem af Academia Europaea^[25]
• CAV Award 2013^[26]
• ERC Advanced Grant, 2015^[12]
• Grundfos Prize 2016^[27]
• Foreign Expert of China, Distinguished Professor, Northeastern University, 2018^[28]
• Willum Investigator 2021 (30 M DKK) fra Veluxfondene^[29]
• CONCUR Test of Time award 2022^[30]

Kim Guldstrand Larsen har udgivet 6 bøger og mere end 400 peer-reviewed papers og er citeret mange gange (https://scholar.google.dk/citations?user=neDFD60AAAAJ&hl=da). Udvalgte publikationer:

• Larsen, K. G.; Skou, A. (1991). "Bisimulation through probabilistic testing. Information and computation". Information and computation. 94 (1): 1-28. doi:10.1016/0890-5401(91)90030-6.
• UPPAAL in a Nutshell, 1997^[15]
• Cassez, F.; Larsen, K.G (2000). Palamidessi, C. (red.). The Impressive Power of Stopwatches. CONCUR 2000 - Concurrency Theory 11th International Conference. Lecture Notes in Computer Science. Berlin: Springer. s. 138-152. doi:10.1007/3-540-44618-4_12. ISBN 9783540446187. Arkiveret fra originalen (PDF) 2023-07-08.
• Aceto, L.; Ingólfsdóttir, A.; Larsen, K.G.; Srba, J. (2007). Reactive systems: modelling, specification and verification. Cambridge University Press. ISBN 9780521875462.
• Larsen, K.G.; Benveniste, A.; Caillaud, B.; Nickovic, D.; Passerone, R.; Raclet, J.-B.; Reinkemeier, P.; Sangiovanni-Vincentelli, A.; Damm, W.; Henzinger, T.A. (2008). Contracts for System Design. Now Foundations and Research. doi:10.1561/1000000053. ISBN 978-1-68083-403-1.
• David, A.; Larsen, K.G.; Legay, A.; Mikučionis, M.; Bøgsted Poulsen, D. (2015). "Uppaal SMC tutorial". TidsskriftInternational Journal on Software Tools for Technology Transfer. 17 (4): 397-415. doi:10.1007/s10009-014-0361-y.
• Mao, H.; Chen, Y.; Jaeger, M.; Nielsen, T.D.; Larsen, K.G.; Nielsen, B. (2016). "Learning deterministic probabilistic automata from a model checking perspective". Machine Learning. 105 (2): 255-299. doi:10.1007/s10994-016-5565-9.
• Furber, R.; Kozen, D.; Larsen, K.G.; Mardare, R.; Panangaden, P. (2017). "Unrestricted stone duality for Markov processes". 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE Symposium on Logic in Computer Science (LICS). IEEE Press. doi:10.1109/LICS40289.2017.
• Tappler, M.; Aichernig; Bacci, G.; Eichlseder, M.; Larsen, K.G. (2019). "L*-Based Learning of Markov Decision Processes". Formal Methods – The Next 30 Years. International Symposium on Formal Methods. Springer. s. 651-669. doi:10.1007/978-3-030-30942-8_38.
• Cassez, F.; Larsen, K.G. (2019). "Converging from branching to linear metrics on Markov chains". Mathematical Structures in Computer Science. 29 (1): 3-37. doi:10.1017/S0960129517000160.

• Profil ved Aalborg Universitet
• UPPAAL an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata