ラディア・クーソット

ラディア・クーソット
生まれる	( 1947-08-06 )1947年8月6日 サキエット・シディ・ユセフ、チュニジア
死亡	2014年5月1日(2014-05-01)（67歳） ニューヨーク市
市民権	フランス語
母校	ロレーヌ国立工科大学
知られている	抽象的解釈
配偶者	パトリック・クソ
受賞歴	ACM SIGPLANプログラミング言語功績賞 IEEE コンピュータ協会Harlan D. Mills 賞
科学者としてのキャリア
フィールド	コンピュータサイエンス
論文	不変性と運命の並行プログラムの方法の財団 (1985)
博士課程の指導教員	クロード・ペア

ラディア・クゾー（1947年8月6日 - 2014年5月1日）^[1]は、抽象解釈を発明したことで知られるフランスのコンピュータ科学者でした。

ラディア・クゾーは1947年8月6日、チュニジアのサキエット・シディ・ユセフに生まれ、1958年2月8日に学校で起きた児童虐殺を生き延びた。その後、スースの女子高等学校、アルジェのフランス高等学校、アルジェ工科学校（成績1位で唯一の女性）に進学した。専攻は数学的最適化と整数線形計画法だった。ユネスコのフェローシップ（1972～1975年）の支援を受けて、1972年にグルノーブルのジョセフ・フーリエ大学でコンピュータサイエンスの修士号（DEA）を取得した。1985年にナンシーでクロード・ペール [fr]の指導の下、数学の博士号を取得した。^{[注 1]}

ラディア・クゾーは、グルノーブルのジョセフ・フーリエ大学のIMAG研究所（1975～1979年）の准研究科学者に任命され、1980年以降は、フランス国立科学研究センターのアンリ・ポアンカレ大学（1980～1983年）、オルセーのパリ第1大学（1984～1988年）、エコール・ポリテクニーク（1989～2008年）のコンピュータサイエンス研究所（1991年以降は「意味論、証明、抽象解釈」研究チームを率いた）、エコール・ノルマル・シュペリュール（2006～2014年）のジュニア研究科学者、研究科学者、上級研究科学者、名誉上級研究科学者として勤務しました。

ラディア・クーゾは夫のパトリックとともに抽象解釈^{[2] [3]}の創始者であり、形式手法における影響力のある技術である。抽象解釈は3つの主要なアイデアに基づいている。

1. コンピュータ システム上のあらゆる推論/証明/静的分析は、ある抽象レベルでその実行可能性を記述するセマンティクスを指します。
2. 推論/証明/静的分析では、推論に関係のないすべての意味プロパティを抽象化する必要があります。
3. 決定不能性のため、コンピュータ システムに関する健全で完全に自動化された、常に終了する推論/証明/静的分析は、抽象的に数学的帰納法を実行する必要があり、近似値しか得られません (有限性と決定可能性の仮説があっても、小さなシステムを超えると組み合わせ爆発が起こるため)。

ラディア・クーゾットは論文の中で、並行プログラムと並列プログラムの意味論、証明、静的解析手法を発展させた。^[4]

ラディア・クゾーは1999年1月に エアバス社とコンタ​​クトを取り、 2001年以降、エコール・ノルマル・シュペリュール^[5]で開発され、現在は静的解析を専門とするドイツのソフトウェア会社AbsInt GmbH[6]によって配布されている組み込み制御/^コマンドソフトウェアの健全な静的プログラム解析ツールであるAstréeランタイムエラーアナライザーの開発につながりました。Astréeは、輸送、宇宙、医療ソフトウェア業界で使用されています。

彼女はパトリック・クゾーとともに、 2013年にACM SIGPLANプログラミング言語功績賞 ^[7]を受賞し、2014年には「抽象解釈の発明、ツールサポートの開発、およびその実用化」 によりIEEEコンピュータソサエティの ハーラン・D・ミルズ賞^[8]を受賞しました。

2014年9月以来、ラディア・クーゾ最優秀若手研究者論文賞^[9]は、静的解析シンポジウム（SAS） ^[10]のプログラム委員会を代表してプログラム委員長によって毎年授与されています。

• 2014 (ミュンヘン、ドイツ): Aleksandar Chakarov (コロラド大学、ボルダー、コロラド州、米国)、確率的プログラムループの期待不変量を固定点として(Sriram Sankaranarayanan と共著)、M. Müller-Olm および H. Seidl (編): SAS 2014、LNCS 8723、pp. 85–100、Springer
• 2015 (フランス、サン・マロ)：マリアンナ・ラポポート（ウォータールー大学、カナダ、オンタリオ州）、相関メソッド呼び出しがある場合の正確なデータフロー分析、（オンドレイ・ロタックおよびフランク・ティップとの共著）、S. ブレイジー＆T. ジェンセン（編）：SAS 2015、LNCS 9291、pp. 54–71、シュプリンガー
• 2016 (エディンバラ、スコットランド): Stefan Schulze Frielinghaus (ミュンヘン工科大学、ドイツ)、手続き間分析の強制終了、(Helmut Seidl および Ralf Vogler と共同)、Xavier Rival (編): SAS 2016、LNCS 9837、pp. 447– 468、スプリンガー
• 2017 (ニューヨーク、ニューヨーク、米国): Suvam Mukherjee (インド科学研究所、バンガロール、インド) および Oded Padon (テルアビブ大学、イスラエル)、スレッドローカルセマンティクスとレースフリープログラムのための効率的なシーケンシャル抽象化、(Sharon Shoham、Deepak D'Souza、Noam Rinetzky との共著)、Francesco Ranzato (編): SAS 2017、LNCS 10422、pp 253–276、Springer

• エコールノルマル高等学院の Radhia Cousot ホームページ
• 略歴
• 高等師範学校におけるラディア・クゾーの出版物
• エコールノルマル高等専門学校でラディア・クーゾ賞を受賞
• CNRSの情報科学相互作用科学研究所におけるラディア・クーゾの格差
• DBLP書誌サーバーの Radhia Cousot
• 数学系譜プロジェクトの Radhia Cousot