ジェラルド・J・ホルツマン

ジェラルド・J・ホルツマン
ジェラルド・J・ホルツマン 2006
生まれる	1951 （1951年） アムステルダム、オランダ
母校	デルフト工科大学
知られている	SPINモデルチェッカーの開発
受賞歴	パリ・カネラキス賞 （2005年）
科学者としてのキャリア
フィールド	モデル検査
機関	ベル研究所
博士課程の指導教員	ウィレム・ファン・デル・プールとJLデ・クロース

ジェラルド・J・ホルツマン（1951年生まれ）は、ベル研究所とNASAに所属するオランダ系アメリカ人のコンピュータ科学者、研究者であり、 SPINモデルチェッカーの開発者として最もよく知られています。^[1]

ホルツマンはオランダのアムステルダムで生まれ、1976年にデルフト工科大学で電気工学の学士号を取得しました。その後、 1979年にデルフト大学でウィレム・ファン・デル・ポールおよびJL・デ・クロースの指導の下、 「マルチプロセッシングシステムにおける調整問題」と題する論文で博士号も取得しました。フルブライト奨学金を受けた後、南カリフォルニア大学でさらに1年間大学院生として過ごし、ペル・ブリンチ・ハンセンとともに研究を行いました。

1980年にマレーヒルのベル研究所に1年間勤務。オランダに戻り、デルフト工科大学で2年間助教授を務めた。 ^{[2] 1983年に}ベル研究所に戻り、コンピューティング科学研究センター（旧Unix研究グループ）で働いた。2003年に NASAに入社し、カリフォルニア州パサデナのNASA JPL 高信頼ソフトウェア研究所^[3]を率いており、JPLフェローでもある。^[1]

1981年、ホルツマンはオランダ王立技術者協会からバーラー教授賞を受賞した。^[2] 2001年、彼は計算機協会（ACM）からソフトウェアシステム賞（SPINに対して）に選ばれた。2002年には、ACM SIGSOFT優秀研究賞に選ばれた。^[4] 2005年にはパリ・カネラキス理論と実践賞に選ばれた。 ^[1]彼はソフトウェア検証のためのモデル検査システムの作成により、2005年に米国工学アカデミーの会員に選出された。 ^{[5] 2011年には}計算機協会のフェローに就任した。^[6]彼は2012年10月にNASA例外的工学功績メダルを受賞した。 ^[1] 2015年にはIEEEハーラン・D・ミルズ賞を受賞した。^[7]

ホルツマンは、1980年代にベル研究所でSPINモデルチェッカー（SPINはSimple Promela Interpreterの略）を開発したことで知られています。このデバイスは並行ソフトウェアの正当性を検証することができ、1991年から無料で利用可能です。

出版物、抜粋：^[8]

• Spin Model Checker — 入門およびリファレンスマニュアル、 Addison - Wesley、2003年。ISBN 0-321-22862-6 。
• コンピュータプロトコルの設計と検証、Prentice Hall、1991年。
• データネットワークの初期の歴史、IEEE Computer Society Press、1995 年。
• 『Beyond Photography — The Digital Darkroom』、Prentice Hall、1988年。ISBN 0-13-074410-7。 

• 計算機協会フェロー一覧

• ホームページ
• インタビュー