Григоре Росу - Grigore Rosu

Григоре Росу
Фотография Григоре Росу, сделанная в 2020.jpg
Rosu в 2020 году
Родившийся (1971-12-12) 12 декабря 1971 г. (48 лет)
НациональностьРумынско-американский
Альма-матерБухарестский университет
Калифорнийский университет в Сан-Диего
ИзвестенПроверка во время выполнения
Языковая структура K
логика сопоставления
круговая коиндукция
Научная карьера
ПоляИнформатика
УчрежденияИллинойсский университет в Урбана-Шампейн
Runtime Verification, Inc.
Университет Александру Иоан Куза
Microsoft Research
Исследовательский центр НАСА Эймса
Калифорнийский университет в Сан-Диего
Бухарестский университет
ТезисСкрытая логика (2000)
ДокторантДжозеф Гогуэн
Интернет сайтфсл.cs.illinois.edu/ ~ grosu

Григоре Рогу это Информатика профессор на Иллинойсский университет в Урбана-Шампейн и Исследователь в Институт информационного доверия.[1] Он известен своим вкладом в проверка во время выполнения, Каркас K,[2]логика сопоставления,[3]и автоматизированное производство.[4]

биография

Росу получил Б.А. в Математика в 1995 году и РС. в Основах вычислительной техники в 1996 г. Бухарестский университет, Румыния и Кандидат наук. в Информатика в 2000 году из Калифорнийский университет в Сан-Диего. С 2000 по 2002 гг. Он был научным сотрудником в Исследовательский центр НАСА Эймса. В 2002 году он поступил на кафедру информатики в Иллинойсский университет в Урбана-Шампейн как доцент. Он стал Доцент в 2008 году и полный профессор в 2014.[1]

Награды

  • Самый влиятельный документ IEEE / ACM в номинации Automate Software Engineering (ASE) в 2016 году[5] (для статьи ASE 2001[6])
  • Проверка времени выполнения (RV), награда за испытание временем[7] (для бумаги RV 2001[8])
  • Почетные награды ACM[9] на ASE 2008, ASE 2016 и OOPSLA 2016
  • Премия за лучшую научную работу в области программного обеспечения на ETAPS 2002[10]
  • Награда NSF CAREER в 2005 году[11]
  • Премия Ad AStra в 2016 году[12]

Взносы

Рошу ввел термин "проверка во время выполнения "вместе с Хавелундом[13]как название мастерской[14]началось в 2001 году с целью решения проблем на границе между формальная проверка и тестирование. Росу и его сотрудники представили алгоритмы и методы параметрического мониторинга свойств,[15]эффективный синтез монитора,[16] прогнозный анализ во время выполнения,[17]и ориентированное на мониторинг программирование.[18]Rosu также основала Runtime Verification, Inc., компанию, нацеленную на коммерциализацию технологии проверки времени выполнения.[19]

Рошу создал и руководил проектированием и разработкой платформы K,[2] который является исполняемым семантический рамки, где языки программирования, системы типов, и формальный анализ инструменты определяются с помощью конфигураций, вычисления, и переписать правила. Языковые инструменты, такие как переводчики, виртуальные машины, компиляторы, символическая казнь и формальная проверка инструменты, автоматически или полуавтоматически генерируются платформой K. Формальная семантика нескольких известных языков программирования, таких как C,[20]Ява,[21]JavaScript,[22]Python,[23]и Виртуальная машина Ethereum[24]определены с использованием платформы K.

Rosu представила логику сопоставления[3]в качестве основы для K framework и для языки программирования, Технические характеристики, и проверка. Это так же выразительно, как логика первого порядка плюс математическая индукция, и использует компактную нотацию для обозначения в качестве синтаксического сахара нескольких формальные системы критически важны, такие как алгебраическая спецификация и начальная алгебра семантика, логика первого порядка с наименьшие фиксированные точки,[25]типизированные или нетипизированные лямбда-исчисления, системы зависимого типа, логика разделения с рекурсивными предикатами, переписывая логику,[26][27]Логика Хоара, темпоральная логика, динамическая логика, и модальное μ-исчисление.

Rosu's Кандидат наук. Тезис[28] предложенная круговая коиндукция[29]как автоматизация коиндукции в контексте скрытой логики. В дальнейшем это было обобщено в принцип, который объединяет и автоматизирует доказательства обоими индукция и коиндукция, и был реализован в Coq,[30]Изабель / ХОЛ,[31]Дафни,[32]и как часть средства доказательства теорем CIRC.[33]

Рекомендации

  1. ^ а б Григоре Рошу Биография Резюме
  2. ^ а б Каркас К. http://www.kframework.org
  3. ^ а б Логика соответствия. http://www.matching-logic.org
  4. ^ Автоматическая коиндукция. http://fsl.cs.illinois.edu/index.php/Circ
  5. ^ Наиболее влиятельные статьи в области автоматизированной разработки программного обеспечения.http://ase-conferences.org/Mip.html
  6. ^ К. Хавелунд, Г. Рошу. 2001, Мониторинг программ с использованием перезаписи, Автоматизированная разработка программного обеспечения (ASE), стр. 135-143.
  7. ^ Проверка во время выполнения.https://www.runtime-verification.org/
  8. ^ К. Хавелунд, Г. Рошу. 2001, Мониторинг программ Java с помощью Java PathExplorer, Электронные заметки по теоретической информатике, том. 55 (2), стр. 200-217.
  9. ^ Почетные бумажные награды ACM SIGSOFT.https://www.sigsoft.org/awards/distinguishedPaperAward.html
  10. ^ Европейская ассоциация изучения науки и технологий.http://easst.aulp.co.uk/awards-to-date
  11. ^ Поиск награды NSF: Награда № 0448501 - КАРЬЕРА: Проверка и мониторинг времени выполнения.https://www.nsf.gov/awardsearch/showAward?AWD_ID=0448501
  12. ^ Григоре Рогу | Premiile Ad Astra.http://premii.ad-astra.ro/?p=314
  13. ^ Домашняя страница Клауса Хавелунда. https://www.havelund.com/
  14. ^ Международная конференция по верификации времени выполнения. http://runtime-verification.org
  15. ^ Г. Рошу, Ф. Чен. 2012, Семантика и алгоритмы параметрического мониторинга Логические методы в компьютерных науках (LMCS), т. 8 (1), стр. 1–47.
  16. ^ П. Мередит, Д. Джин, Ф. Чен, Г. Рошу. 2010, Эффективный мониторинг параметрических контекстно-свободных шаблонов Журнал автоматизированной программной инженерии, вып. 17 (2), стр. 149-180.
  17. ^ Ф. Чен, Т. Сербанута, Г. Рошу, 2008, г. jPredictor: инструмент прогнозирующего анализа времени выполнения для Java Международная конференция по программной инженерии (ICSE), стр. 221–230.
  18. ^ Программирование, ориентированное на мониторинг. http://fsl.cs.illinois.edu/index.php/Monitoring-Oriented_Programming
  19. ^ Runtimve Verification Inc.
  20. ^ К. Хатхорн, К. Эллисон, Г. Росу, 2015 г.,Определение неопределенности C В Proceedings of Programming Language Design and Implementation (PLDI), стр. 336-345.
  21. ^ Д. Богданас, Г. Рошу. 2015,K-Java: полная семантика Java В Proceedings of Principles of Programming Languages ​​(POPL), стр. 445-456.
  22. ^ Д. Парк, А. Стефанеску, Г. Рошу, 2015, г.KJS: полная формальная семантика JavaScript В Proceedings of Programming Language Design and Implementation (PLDI), стр. 346-356.
  23. ^ Д. Гут, 2013, М. Тезис,Формальная семантика Python 3.3 Университет Иллинойса в Урбане-Шампейн.
  24. ^ Э. Хильденбрандт, М. Саксена, X. Чжу, Н. Родригес, П. Дайан, Д. Гут, Б. Мур, Ю. Чжан, Д. Парк, А. Стефанеску, Г. Рошу. 2018,KEVM: полная семантика виртуальной машины Ethereum В Proceedings of Computer Security Foundation (CSF), стр. 204-217.
  25. ^ Ю. Гуревич, С. Шелах.1985, г.Расширения с фиксированной точкой логики первого порядка В Трудах основ информатики (SFCS), стр. 346-353.
  26. ^ J. Meseguer.2012,Двадцать лет переписывания логики В Журнале логики и алгебраического программирования (JLAP), т. 81 (7-8), стр. 721-781.
  27. ^ Переписывая логику и системы,http://www.csl.sri.com/programs/rewriting/
  28. ^ G. Rosu. 2000 г., канд. ТезисСкрытая логика Калифорнийский университет в Сан-Диего.
  29. ^ Г. Рошу, Д. Лукану, 2009 г., Круговая коиндукция: доказательная теоретическая основа В Proceedings of Algebra and Coalgebra in Computer Science (CALCO), стр. 127-144.
  30. ^ Дж. Эндруллис, Д. Хендрикс, М. Боден.Циркулярная коиндукция в Coq с использованием методов бисимуляции-до Международная конференция по интерактивному доказательству теорем, стр. 354-369.
  31. ^ Д. Хаусманн, Т. Мосаковски, Л. Шредер.Итеративная круговая коиндукция для CoCasl в Isabelle / HOL Международная конференция по фундаментальным подходам к разработке программного обеспечения, стр. 341-356.
  32. ^ К. Рустан, М. Лейно, М. Москаль.Коиндукция просто - автоматические коиндуктивные доказательства в программном верификаторе Международный симпозиум по формальным методам, стр. 382-398.
  33. ^ Лаборатория формальных систем | Circ Prover. http://fsl.cs.illinois.edu/index.php/Circ

внешняя ссылка