Kim Guldstrand Larsen (born 1957) is a Danish scientist and professor of computer science at Aalborg University in Denmark. His research focuses on modeling, validation, and verification of real-time systems. He also studies performance analysis and the development of embedded and cyber-physical systems. His work uses and helps improve concurrency theory and model checking. He has played a key role in creating and improving one of the most widely used verification tools. He has received several awards and honors for his work.

Education

Larsen earned a Master of Science in mathematics from Aalborg University in 1982. In 1986, he received a Doctor of Philosophy in Computer Science from the University of Edinburgh. His PhD advisor was Robin Milner.

Career

Since 1993, Larsen has worked as a professor in Computer Science at Aalborg Universitet. He has also been a visiting professor at several places around the world, including the National Institute for Research in Digital Science and Technology (INRIA), where he held an international chair from 2016 to 2020.

Larsen leads the Center for Embedded Software Systems (CISS). Between 2007 and 2011, he was the director of the university-industry group Danish Network of Embedded Systems (DaNES). From 2011 to 2017, he was the Danish co-lead of the Danish-Chinese Center for IDEA4CPS: Foundations for Cyber-Physical Systems, which was established by the Danish National Research Foundation and the Natural Science Foundation of China (NSFC).

Additionally, he directed the Danish ICT Innovation Network (InfinIT) from 2009 to 2020. He also led the Center for Data-Intensive Cyber-Physical Systems (DiCyPS), which was funded by Innovation Fund Denmark, from 2015 to 2021. From 2015 to 2020, he was the head of the project titled "Learning, Analysis, Synthesis, and Optimization of Cyber-Physical Systems (LASSO)," which was supported by an ERC Advanced Grant.

Larsen is one of the main people behind the award-winning tool UPPAAL, which is widely used for checking real-time models. A paper titled "UPPAAL in a Nutshell," written by Larsen and colleagues, is one of the most frequently cited papers in The Journal of Software Tools for Technology Transfer, published by Springer. It is ranked in the 99th percentile for citations.

He is a member of the Royal Danish Academy of Sciences and Letters. He has also been elected as a fellow and digital expert (vismand) in the Danish Academy of Technical Sciences. He served as the national expert for the Information and Communication Technology theme under the EU's 7th Framework Programme (FP7-ICT). Currently, he is a member of the Digital, Industry, and Space reference group, which supports the Danish Ministry of Higher Education and Science in connection to the EU Horizon Europe program.

Awards and honors (selected)

• Honorary Doctorate, Uppsala University, 1999
• Honorary Doctorate, École normale supérieure Paris-Saclay (previously École normale supérieure de Cachan), Paris, 2007
• Thomson Scientific Award for being the most cited Danish computer scientist, 1990–2004
• Knight of the Order of the Dannebrog, 2007
• Member of Academia Europaea
• CAV Award, 2013
• ERC Advanced Grant, 2015
• Grundfos Prize [da], 2016
• Foreign Expert of China, Distinguished Professor, Northeastern University, 2018
• Villum Investigator 2021 (30 M DKK) from Villum Foundation
• CONCUR Test of Time Award, 2022

Selected works

Larsen has written six books (monographs) and more than 400 peer-reviewed papers. His work has been cited many times (Google Scholar Citation Tracker). Selected works include:

• Larsen, K. G.; Skou, A. (1991). "Bisimulation through probabilistic testing." Information and Computation. 94 (1): 1–28. doi: 10.1016/0890-5401(91)90030-6.
• UPPAAL in a Nutshell, 1997.
• Cassez, F.; Larsen, K.G. (2000). Palamidessi, C. (ed.). The Impressive Power of Stopwatches. CONCUR 2000 – Concurrency Theory 11th International Conference. Lecture Notes in Computer Science. Berlin: Springer. pp. 138–152. doi: 10.1007/3-540-44618-4_12. ISBN 9783540446187. Archived from the original (PDF) on 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." International 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, Bernhard K.; 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. pp. 651–669. arXiv: 1906.12239. doi: 10.1007/978-3-030-30942-8_38.
• Bacci, Giorgio; Bacci, Giovanni; Larsen, K.G.; Mardare, R. (2019). "Converging from branching to linear metrics on Markov chains" (PDF). Mathematical Structures in Computer Science. 29 (1): 3–37. doi: 10.1017/S0960129517000160. S2CID 15996500.