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