オフェル・ストリッチマン

オフェル・ストリッチマン
生まれる	( 1968-09-04 )1968年9月4日（56歳） ハイファ、イスラエル
国籍	イスラエル
母校	テクニオン・ ワイツマン研究所
科学者としてのキャリア
フィールド	コンピュータサイエンス、計算論理
機関	テクニオン
論文	検証のための効率的な意思決定手順 （2001）
博士課程の指導教員	アミール・プヌエリ

オフェル・ストリヒマン（ヘブライ語：עופר שטרייכמן、1968年9月4日生まれ）は、イスラエル工科大学テクニオン校のデイビッドソン産業工学・経営学部の計算論理学およびコンピュータサイエンスの教授である。生産工学のジョセフ・グルエンブラット教授も務めている。^[1]

オフェル・ストリヒマンはハイファで生まれ育った。1986年にアライアンス高校を卒業し、イスラエル国防軍の予備役プログラムに参加した。1991年にテクニオンで産業工学（オペレーションズ・リサーチと情報システム専攻）の理学士号を取得した。その後、テクニオンでオペレーションズ・リサーチと情報システムの理学修士号取得を目指しながら、6年間イスラエル国防軍に勤務した。^[1]

イスラエル国防軍を退役後、1997年にイスラエルのレホヴォトにあるワイツマン研究所でアミール・プヌエリ教授の指導の下、博士課程を開始した。^[2] 専門は形式手法と計算論理で、特にコンパイラの翻訳検証、境界モデル検査、決定手続きであった。論文のタイトルは「検証のための効率的な決定手続き」であった。2001年にエドモンド・クラーク教授の支援の下、カーネギーメロン大学でポスドク研究員となり、モデル検査を専門とした。^[3]

ストリッヒマンは2003年にテクニオンのデータおよび意思決定科学学部の情報システムグループに上級講師として加わった。 2009年に准教授に昇進し、2017年に教授に昇進した。2020年に生産工学のジョセフ・グルエンブラット教授に任命された。^[1]

2003年から2015年にかけて、ストリッチマンは毎年夏にピッツバーグのソフトウェア工学研究所で客員研究員を務めた。 [ 4 ] 2004年^{から6年間、} IBMリサーチのコンサルタントを務めた。2010年にはサバティカル休暇の一環としてワシントン州レドモンドのマイクロソフトリサーチで客員研究員を務めた。^[3]

ストリッヒマン教授の主な研究分野は形式検証と計算論理です。彼は、イスラエルの科学者仲間のベニー・ゴドリンとともに、再帰プログラムの等価性を証明する手法を説明する「回帰検証」という用語を作り出したことや、さまざまな決定手順（主に解釈されていない関数の等価性）を開発したことで知られています。^{[5] [6]} 彼はまた、増分的充足可能性などのSAT解決にも貢献しました。^[7]

ストリッヒマンは2010年にテクニオンのグートヴィルト賞を受賞し、2021年には「充足可能性法理論（SMT）の理論と実践の基礎への先駆的な貢献」によりCAV賞を受賞しました。 ^{[8] [9]} 彼の指導の下で学生が開発したいくつかのソフトウェアツール（SATソルバーとCSPソルバー）は、国際コンテストで金メダルと銀メダルを獲得しました。^{[10] [11] [12] [13]}

• 意思決定手順 - アルゴリズム的観点 ダニエル・クローニング共著Springer-Verlag、2008年。 ^[14]
• 検証のための効率的な意思決定手順（ストリッチマン博士論文集の再編集版）LAP Lambert Academic Publishing、2010年。^[15]

• 究極的に増分的な SAT。満足度テストの理論と応用に関する第 17 回国際会議 (SAT'14) の議事録。Alexander Nadel および Vadim Ryvchin と共著、2014 年。
• Resolution による効率的な MUS 抽出。第 13 回コンピュータ支援設計の形式手法に関する会議 (FMCAD'13) の議事録。Vadim Ryvchin および Alexander Nadel と共著、2013 年。
• 回帰検証：類似プログラムの同等性の証明。ソフトウェアテスト、検証、信頼性、23(3) 241–258、2013年。Benny Godlinと共著、2013年。
• プログラムの相互終了の証明。第 8 回ハイファ検証会議 (HVC'12) 議事録。Dima Elenbogen および Shmuel Katz と共著、2012 年。
• 線形時間での解決証明のサイズの削減。ソフトウェア ツールとテクノロジ移転ジャーナル (STTT)、第 13 巻、第 3 号、263 ページ、2011 年。Omer Bar-Ilan、Oded Fuhrmann、Shlomo Hoory、Ohad Shacham と共著、2011 年。
• 証明を生成する CSP ソルバー。人工知能推進協会 (AAAI'10) 第 24 回会議議事録。Michael Veksler と共著、2010 年。
• L* による Assume-Guarantee 推論の 3 つの最適化。Formal Methods in Systems Design、第 32 巻、第 3 号、267 ～ 284 ページ、2008 年。Sagar Chaki と共著、2008 年。
• SAT ベースの境界モデル検査問題に対する剪定手法。正しいハードウェア設計および検証方法に関する第 11 回先端研究ワーキング カンファレンス (CHARME'01) の議事録、コンピュータ サイエンスの講義ノート第 2144 巻、58 ～ 70 ページ、2001 年。
• 境界モデル検査のためのSATチェッカーのチューニング。国際コンピュータ支援検証会議（CAV）、2000年、480～494ページ。

• オフェル・ストリヒマンのページ、テクニオン
• Ofer Strichman のページ、dblp