Kim Guldstrand Larsen R (born 1957) is a Danish scientist and professor of computer science at Aalborg University, Denmark. His field of research includes modeling, validation and verification, performance analysis, and synthesing of real-time, embedded, and cyber-physical systems utilizing and contributing to concurrency theory and model checking. Within this domain, he has been instrumental in the invention and continuous development of one of the most widely used verification tools, and has received several awards and honors for his work.
Kim Guldstrand Larsen | |
---|---|
Born | |
Nationality | Danish |
Alma mater | University of Edinburgh (PhD) Aalborg University (MSc) |
Known for | Verification of Real-time computing in embedded systems |
Spouse | Merete Kruse Hansen |
Children | 2 daughters |
Awards | CAV Award CONCUR Test of Time Award |
Scientific career | |
Fields | Computer science |
Institutions | Aalborg University |
Website | https://vbn.aau.dk/en/persons/103881 |
Education
editLarsen has an MSc in mathematics from Aalborg University, 1982.[1] In 1986, he received his PhD in Computer Science from University of Edinburgh, advised by Robin Milner.[2]
Career
editSince 1993, Larsen has been a professor in Computer Science at Aalborg Universitet.[3] 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) (as an international chair 2016-2020).[4]
Larsen heads the Center for Embedded Software Systems (CISS).[5] From 2007 to 2011, he was director of the university-industry consortium Danish Network of Embedded Systems (DaNES), and from 2011 to 2017, he was the Danish co-lead of the Danish-Chinese Center for IDEA4CPS: Foundations for Cyber-Physical Systems, established by the Danish National Research Foundation and the Natural Science Foundation of China (NSFC).[6][7][8]
In addition, he was director of the Danish ICT Innovation Network (InfinIT) from 2009 to 2020, director of the Center for Data-Intensive Cyber-Physical Systems (DiCyPS) funded by Innovation Fund Denmark from 2015 to 2021, and head of project on the Learning, Analysis, Synthesis, and Optimization of Cyber-Physical Systems (LASSO) project from 2015 to 2020, funded by an ERC Advanced Grant.[9][10][11][12]
Larsen is one of the key figures behind the award-winning tool UPPAAL, which is one of the most widely used tools for the verification of real-time models.[13][14] "UPPAAL in a Nutshell," written by Larsen and colleagues, is one of the most cited papers in The Journal Software Tools for Technology Transfer, published by Springer (citation rank in the 99th percentile).[15][16]
He is a member of Royal Danish Academy of Sciences and Letters and elected fellow and digital expert (vismand) in the Danish Academy of Technical Sciences . He has served as the national expert for the Information and Communication Technology theme under the EU's 7th Framework Programme (FP7-ICT), and currently he is a member of the Digital, Industry, and Space referencegroup that serves the Danish Ministry of Higher Education and Science in connection to the EU Horizon Europe program.[17][18][19][20]
Awards and honors (selected)
edit- Honorary Doctor (Honoris causa), Uppsala University, 1999[21]
- Honorary Doctor (Honoris causa), École normale supérieure Paris-Saclay (formerly École normale supérieure de Cachan), Paris, 2007[22]
- Thomson Scientific Award as the most cited Danish computer scientist 1990-2004[23]
- Knight of the Order of the Dannebrog, 2007[24]
- Member of 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]
- Villum Investigator 2021 (30 M DKK) from Villum Foundation[29]
- CONCUR Test of Time award 2022[30]
Selected works
editLarsen has published six books (monographs) and more than 400 peer-reviewed papers and he has been cited many times (Google Scholar Citation Tracker). Selected works:
- 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. (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". 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, 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.
References
edit- ^ Computer Science Aalborg University Research Evaluation 1991-1995 (PDF), 1996, p. 59, archived (PDF) from the original on 2023-08-11, retrieved 2023-12-01
- ^ Larsen, Kim Guldstrand (1986). Context-dependent bisimulation between processes (PDF) (PhD thesis). University of Edinburgh.
- ^ Aalborg University Institute of Electronic Systems Department of Mathematics and Computer Science Research Evaluation 1991-1995 (PDF), 1996-05-01, archived from the original (PDF) on 2022-12-05, retrieved 2023-08-09
- ^ Holders of Inria International Chairs (PDF), 2019-11-01, archived from the original (PDF) on 2022-03-08, retrieved 2023-08-09
- ^ CISS Management, archived from the original on 2023-06-04, retrieved 2023-08-10
- ^ DaNES project description, archived from the original on 2022-05-21, retrieved 2023-08-10
- ^ Speakers presentation at the ArtistDesign European Network of Excellence on Embedded Systems Design summer school 2009, archived from the original on 2023-06-10, retrieved 2023-08-10
- ^ Meet the IDEA4CPS researchers, archived from the original on 2023-05-28, retrieved 2023-08-10
- ^ "What is InfinIT?". 2021. Archived from the original on 2022-01-21. Retrieved 2023-08-11.
- ^ DiCyPS in English, archived from the original on 2023-06-02, retrieved 2023-08-11
- ^ The LASSO team, archived from the original on 2023-06-02, retrieved 2023-08-11
- ^ a b CORDIS factsheet on Learning, Analysis, SynthesiS and Optimization of Cyber-Physical Systems, Grant agreement ID: 669844, 2023-05-04, archived from the original on 2023-03-27, retrieved 2023-08-11
- ^ "UPPAAL team". Archived from the original on 2023-08-03. Retrieved 2023-08-11.
- ^ Naeem, A.; Azam, F.; Amjad, A.; Anwar, M.W. (2018). "Comparison of Model Checking Tools Using Timed Automata - PRISM and UPPAAL". 2018 IEEE International Conference on Computer and Communication Engineering Technology (CCET). pp. 248–253. doi:10.1109/CCET.2018.8542231. ISBN 978-1-5386-7437-6. S2CID 53753025.
- ^ a b Larsen, Kim G.; Pettersson, Paul; Yi, Wang (1997). "UPPAAL in a Nutshell". International Journal on Software Tools for Technology Transfer. 1 (1–2): 134–152. doi:10.1007/s100090050010. ISSN 1433-2779.
- ^ Larsen, Kim G.; Pettersson, Paul; Yi, Wang (December 1997), "SpringerNature Citation Details for 'UUPAAL in a Nutshell'", International Journal on Software Tools for Technology Transfer, 1 (1–2): 134–152, doi:10.1007/s100090050010, S2CID 648658, retrieved 2023-08-14
- ^ Members of the Royal Danish Academy of Sciences and Letters, archived from the original on 2020-08-09, retrieved 2023-09-22
- ^ ATV's Digitale Vismandsråd (in Danish), archived from the original on 2023-08-14
- ^ Computer Science, Aalborg University, Research Evaluation 2011-2015 (PDF), archived from the original (PDF) on 2023-08-16, retrieved 2023-08-16
- ^ Medlemmer af referencegruppe for Det digitale område, industrien og rummet (in Danish), archived from the original on 2023-02-06, retrieved 2023-08-16
- ^ Honorary Doctors of the Faculty of Science and Technology, Uppsala University, 2023-06-08, archived from the original on 2023-08-16, retrieved 2023-08-16
- ^ Docteur honoris causa (in French), archived from the original on 2022-05-16, retrieved 2023-08-17
- ^ Research Evaluation 2001–2005, Aalborg University, Department of Computer Science (PDF), 2006-03-01, archived from the original (PDF) on 2023-08-11, retrieved 2023-08-16
- ^ Oversigt over modtagere af danske dekorationer (Directory of recipients of the Order of the Dannebrog) (in Danish), retrieved 2023-08-16
- ^ AE member biography - Kim Guldstrand Larsen, 2012-10-05, archived from the original on 2022-07-07, retrieved 2023-08-17
- ^ International Conference on Computer-Aided Verification, archived from the original on 2023-06-21, retrieved 2023-08-17
- ^ Grundfos Prize Winners, archived from the original on 2023-03-30, retrieved 2023-08-17
- ^ AAU-professor skal rådgive kinesisk premierminister om digitalisering (AAU professor to advise the Chinese Prime Minister on digitalization) (in Danish), 2019-01-21, archived from the original on 2023-08-17, retrieved 2023-08-17
- ^ The Villum Investigators 2021 are fuelled by curiosity, 13 April 2021, archived from the original on 2023-08-20, retrieved 2023-09-24
- ^ Test of Time award, archived from the original on 2023-04-29, retrieved 2023-09-02
External links
edit- Profile at Aalborg University
- UPPAAL an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata