Григоре Рошу

Григоре Рошу
Григоре Рошу
	Красный в 2020 году
Рожденный	12 декабря 1971 г. (52 года)
Национальность	румынско-американский
Альма-матер	Университет Бухареста ; Калифорнийский университет, Сан-Диего
Известный	Проверка времени выполнения ; Языковая структура K ; соответствующая логика ; круговая коиндукция
	Научная карьера
Поля	Информатика
Учреждения	Университет Иллинойса в Урбана-Шампейн ; Проверка времени выполнения, Inc. ; Университет Александру Иоана Кузы ; Microsoft Исследования ; Исследовательский центр НАСА Эймса ; Калифорнийский университет в Сан-Диего ; Университет Бухареста
Диссертация	Скрытая логика (2000)
Докторантура	Джозеф Гоген
Веб-сайт	фсл .cs .Иллинойс .edu /~толстый

Григоре Рошу (родился 12 декабря 1971 г.) — информатики профессор Иллинойского университета в Урбана-Шампейн и исследователь в области Институт информационного доверия . ^{[ 1 ]} Он известен своим вкладом в проверку времени выполнения , K framework, ^{[ 2 ]} соответствие логике, ^{[ 3 ]} и автоматизированная коиндукция . ^{[ 4 ]}

Биография

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

Награды

Награда IEEE/ACM за самый влиятельный документ Международной конференции по автоматизированной разработке программного обеспечения (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 ]} Рошу также основал Runtime Verification, Inc., компания, стремящаяся коммерциализировать технологию проверки времени выполнения. ^{[ 19 ]}

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

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

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

Ссылки

^ Jump up to: ^а ^б Григоре Рошу Биографическая справка
^ Jump up to: ^а ^б К-фреймворк. https://kframework.org
^ Jump up to: ^а ^б Соответствующая логика. https://matching-logic.org
^ Автоматизированная коиндукция. https://fsl.cs.illinois.edu/index.php/Circ
^ Самые влиятельные статьи по автоматизированной разработке программного обеспечения. https://ase-conferences.org/Mip.html
^ К. Хавелунд, Г. Розу. 2001, Программы мониторинга с использованием перезаписи , Автоматизированная разработка программного обеспечения (ASE), стр. 135–143.
^ Проверка времени выполнения. https://runtime-verification.org/
^ К. Хавелунд, Г. Розу. 2001, Мониторинг Java-программ с помощью Java PathExplorer , Электронные заметки по теоретической информатике, том. 55(2), стр. 200–217.
^ ACM SIGSOFT отмечена бумажными наградами. https://sigsoft.org/awards/distinguishedPaperAward.html
^ Европейская ассоциация по изучению науки и технологий. https://easst.aulp.co.uk/awards-to-date
^ Поиск награды NSF: Award#0448501 — КАРЬЕРА: Проверка и мониторинг среды выполнения. https://nsf.gov/awardsearch/showAward?AWD_ID=0448501
^ Григоре Рошу | Награды Ad Astra. https://premii.ad-astra.ro/?p=314
^ Домашняя страница Клауса Хавелунда. https://havelund.com/
^ Международная конференция по верификации времени выполнения. https://runtime-verification.org
^ Г. Росу, Ф. Чен. 2012, Семантика и алгоритмы параметрического мониторинга. Логические методы в информатике (LMCS), том. 8 (1), стр. 1–47.
^ П. Мередит, Д. Джин, Ф. Чен, Г. Рошу. 2010, Эффективный мониторинг параметрических бесконтекстных шаблонов. Журнал автоматизированной разработки программного обеспечения, том. 17(2), стр. 149–180.
^ Ф. Чен, Т. Сербанута, Г. Рошу. 2008, jPredictor: инструмент прогнозного анализа времени выполнения для Java. Международная конференция по программной инженерии (ICSE), стр. 221–230.
^ Мониторинг-ориентированное программирование. https://fsl.cs.illinois.edu/index.php/Monitoring-Oriented_Programming
^ Runtimve Verification Inc.
^ К. Хэтхорн, К. Эллисон, Г. Розу. 2015, Определение неопределенности C В Трудах по проектированию и реализации языков программирования (PLDI), стр. 336-345.
^ Д. Богданас, Г. Рошу. 2015, K-Java: полная семантика Java В Трудах по принципам языков программирования (POPL), стр. 445-456.
^ Д. Парк, А. Стефанеску, Г. Рошу. 2015, KJS: полная формальная семантика JavaScript В Трудах по проектированию и реализации языков программирования (PLDI), стр. 346-356.
^ Д. Гут. 2013 г., кандидатская диссертация, Формальная семантика Python 3.3 Университет Иллинойса в Урбана-Шампейн.
^ Э. Хильденбрандт, М. Саксена, К. Чжу, Н. Родригес, П. Даян, Д. Гут, Б. Мур, Ю. Чжан, Д. Парк, А. Стефанеску, Г. Рошу. 2018, KEVM: полная семантика виртуальной машины Ethereum В Трудах Фонда компьютерной безопасности (CSF), стр. 204-217.
^ Ю. Гуревич, С. Шелах. 1985, Расширения логики первого порядка с фиксированной точкой В Трудах основ компьютерных наук (SFCS), стр. 346-353.
^ Ж. Мезегер. 2012, Двадцать лет переписывания логики В Журнале логического и алгебраического программирования (JLAP) том. 81(7-8), стр. 721-781.
^ Переписывание логики и систем, https://csl.sri.com/programs/rewriting/
^ Г. Розу. 2000, доктор философии диссертация Скрытая логика Калифорнийский университет в Сан-Диего.
^ Г. Рошу, Д. Лукану. 2009, Круговая коиндукция: теоретическая основа доказательств. В Трудах по алгебре и коалгебре в информатике (CALCO), стр. 127-144.
^ Дж. Эндруллис, Д. Хендрикс, М. Боден. Круговая коиндукция в Coq с использованием методов бисимуляции до достижения результата Международная конференция по интерактивному доказательству теорем, стр. 354-369.
^ Д. Хаусманн, Т. Моссаковски, Л. Шредер. Итеративная круговая коиндукция CoCasl в Isabelle/HOL Международная конференция по фундаментальным подходам к программной инженерии, стр. 341-356.
^ К. Рустан М. Лейно, М. Москаль. Просто коиндукция — автоматическое коиндуктивное доказательство в верификаторе программ Международный симпозиум по формальным методам, стр. 382-398.
^ Лаборатория формальных систем | Цирк Прувер. https://fsl.cs.illinois.edu/index.php/Circ

Внешние ссылки

[cv-1] Jump up to: ^а ^б Григоре Рошу Биографическая справка

[k-2] Jump up to: ^а ^б К-фреймворк. https://kframework.org

[ml-3] Jump up to: ^а ^б Соответствующая логика. https://matching-logic.org

[circ-4] Автоматизированная коиндукция. https://fsl.cs.illinois.edu/index.php/Circ

[5] Самые влиятельные статьи по автоматизированной разработке программного обеспечения. https://ase-conferences.org/Mip.html

[6] К. Хавелунд, Г. Розу. 2001, Программы мониторинга с использованием перезаписи , Автоматизированная разработка программного обеспечения (ASE), стр. 135–143.

[7] Проверка времени выполнения. https://runtime-verification.org/

[8] К. Хавелунд, Г. Розу. 2001, Мониторинг Java-программ с помощью Java PathExplorer , Электронные заметки по теоретической информатике, том. 55(2), стр. 200–217.

[9] ACM SIGSOFT отмечена бумажными наградами. https://sigsoft.org/awards/distinguishedPaperAward.html

[10] Европейская ассоциация по изучению науки и технологий. https://easst.aulp.co.uk/awards-to-date

[11] Поиск награды NSF: Award#0448501 — КАРЬЕРА: Проверка и мониторинг среды выполнения. https://nsf.gov/awardsearch/showAward?AWD_ID=0448501

[12] Григоре Рошу | Награды Ad Astra. https://premii.ad-astra.ro/?p=314

[13] Домашняя страница Клауса Хавелунда. https://havelund.com/

[rvconf-14] Международная конференция по верификации времени выполнения. https://runtime-verification.org

[15] Г. Росу, Ф. Чен. 2012, Семантика и алгоритмы параметрического мониторинга. Логические методы в информатике (LMCS), том. 8 (1), стр. 1–47.

[16] П. Мередит, Д. Джин, Ф. Чен, Г. Рошу. 2010, Эффективный мониторинг параметрических бесконтекстных шаблонов. Журнал автоматизированной разработки программного обеспечения, том. 17(2), стр. 149–180.

[17] Ф. Чен, Т. Сербанута, Г. Рошу. 2008, jPredictor: инструмент прогнозного анализа времени выполнения для Java. Международная конференция по программной инженерии (ICSE), стр. 221–230.

[mop-18] Мониторинг-ориентированное программирование. https://fsl.cs.illinois.edu/index.php/Monitoring-Oriented_Programming

[19] Runtimve Verification Inc.

[20] К. Хэтхорн, К. Эллисон, Г. Розу. 2015, Определение неопределенности C В Трудах по проектированию и реализации языков программирования (PLDI), стр. 336-345.

[21] Д. Богданас, Г. Рошу. 2015, K-Java: полная семантика Java В Трудах по принципам языков программирования (POPL), стр. 445-456.

[22] Д. Парк, А. Стефанеску, Г. Рошу. 2015, KJS: полная формальная семантика JavaScript В Трудах по проектированию и реализации языков программирования (PLDI), стр. 346-356.

[23] Д. Гут. 2013 г., кандидатская диссертация, Формальная семантика Python 3.3 Университет Иллинойса в Урбана-Шампейн.

[24] Э. Хильденбрандт, М. Саксена, К. Чжу, Н. Родригес, П. Даян, Д. Гут, Б. Мур, Ю. Чжан, Д. Парк, А. Стефанеску, Г. Рошу. 2018, KEVM: полная семантика виртуальной машины Ethereum В Трудах Фонда компьютерной безопасности (CSF), стр. 204-217.

[25] Ю. Гуревич, С. Шелах. 1985, Расширения логики первого порядка с фиксированной точкой В Трудах основ компьютерных наук (SFCS), стр. 346-353.

[26] Ж. Мезегер. 2012, Двадцать лет переписывания логики В Журнале логического и алгебраического программирования (JLAP) том. 81(7-8), стр. 721-781.

[27] Переписывание логики и систем, https://csl.sri.com/programs/rewriting/

[28] Г. Розу. 2000, доктор философии диссертация Скрытая логика Калифорнийский университет в Сан-Диего.

[29] Г. Рошу, Д. Лукану. 2009, Круговая коиндукция: теоретическая основа доказательств. В Трудах по алгебре и коалгебре в информатике (CALCO), стр. 127-144.

[30] Дж. Эндруллис, Д. Хендрикс, М. Боден. Круговая коиндукция в Coq с использованием методов бисимуляции до достижения результата Международная конференция по интерактивному доказательству теорем, стр. 354-369.

[31] Д. Хаусманн, Т. Моссаковски, Л. Шредер. Итеративная круговая коиндукция CoCasl в Isabelle/HOL Международная конференция по фундаментальным подходам к программной инженерии, стр. 341-356.

[32] К. Рустан М. Лейно, М. Москаль. Просто коиндукция — автоматическое коиндуктивное доказательство в верификаторе программ Международный симпозиум по формальным методам, стр. 382-398.

[33] Лаборатория формальных систем | Цирк Прувер. https://fsl.cs.illinois.edu/index.php/Circ

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ 24 ]

[ 25 ]

[ 26 ]

[ 27 ]

[ 28 ]

[ 29 ]

[ 30 ]

[ 31 ]

[ 32 ]

[ 33 ]

Базы данных авторитетного контроля
Международный	ЯВЛЯЮТСЯ 2 ВИАФ WorldCat
Национальный	Соединенные Штаты Чешская Республика Нидерланды Израиль
академики	ОРЦИД Ассоциация вычислительной техники Google Академика ДБЛП