Grigore Roșu es profesor de informática en la Universidad de Illinois en Urbana-Champaign e investigador del Information Trust Institute . [1] Es conocido por sus contribuciones en la verificación en tiempo de ejecución , el marco K, [2] la lógica de emparejamiento, [3] y la coinducción automatizada. [4]
Grigore Rosu | |
---|---|
Nació | 12 de diciembre de 1971 |
Nacionalidad | Rumano-americano |
alma mater | Universidad de Bucarest Universidad de California, San Diego |
Conocido por | Verificación en tiempo de ejecución Marco de lenguaje K coincidencia lógica de coinducción circular |
Carrera científica | |
Campos | Ciencias de la Computación |
Instituciones | Universidad de Illinois en Urbana-Champaign Runtime Verification, Inc. Universidad Alexandru Ioan Cuza Investigación de Microsoft Centro de investigación Ames de la NASA Universidad de California en San Diego Universidad de Bucarest |
Tesis | Lógica oculta (2000) |
Asesor de doctorado | Joseph Goguen |
Sitio web | fsl |
Biografía
Rosu recibió una licenciatura en Matemáticas en 1995 y una maestría en Fundamentos de Computación en 1996, ambas de la Universidad de Bucarest , Rumania, y un Ph.D. en Ciencias de la Computación en 2000 de la Universidad de California en San Diego . Entre 2000 y 2002 fue científico investigador en el Centro de Investigación Ames de la NASA . En 2002, se incorporó al departamento de informática de la Universidad de Illinois en Urbana-Champaign como profesor asistente . Se convirtió en profesor asociado en 2008 y profesor titular en 2014. [1]
Premios
- IEEE / ACM artículo más influyente del premio Automate Software Engineering (ASE) en 2016 [5] (para un artículo ASE 2001 [6] )
- Prueba de adjudicación de tiempo de verificación de tiempo de ejecución (RV) [7] (para un artículo de RV 2001 [8] )
- Premios de papel distinguidos de ACM [9] en ASE 2008, ASE 2016 y OOPSLA 2016
- Premio al mejor artículo científico de software en ETAPS 2002 [10]
- Premio NSF CAREER en 2005 [11]
- Premio Ad AStra en 2016 [12]
Contribuciones
Rosu acuñó el término " verificación en tiempo de ejecución " junto con Havelund [13] como el nombre de un taller [14] iniciado en 2001, con el objetivo de abordar los problemas en la frontera entre la verificación formal y las pruebas . Rosu y sus colaboradores introdujeron algoritmos y técnicas para el monitoreo de propiedades paramétricas, [15] síntesis de monitoreo eficiente, [16] análisis predictivo en tiempo de ejecución , [17] y programación orientada al monitoreo. [18] Rosu también ha fundado Runtime Verification, Inc., una empresa destinada a comercializar tecnología de verificación en tiempo de ejecución. [19]
Rosu creó y dirigió el diseño y desarrollo del marco K, [2] que es un marco semántico ejecutable donde los lenguajes de programación , los sistemas de tipos y las herramientas de análisis formales se definen utilizando configuraciones, cálculos y reglas de reescritura . Las herramientas de lenguaje, como intérpretes , máquinas virtuales , compiladores , ejecución simbólica y herramientas de verificación formal , son generadas de forma automática o semiautomática por el marco K. La semántica formal de varios lenguajes de programación conocidos, como C , [20] Java , [21] JavaScript , [22] Python , [23] y Ethereum Virtual Machine [24] se definen utilizando el marco K.
Rosu introdujo la lógica de emparejamiento [3] como base para el marco K y para los lenguajes de programación , la especificación y la verificación . Es tan expresivo como la lógica de primer orden más la inducción matemática , y utiliza una notación compacta para capturar, como azúcar sintáctico, varios sistemas formales de importancia crítica, como la especificación algebraica y la semántica del álgebra inicial , la lógica de primer orden con menos puntos fijos , [25] cálculos lambda tipados o no tipados , sistemas de tipos dependientes , lógica de separación con predicados recursivos , lógica de reescritura, [26] [27] lógica Hoare , lógica temporal , lógica dinámica y cálculo μ modal .
Ph.D. de Rosu La tesis [28] propuso la coinducción circular [29] como una automatización de la coinducción en el contexto de la lógica oculta. Esto se generalizó aún más en un principio que unifica y automatiza las demostraciones tanto por inducción como por coinducción , y se ha implementado en Coq , [30] Isabelle / HOL , [31] Dafny , [32] y como parte del demostrador del teorema CIRC. [33]
Referencias
- ^ a b Currículum vitae de Grigore Rosu
- ^ a b K marco. http://www.kframework.org
- ^ a b Lógica coincidente. http://www.matching-logic.org
- ^ Coinducción automatizada. http://fsl.cs.illinois.edu/index.php/Circ
- ^ Artículos más influyentes de la ingeniería de software automatizada. http://ase-conferences.org/Mip.html
- ^ K. Havelund, G. Rosu. 2001, Programas de seguimiento mediante reescritura , Ingeniería de software automatizada (ASE), págs. 135-143.
- ^ Verificación de tiempo de ejecución. https://www.runtime-verification.org/
- ^ K. Havelund, G. Rosu. 2001, Monitorización de programas Java con Java PathExplorer , Notas electrónicas en informática teórica vol. 55 (2), págs. 200-217.
- ^ Premios al papel distinguido ACM SIGSOFT. https://www.sigsoft.org/awards/distinguishedPaperAward.html
- ^ Asociación europea para el estudio de la ciencia y la tecnología. http://easst.aulp.co.uk/awards-to-date
- ^ Búsqueda de premios de la NSF: Premio n. ° 0448501 - CARRERA: Verificación y supervisión del tiempo de ejecución. https://www.nsf.gov/awardsearch/showAward?AWD_ID=0448501
- ^ Grigore Roșu | Premiile Ad Astra. http://premii.ad-astra.ro/?p=314
- ^ Página de inicio de Klaus Havelund. https://www.havelund.com/
- ^ Conferencia internacional de verificación en tiempo de ejecución. http://runtime-verification.org
- ^ G. Rosu, F. Chen. 2012, Semántica y algoritmos para métodos lógicos de monitoreo paramétrico en ciencias de la computación (LMCS), vol. 8 (1), págs. 1-47.
- ^ P. Meredith, D. Jin, F. Chen, G. Rosu. 2010, Monitoreo eficiente de patrones paramétricos libres de contexto Journal of Automated Software Engineering, vol. 17 (2), págs. 149-180.
- ↑ F. Chen, T. Serbanuta, G. Rosu. 2008, jPredictor: una herramienta de análisis de tiempo de ejecución predictivo para Java International Conference on Software Engineering (ICSE), págs. 221–230.
- ^ Programación orientada a la supervisión. http://fsl.cs.illinois.edu/index.php/Monitoring-Oriented_Programming
- ^ Verificación de Runtimve Inc.
- ↑ C. Hathhorn, C. Ellison, G. Rosu. 2015, Definición de la indefinición de C en procedimientos de diseño e implementación de lenguajes de programación (PLDI), págs. 336-345.
- ↑ D. Bogdanas, G. Rosu. 2015, K-Java: Una semántica completa de Java en Proceedings of Principles of Programming Languages (POPL), págs. 445-456.
- ↑ D. Park, A. Stefanescu, G. Rosu. 2015, KJS: Una semántica formal completa de JavaScript en procedimientos de diseño e implementación de lenguajes de programación (PLDI), págs. 346-356.
- ^ D. Guth. 2013, tesis de maestría, una semántica formal de Python 3.3 Universidad de Illinois en Urbana-Champaign.
- ↑ E. Hildenbrandt, M. Saxena, X. Zhu, N. Rodrigues, P. Daian, D. Guth, B. Moore, Y. Zhang, D. Park, A. Stefanescu, G. Rosu. 2018, KEVM: Una semántica completa de la máquina virtual Ethereum en procedimientos de Computer Security Foundations (CSF), págs.204-217.
- ^ Y. Gurevich, S. Shelah. 1985, Extensiones de punto fijo de la lógica de primer orden en Proceedings of Foundations of Computer Science (SFCS), págs. 346-353.
- ^ J. Meseguer. 2012, Veinte años reescribiendo la lógica en el Journal of Logic and Algebraic Programming (JLAP), vol. 81 (7-8), págs. 721-781.
- ^ Reescritura de lógicas y sistemas, http://www.csl.sri.com/programs/rewriting/
- ^ G. Rosu. 2000, Ph.D. tesis Hidden Logic de la Universidad de California en San Diego.
- ↑ G. Rosu, D. Lucanu. 2009, Coinducción circular: una base teórica de prueba en Actas de álgebra y álgebra en ciencias de la computación (CALCO), págs. 127-144.
- ^ J. Endrullis, D. Hendriks, M. Bodin. Coinducción circular en Coq usando técnicas de bisimulación hasta la fecha Conferencia internacional sobre demostración interactiva de teoremas, págs. 354-369.
- ^ D. Hausmann, T. Mossakowski, L. Schroder. Coinducción circular iterativa para CoCasl en Isabelle / HOL International Conference on Fundamental Approaches to Software Engineering, pp. 341-356.
- ↑ K. Rustan M. Leino, M. Moskal. Co-inducción simplemente: pruebas co-inductivas automáticas en un simposio internacional de verificadores de programas sobre métodos formales, págs. 382-398.
- ^ Laboratorio de sistemas formales | Circ Prover. http://fsl.cs.illinois.edu/index.php/Circ
enlaces externos
- Página de inicio
- Publicaciones ( Google , DBLP )