Kim Guldstrand Larsen - Enciclopedia

Kim Guldstrand Larsen R (nacido en 1957) es un científico danés y profesor de ciencias de la computación en la Universidad de Aalborg, Dinamarca. Su campo de investigación incluye modelado, validación y verificación, análisis de rendimiento y síntesis de sistemas de tiempo real, embebidos y ciberfísicos, utilizando y contribuyendo a la teoría de la concurrencia y la verificación de modelos. Dentro de este dominio, ha sido fundamental en la invención y el desarrollo continuo de uno de los herramientas de verificación más ampliamente utilizados, y ha recibido varios premios y honores por su trabajo.


Educación
Larsen tiene un máster en matemáticas de la Universidad de Aalborg, 1982. En 1986, recibió su doctorado en Ciencias de la Computación de la Universidad de Edimburgo, bajo la orientación de Robin Milner.


Carrera
Desde 1993, Larsen ha sido profesor de Ciencias de la Computación en la Universidad de Aalborg. También ha sido profesor visitante en varios lugares del mundo, incluyendo el Instituto Nacional de Investigación en Ciencias y Tecnologías Digitales (INRIA) (como catedrático internacional 2016-2020).
Larsen lidera el Centro de Sistemas de Software Embebido (CISS). De 2007 a 2011, fue director del consorcio universidad-industria Danish Network of Embedded Systems (DaNES), y de 2011 a 2017, fue el co-líder danés del Danish-Chinese Center for IDEA4CPS: Fundamentos para Sistemas Ciberfísicos, establecido por la Fundación Nacional de Investigación de Dinamarca y la Fundación de Ciencias Naturales de China (NSFC).
Además, fue director de la Red Danesa de Innovación en TIC (InfinIT) de 2009 a 2020, director del Centro para Sistemas Ciberfísicos de alta densidad de datos (DiCyPS) financiado por el Fondo de Innovación de Dinamarca de 2015 a 2021, y jefe del proyecto sobre el Aprendizaje, Análisis, Síntesis y Optimización de Sistemas Ciberfísicos (LASSO) del 2015 al 2020, financiado por una subvención ERC Advanced Grant.
Larsen es una de las figuras clave detrás del galardonado herramienta UPPAAL, que es una de las herramientas más ampliamente utilizadas para la verificación de modelos de tiempo real. "UPPAAL en una Cascarilla", escrito por Larsen y colegas, es uno de los artículos más citados en The Journal Software Tools for Technology Transfer, publicado por Springer (posición en el 99º percentile).
Es miembro de la Real Academia Danesa de Ciencias y Letras y fue elegido miembro y experto digital (vismand) en la Academia Danesa de Ciencias Técnicas. Ha servido como experto nacional para el tema de Tecnologías de la Información y la Comunicación bajo el programa marco 7 de la UE (FP7-ICT), y actualmente es miembro del grupo de referencia Digital, Industria y Espacio que asiste al Ministerio de Educación Superior y Ciencia de Dinamarca en relación con el programa de la UE Horizonte Europa.


Premios y honores (selección)
Doctor Honoris Causa, Universidad de Uppsala, 1999
Doctor Honoris Causa, École normale supérieure Paris-Saclay (anteriormente École normale supérieure de Cachan), París, 2007
Premio Thomson Scientific como el científico danés más citado de 1990-2004
Caballero de la Orden de los Símbolos Daneses, 2007
Miembro de Academia Europaea
Premio CAV 2013
Subvención ERC Advanced Grant, 2015
Premio Grundfos 2016
Experto Extranjero de China, Profesor Distinguido, Universidad de Northeastern, 2018
Becario Villum 2021 (30 M DKK) de la Fundación Villum
Premio CONCUR Test of Time 2022


Obras seleccionadas
Larsen ha publicado seis libros (monografías) y más de 400 artículos revisados por pares y ha sido citado muchas veces (Google Scholar Citation Tracker). Obras seleccionadas:

Larsen, K. G.; Skou, A. (1991). "Bisimulación a través de pruebas probabilísticas. Information and Computation". Information and Computation. 94 (1): 1–28. doi:10.1016/0890-5401(91)90030-6.
UPPAAL en una Cascarilla, 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". 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.


Referencias


Enlaces externos
Perfil en la Universidad de Aalborg
UPPAAL, un entorno de herramienta integrado para el modelado, validación y verificación de sistemas de tiempo real modelados como redes de autómatas temporizados.