ジョセフ・シファキス

ジョセフ・シファキス（ギリシャ語: Ιωσήφ Σηφάκης、1946年12月26日生まれ）は、ギリシャ系フランス人のコンピュータ科学者である。彼はモデル検査に関する研究で、エドマンド・M・クラーク、E・アレン・エマーソンとともに2007年のチューリング賞を受賞した。

ジョセフ・シファキスは1946年にクレタ島のイラクリオンで生まれ、現在はフランスに住んでいます。彼はフランスの奨学金を受けて、アテネ国立工科大学で電気工学を、グルノーブル大学でコンピュータサイエンスを学びました。 1974年にグルノーブル大学から工学博士号を取得し^{[ 1 ]}、1979年には同大学から国家博士号も授与されました^{[ 2 ] [ 3 ] [ 4 ]。}

彼は現在、グルノーブル近郊のVERIMAG研究所にある国立科学研究センターの名誉研究ディレクターであり、同研究所の創設者でもある。シファキスは、モデル検査と組み込みシステムの分野で指導的な役割を果たしてきた。彼はエドモンド・M・クラークとアミール・プヌエリと共にCAV会議を創設し、1989年にグルノーブルで初めて開催された。彼は組み込みシステム研究のためのARTIST欧州ネットワーク・オブ・エクセレンスのコーディネーターを務めた^{[ 5 ]}（2004年～2012年）。

シファキスはINRIA-シュナイダー寄付産業講座^{[ 6 ]} （2008～2011年）を務め、 EPFLのコンピュータ・通信科学部で正教授^{[ 7 ]} および「厳密システム設計研究所」所長（2011～2016年）を務めた。清華大学（2011～2012年）および南方科技大学（2019年）で客員教授を務めた^{[ 8 ] 。}

シファキス氏は、ギリシャ国立研究技術評議会の会長を務めた（2014年～2016年）。

シファキスはシステム検証とシステム設計への形式手法の応用に取り組んだ。博士号取得のための研究^{[ 3 ]}では、後にモデル検査として知られるアルゴリズム検証手法の原理を研究した。1982年には、この手法がジャン＝ピエール・クエイユの博士論文に適用され、CESAR検証ツールが開発された^{[ 9 ]}。

シファキスは14 年間VERIMAGのディレクターを務めた。当初はCNRSと Verilog SA.の混合産業研究所として設立されたVERIMAG は、エアバスやシュナイダーエレクトリックと協力して、安全性が重要なシステムの開発のための方法とツール、特にLustre 言語に基づく同期プログラミング環境SCADE を開発してきた。シファキスは、トーマス・ヘンジンガー^{[ 10 ] [ 11 ]}と時間制約のあるシステムとハイブリッドシステムの検証に取り組み、アミール・プヌエリとオデッド・マラー^{[ 12 ]}と時間制約のあるシステムの合成に取り組んできた。彼は、IF ツールセット、 Kronos、CADP、 TGVなどの検証ツールの開発に参加し 、抽象化技術を使用して状態爆発に対処するための理論を開発してきた。

過去20年間、彼の研究はBIPコンポーネントフレームワーク^{[ 13 ]}を用いた厳密なコンポーネントベース設計に焦点を当てており、近年では信頼性の高い自律システム、特に自動運転車の設計に取り組んでいる。彼は2022年5月にシュプリンガー社から出版された著書『Understanding and Changing the World』の著者でもある。

• チューリング賞、2007年^{[ 14 ]}
• レオナルド・ダ・ヴィンチ・メダル、2012年^{[ 15 ]}
• フランス国家功労勲章大将校、2008年^{[ 16 ]}
• 2008年、フランス工学アカデミー会員^{[ 17 ]}
• レジオンドヌール勲章コマンドゥール、フランス、2011年^{[ 18 ]}
• フランス科学アカデミー会員、2010年^{[ 19 ]}
• 2008年、ヨーロッパ学術アカデミー会員^{[ 20 ]}
• アメリカ芸術科学アカデミー会員、2015年^{[ 21 ]}
• 全米技術アカデミー会員、2017年^{[ 22 ]}
• 中国科学院外国人会員、2019年^{[ 23 ]}
• 米国科学アカデミー会員、2024年^{[ 24 ]}

• 個人ホームページ
• 公式サイト
• チューリング賞の発表
• 出版物一覧：dblp：ジョセフ・シファキス