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

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

バイオグラフィー

ロシュは、1995年にルーマニアのブカレスト大学で数学の学士号、 1996年にコンピューティング基礎の修士号を取得し、2000年にカリフォルニア大学サンディエゴ校でコンピュータサイエンスの博士号を取得しました。

博士号を取得後、 2000 年にNASAのエイムズ研究センターの研究科学者として入社し、飛行およびナビゲーション ソフトウェアの形式仕様と検証に注力し、ミッション クリティカルなシステムの信頼性を高めるために「ランタイム検証」という用語を生み出しました。

2002年にイリノイ大学アーバナ・シャンペーン校のコンピュータサイエンス学部に助教授として着任し、その後2008年に准教授、2014年に教授となった。

2003 年、ロシュは学生のTraian Serbanutaとともに、プログラミング言語の形式意味を定義する直感的でモジュール式のアプローチを提供する K フレームワークを開発しました。

彼は 2010 年に Runtime Verification, Inc. を設立し、組み込みシステム分野の ボーイングやトヨタなどの業界リーダーと協力して、自身の研究を実際のアプリケーションに変換しました。

2023 年後半、彼はプログラミング言語の相互運用性と計算の信頼性における課題の解決を目指し、Runtime Verification からのスピンオフとして Pi Squared, Inc.を設立しました。

受賞歴

貢献

ロシュはハヴェルンド[ 15 ]と共同で「実行時検証」という用語を考案しました。これは、形式検証とテストの 境界にある問題に取り組むことを目的としたワークショップ[ 16 ] の名称です。ロシュと彼の共同研究者は、パラメトリックプロパティモニタリング[ 17 ] 、効率的なモニター合成[ 18 ] 、実行時予測分析[ 19 ]、 モニタリング指向プログラミング[ 20 ]のためのアルゴリズムと技術を導入しました。

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

RoșuはKフレームワークとプログラミング言語、 仕様記述、検証 の基礎としてマッチング論理[ 3 ]を導入した。マッチング論理は一階述語論理と数学的帰納法を組み合わせたものと同様の表現力を持ち、簡潔な記法を用いて、代数仕様記述や初期代数意味論、最小固定点を持つ一階述語論理[ 26 ]、型付きまたは型なしのラムダ計算、 依存型システム、 再帰述語を持つ分離論理、書き換え論理[ 27 ] 、 [ 28 ] 、ホーア論理、時相論理、 動的論理、様相μ計算といった、極めて重要ないくつかの形式体系を構文糖衣として表現している。

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

参考文献

  1. ^グリゴレ・ロシュの
  2. ^ a b Kフレームワーク。https ://kframework.org
  3. ^ a b マッチングロジック。https ://matching-logic.org
  4. ^ 自動コインダクション。https ://fsl.cs.illinois.edu/index.php/Circ
  5. ^ 自動ソフトウェアエンジニアリングに関する最も影響力のある論文。https ://ase-conferences.org/Mip.html
  6. ^ K. Havelund、G. Rosu、2001、「書き換えを使用したプログラムの監視」、Automated Software Engineering (ASE)、pp. 135-143。
  7. ^ Havelund, Klaus; Roşu, Grigore (2001-10-01). 「Java PathExplorerによるJavaプログラムの監視」 . Electronic Notes in Theoretical Computer Science . RV'2001, Runtime Verification (in connection with CAV '01). 55 (2): 200– 217. doi : 10.1016/S1571-0661(04)00253-1 . hdl : 2060/20020051234 . ISSN  1571-0661 .
  8. ^ 「Awards」 .ランタイム検証. 2025年3月24日閲覧。
  9. ^ ACM SIGSOFT 優秀論文賞。https ://sigsoft.org/awards/distinguishedPaperAward.html
  10. ^ 欧州科学技術協会。https ://easst.aulp.co.uk/awards-to-date
  11. ^ NSF Award Search: Award#0448501 - CAREER: ランタイム検証および監視。https ://nsf.gov/awardsearch/showAward? AWD_ID=0448501
  12. ^ グリゴレ・ロシュ |プレミアアド・アストラ。 https://premii.ad-astra.ro/?p=314
  13. ^ 2021 IEEEコンピュータソサエティフェロー
  14. ^ 「2022 AAASフェロー | アメリカ科学振興協会（AAAS）」 www.aaas.org . 2025年3月24日閲覧。
  15. ^ クラウス・ハヴェルンドのホームページ。https ://havelund.com/
  16. ^ ランタイム検証に関する国際会議。https ://runtime-verification.org
  17. ^ G. Rosu, F. Chen. 2012、「パラメトリックモニタリングのためのセマンティクスとアルゴリズム、 コンピュータサイエンスにおける論理的手法 (LMCS)」、vol.8(1)、pp.1–47。
  18. ^ P. Meredith、D. Jin、F. Chen、G. Rosu。2010、「パラメトリックコンテキストフリーパターンの効率的な監視」 Journal of Automated Software Engineering、vol. 17(2)、pp. 149-180。
  19. ^ F. Chen、T. Serbanuta、G. Rosu、2008、「jPredictor: Java の予測実行時分析ツール」、 International Conference on Software Engineering (ICSE)、pp. 221–230。
  20. ^ モニタリング指向プログラミング。https ://fsl.cs.illinois.edu/index.php/Monitoring-Oriented_Programming
  21. ^ C. Hathhorn、C. Ellison、G. Rosu、2015、「 Cの未定義性の定義」 、プログラミング言語の設計と実装の議事録(PLDI)、pp. 336-345。
  22. ^ D. Bogdanas、G. Rosu、2015、 「K-Java: Javaの完全なセマンティクス」、 Proceedings of Principles of Programming Languages (POPL)、pp. 445-456。
  23. ^ D. Park、A. Stefanescu、G. Rosu、2015、 「KJS: JavaScript の完全な形式意味論」 『プログラミング言語の設計と実装 (PLDI) の議事録』、pp. 346-356。
  24. ^ D. Guth. 2013、修士論文、 Python 3.3 の形式意味論、 イリノイ大学アーバナシャンペーン校。
  25. ^ E. Hildenbrandt、M. Saxena、X. Zhu、N. Rodrigues、P. Daian、D. Guth、B. Moore、Y. Zhang、D. Park、A. Stefanescu、G. Rosu。2018、 「KEVM：Ethereum仮想マシンの完全なセマンティクス」 、Computer Security Foundations（CSF）の論文集、pp. 204-217。
  26. ^ Y. Gurevich, S. Shelah. 1985、 「第一階論理の固定小数点拡張」 『コンピュータサイエンスの基礎 (SFCS) の議事録』346-353 ページ。
  27. ^ J. Meseguer. 2012、 「論理の書き換え20年」 、Journal of Logic and Algebraic Programming (JLAP)、vol. 81(7-8)、pp. 721-781。
  28. ^ 論理とシステムの書き換え、 https://csl.sri.com/programs/rewriting/
  29. ^ G. Rosu. 2000年、Ph.D. 論文 、Hidden Logic、 カリフォルニア大学サンディエゴ校。
  30. ^ G. Rosu, D. Lucanu、2009、「Circular Coinduction: 証明理論的基礎」 、Proceedings of Algebra and Coalgebra in Computer Science (CALCO)、pp. 127-144。
  31. ^ J. Endrullis、D. Hendriks、M. Bodin。Coq における循環共帰納法、双模倣法を用いた技術、 インタラクティブ定理証明に関する国際会議、pp. 354-369。
  32. ^ D. Hausmann, T. Mossakowski, L. Schroder. Isabelle/HOLにおけるCoCaslの反復的循環共帰納法、 ソフトウェア工学への基本的アプローチに関する国際会議、pp. 341-356。
  33. ^ K. Rustan M. Leino、M. Moskal. Co-induction Simply - プログラム検証における自動Co-inductive証明、 International Symposium on Formal Methods、pp. 382-398。
  34. ^ 形式システム研究所 | Circ 証明器。https ://fsl.cs.illinois.edu/index.php/Circ
「 https://en.wikipedia.org/w/index.php?title=Grigore_Roșu&oldid=1322468437」から取得