stringtranslate.com

Офер Стрихман

Офер Стрихман (ивр. עופר שטרייכמן, родился 4 сентября 1968 г.) — профессор вычислительной логики и компьютерных наук в Davidson Industrial Engineering and Management , Technion — Израильский технологический институт. Он занимает кафедру Joseph Gruenblat в области производственной инженерии. [1]

Ранняя жизнь и образование

Офер Стрихман родился и вырос в Хайфе . Он окончил среднюю школу Альянса в 1986 году и присоединился к программе академического резерва Армии обороны Израиля . Он получил степень бакалавра в области промышленной инженерии (специализация — исследование операций и информационные системы ) в Технионе в 1991 году. Затем он шесть лет служил в Армии обороны Израиля, одновременно обучаясь на степень магистра в области исследования операций и информационных систем в Технионе. [1]

После ухода из IDF он начал программу PhD в 1997 году в Институте Вейцмана в Реховоте , Израиль, под руководством профессора Амира Пнуэли . [2] Он специализировался на формальных методах и вычислительной логике, а именно на проверке трансляции для компиляторов , проверке ограниченных моделей и процедурах принятия решений. Название его диссертации было «Эффективные процедуры принятия решений для проверки». В 2001 году он начал постдокторантскую должность в Университете Карнеги-Меллона под спонсорством профессора Эдмунда Кларка , где он специализировался на проверке моделей . [3]

Академическая карьера

Стрихман присоединился к группе информационных систем на факультете науки о данных и решениях в Технионе в 2003 году в качестве старшего преподавателя . Он был повышен до доцента в 2009 году и до полного профессора в 2017 году. В 2020 году он был награжден кафедрой Йозефа Грюнблата по производственной инженерии. [1]

В течение каждого лета в 2003–2015 годах Стрихман был приглашенным ученым в Институте программной инженерии в Питтсбурге . [4] Он был консультантом IBM Research в течение 6 лет, по состоянию на 2004 год. В 2010 году он был приглашенным ученым в Microsoft Research в Редмонде, штат Вашингтон , в рамках творческого отпуска . [3]

Исследовать

Основные области исследований профессора Стрихмана — формальная верификация и вычислительная логика. Он, вместе с коллегой-израильским ученым Бенни Годлином, известен тем, что ввел термин «регрессионная верификация» для описания метода доказательства эквивалентности рекурсивных программ, а также разработкой различных процедур принятия решений (в основном для равенств с неинтерпретируемыми функциями). [5] [6] Он также внес вклад в решение SAT, например, в инкрементальную выполнимость. [7]


Почести и награды

В 2010 году Стрихман получил премию Гутвирта от Техниона, а в 2021 году — премию CAV за «новаторский вклад в основы теории и практики модульных теорий выполнимости (SMT)». [8] [9] Несколько программных инструментов (решатель SAT и решатель CSP), разработанных его учениками под его руководством, завоевали золотые и серебряные медали на международных конкурсах. [10] [11] [12] [13]

Публикации

Книги

Избранные статьи

Ссылки

  1. ^ abc "Офер Стрихман". Технион.
  2. ^ "Офер Стрихман". Проект генеалогии математики .
  3. ^ ab "Резюме" (PDF) . Технион.
  4. ^ "Публикации Офера Стрихмана". Институт программной инженерии.
  5. ^ Мюллер, Петер; Шефер, Ина (2018-10-23). ​​Принципиальная разработка программного обеспечения: эссе, посвященные Арнду Пётцш-Хеффтеру по случаю его 60-летия. Springer. ISBN 978-3-319-98047-8.
  6. ^ "Karlsruhe Reports in Informatics 2015,6 - Regression Verification for Programmable Logic Controller Software". Технологический институт Карлсруэ, Германия . Получено 20 апреля 2022 г.
  7. ^ Strichman, Ofer (2001). Методы обрезки для проблемы проверки ограниченной модели на основе SAT. Springer. ISBN 978-3-540-44798-6.
  8. ^ "Премия CAV 2021". CAV.
  9. ^ "Профессор Офер Стрихман получил премию CAV (Computer Aided Verification) 2021". Технион. 4 августа 2021 г.
  10. ^ "Конкурс SAT 2011: групповой трек MUS: список решателей". Университет Артуа .
  11. ^ "Конкурс SAT 2011: простой трек MUS: рейтинг решателей". Университет Артуа.
  12. ^ "HCSP - CSP-решатель с неклаузальным обучением". MiniZinc .
  13. ^ "Вызов MiniZinc". MiniZinc.
  14. ^ Монахан, Розмари (2018). «Даниэль Кренинг и Офер Стрихман: процедуры принятия решений» (PDF) . Формальные аспекты вычислений . 30 (6): 759. doi : 10.1007/s00165-018-0466-2 . S2CID  51905876.
  15. ^ Эффективные процедуры принятия решений для проверки: проверка перевода, процедуры принятия решений для логики равенства и настройка SAT для проверки ограниченной модели . LAP Lambert Academic Publishing. 15 мая 2010 г. ISBN 978-3838300825.

Внешние ссылки