グリゴレ・ロシュ

グリゴレ・ロシュ
2020年のロシュ
生まれる	( 1971-12-12 )1971年12月12日（53歳）
国籍	ルーマニア系アメリカ人
母校	ブカレスト大学 カリフォルニア大学サンディエゴ校
知られている	実行時検証 K言語フレームワーク マッチング ロジック循環共帰
科学者としてのキャリア
フィールド	コンピュータサイエンス
機関	イリノイ大学アーバナ・シャンペーン校 Runtime Verification, Inc. Alexandru Ioan Cuza 大学 Microsoft Research NASA エイムズ研究センター カリフォルニア大学サンディエゴ 校 ブカレスト大学
論文	隠された論理（2000）
博士課程の指導教員	ジョセフ・ゴーゲン
Webサイト	fsl.cs.illinois.edu/~grosu

グリゴレ・ロシュ（1971年12月12日生まれ）は、イリノイ大学アーバナ・シャンペーン校のコンピュータサイエンス 教授であり、Information Trust Instituteの 研究員である。^[1]彼は、ランタイム検証、Kフレームワーク、^[2] マッチングロジック、^[3] および自動コインダクション における貢献で知られている。^[4]

ロシュは、1995年にルーマニアのブカレスト大学で数学の学士号、 1996年にコンピューティングの基礎の修士号を取得し、 2000年にカリフォルニア大学サンディエゴ校でコンピュータサイエンスの博士号を取得しました。2000年から2002年にかけて、 NASAエイムズ研究センターの研究員を務めました。2002年に、イリノイ大学アーバナシャンペーン校のコンピュータサイエンス学部に助教授として加わりました。2008年に准教授、2014年に教授になりました。^[1]

• IEEE/ACM 2016年国際自動ソフトウェア工学会議（ASE）最優秀論文賞^[5]（ASE 2001論文^[6]）
• 実行時検証（RV）テスト賞^[7]（RV 2001論文^[8]）
• ASE 2008、ASE 2016、OOPSLA 2016 でACM 優秀論文賞^{[9] を受賞}
• ETAPS 2002における最優秀ソフトウェア科学論文賞^[10]
• 2005年NSFキャリア賞^[11]

• 2016年のAd AStra賞^[12]

RoșuはHavelund ^[13]と共同で「ランタイム検証」という用語を作り出した。これは、形式検証とテスト の境界にある問題に取り組むことを目的とした ワークショップ^{[14]の名前である。Roșuと彼の協力者は、パラメトリックプロパティモニタリング[15]} 、効率的なモニター合成^[16]、^[17] 、 およびモニタリング指向プログラミング[18]のアルゴリズムと技術を導入した。Roșuは また、ランタイム検証技術の商業化を目的とした会社、Runtime Verification, Inc.を設立した。^{[19 ]}

^{Roșuは、Kフレームワーク[2]}の設計と開発を考案し、主導しました。Kフレームワークは、設定、計算、書き換えルールを使用してプログラミング言語、 型システム、形式分析ツールが定義される実行可能な 意味論的フレームワークです。インタープリタ、 仮想マシン、コンパイラ、シンボリック実行、形式検証ツールなどの言語ツールは、Kフレームワークによって自動的または半自動的に生成されます。C 、^[20]、Java、^[21]、JavaScript、^[22]、Python、^[23] 、Ethereum仮想マシン^[24]など、いくつかの既知のプログラミング言語の形式意味論は 、Kフレームワークを使用して定義されています 。

Roșuは、 Kフレームワークとプログラミング言語、 仕様、検証 の基礎としてマッチングロジック^[3]を導入しました。マッチングロジックは、一階述語論理と数学的帰納法を組み合わせたものと同じくらい表現力があり、代数仕様と初期代数意味論、最小固定点を持つ一階述語論理^{[25] 、}型付きまたは型なしラムダ計算、 依存型システム、 再帰述語を持つ分離論理、書き換え論理^{[26] [27]} Hoare論理、時相論理、 動的論理、様相μ計算など、非常に重要ないくつかの形式システムを構文糖衣としてコンパクトな表記法で表現しています。

Roșuの博士論文^[28]では、 隠れた論理の文脈における共帰納法の自動化として、循環共帰納法^{[29]が提案された。これはさらに、}帰納法と共帰納法の両方による証明を統合して自動化する原理へと一般化され、 Coq ^[30]、Isabelle/HOL ^[31]、Dafny ^[32]、 およびCIRC定理証明器^[33]の一部として実装されている。

• ホームページ
• リンクトイン
• 出版物（Google、DBLP）