stringtranslate.com

Grigore Roşu

Grigore Roșu (nacido el 12 de diciembre de 1971) 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 coincidencia, [3] y la coinducción automatizada . [4]

Biografía

Roșu obtuvo 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 doctorado 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 unió al departamento de ciencias de la computación en la Universidad de Illinois en Urbana-Champaign como profesor asistente . Se convirtió en profesor asociado en 2008 y profesor titular en 2014. [1]

Premios

Contribuciones

Roșu 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 problemas en el límite entre la verificación formal y las pruebas . Roșu y sus colaboradores introdujeron algoritmos y técnicas para el monitoreo de propiedades paramétricas, [15] síntesis de monitores eficientes, [16] análisis predictivo en tiempo de ejecución , [17] y programación orientada al monitoreo. [18] Roșu también fundó Runtime Verification, Inc., una empresa destinada a comercializar tecnología de verificación en tiempo de ejecución. [19]

Roșu 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 formal 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.

Roșu introdujo la lógica de emparejamiento [3] como base para el marco K y para los lenguajes de programación , especificación y verificación . Es tan expresiva 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 los mínimos puntos fijos , [25] los cálculos lambda tipados o no tipados , los sistemas de tipos dependientes , la lógica de separación con predicados recursivos , la lógica de reescritura, [26] [27] la lógica de Hoare , las lógicas temporales , la lógica dinámica y el μ-cálculo modal .

La tesis doctoral de Roșu [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 implementó en Coq , [30] Isabelle/HOL , [31] Dafny , [32] y como parte del demostrador de teoremas CIRC. [33]

Referencias

  1. ^ ab Currículum vitae de Grigore Rosu
  2. ^ Marco de K ab. https://kframework.org
  3. ^ ab Lógica de emparejamiento. https://matching-logic.org
  4. ^ Coinducción automatizada. https://fsl.cs.illinois.edu/index.php/Circ
  5. ^ Artículos más influyentes sobre ingeniería de software automatizada. https://ase-conferences.org/Mip.html
  6. ^ K. Havelund, G. Rosu. 2001, Monitoreo de programas mediante reescritura, Ingeniería de software automatizada (ASE), págs. 135-143.
  7. ^ Verificación en tiempo de ejecución. https://runtime-verification.org/
  8. ^ K. Havelund, G. Rosu. 2001, Monitoreo de programas Java con Java PathExplorer, Notas electrónicas en ciencias de la computación teórica vol. 55(2), pp. 200-217.
  9. ^ Premios ACM SIGSOFT a los artículos destacados. https://sigsoft.org/awards/distinguishedPaperAward.html
  10. ^ Asociación Europea para el Estudio de la Ciencia y la Tecnología. https://easst.aulp.co.uk/awards-to-date
  11. ^ Búsqueda de premios de la NSF: Premio n.º 0448501 - CARRERA: Verificación y monitoreo en tiempo de ejecución. https://nsf.gov/awardsearch/showAward?AWD_ID=0448501
  12. ^ Grigore Roșu | Premiile Ad Astra. https://premii.ad-astra.ro/?p=314
  13. ^ Página de inicio de Klaus Havelund. https://havelund.com/
  14. ^ Conferencia internacional sobre verificación en tiempo de ejecución. https://runtime-verification.org
  15. ^ 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.
  16. ^ 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.
  17. ^ F. Chen, T. Serbanuta, G. Rosu. 2008, jPredictor: una herramienta de análisis predictivo en tiempo de ejecución para Java Conferencia internacional sobre ingeniería de software (ICSE), págs. 221–230.
  18. ^ Programación orientada al monitoreo. https://fsl.cs.illinois.edu/index.php/Monitoring-Oriented_Programming
  19. ^ Verificación Runtimve Inc.
  20. ^ C. Hathhorn, C. Ellison, G. Rosu. 2015, Definición de la indefinición de C en Actas de Diseño e Implementación de Lenguajes de Programación (PLDI), págs. 336-345.
  21. ^ D. Bogdanas, G. Rosu. 2015, K-Java: una semántica completa de Java en Actas de Principios de lenguajes de programación (POPL), págs. 445-456.
  22. ^ D. Park, A. Stefanescu, G. Rosu. 2015, KJS: Una semántica formal completa de JavaScript en Actas de Diseño e Implementación de Lenguajes de Programación (PLDI), págs. 346-356.
  23. ^ D. Guth. 2013, tesis de maestría, Una semántica formal de Python 3.3 Universidad de Illinois en Urbana-Champaign.
  24. ^ 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 Actas de Computer Security Foundations (CSF), págs. 204-217.
  25. ^ 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.
  26. ^ J. Meseguer. 2012, Veinte años de reescritura de la lógica en el Journal of Logic and Algebraic Programming (JLAP), vol. 81(7-8), pp. 721-781.
  27. ^ Reescribiendo lógicas y sistemas, https://csl.sri.com/programs/rewriting/
  28. ^ G. Rosu. 2000, Tesis doctoral Lógica Oculta Universidad de California San Diego.
  29. ^ G. Rosu, D. Lucanu. 2009, Coinducción circular: una base teórica de prueba en Actas de Álgebra y Coálgebra en Ciencias de la Computación (CALCO), págs. 127-144.
  30. ^ J. Endrullis, D. Hendriks, M. Bodin. Coinducción circular en Coq usando técnicas de bisimulación hasta la Conferencia internacional sobre demostración interactiva de teoremas, págs. 354-369.
  31. ^ D. Hausmann, T. Mossakowski, L. Schroder. Coinducción circular iterativa para CoCasl en Isabelle/HOL International Conference on Fundamental Approaches to Software Engineering, págs. 341-356.
  32. ^ K. Rustan M. Leino, M. Moskal. Co-inducción Simplemente - Pruebas co-inductivas automáticas en un verificador de programas Simposio internacional sobre métodos formales, págs. 382-398.
  33. ^ Laboratorio de sistemas formales | Circ Prover. https://fsl.cs.illinois.edu/index.php/Circ

Enlaces externos