Офер Стрихман
Офер Стрихман
Рожденный( 1968-09-04 )4 сентября 1968 г. (56 лет)
Хайфа , Израиль
Национальностьизраильский
Альма-матер Институт Вейцмана Технион
Научная карьера
ПоляИнформатика , вычислительная логика
УчрежденияТехнион
ТезисЭффективные процедуры принятия решений для валидации  (2001)
научный руководительАмир Пнуэли

Офер Стрихман (ивр. עופר שטרייכמן, родился 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]

Публикации

Книги

  • Процедуры принятия решений - алгоритмическая точка зрения Совместно с Даниэлем Кренингом. Springer-Verlag , 2008. [14]
  • Эффективные процедуры принятия решений для валидации (переизданная коллекция публикаций доктора философии Стрихмана). LAP Lambert Academic Publishing , 2010. [15]

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

  • Ultimately Incremental SAT . Труды 17-й Международной конференции по теории и применению тестирования выполнимости (SAT'14). Совместно с Александром Наделем и Вадимом Рывчиным, 2014.
  • Эффективное извлечение MUS с разрешением . Труды 13-й конференции по формальным методам в автоматизированном проектировании (FMCAD'13). Совместно с Вадимом Рывчиным и Александром Наделем, 2013.
  • Регрессионная верификация: Доказательство эквивалентности подобных программ . Тестирование программного обеспечения, верификация и надежность, 23(3) 241–258, 2013. Совместно с Бенни Годлином, 2013.
  • Доказательство взаимного прекращения программ . Труды восьмой Хайфской конференции по проверке (HVC'12). Совместно с Димой Эленбогеном и Шмуэлем Кацем, 2012.
  • Уменьшение размера доказательств разрешений за линейное время . Журнал по программным инструментам и передаче технологий (STTT), т. 13, выпуск 3, стр. 263, 2011. Совместно с Омером Бар-Иланом, Одедом Фурманном, Шломо Хури и Охадом Шахамом, 2011.
  • Решатель CSP-задач, дающий доказательства . Труды 24-й конференции Ассоциации по развитию искусственного интеллекта (AAAI'10). Совместно с Майклом Векслером, 2010.
  • Три оптимизации для рассуждений «Предположение-Гарантия» с L* . Формальные методы в проектировании систем, т. 32, номер 3, страницы 267–284, 2008. Совместно с Сагаром Чаки, 2008.
  • Методы обрезки для проблемы проверки ограниченной модели на основе SAT . Труды 11-й Рабочей конференции передовых исследований по корректному проектированию оборудования и методам верификации (CHARME'01), том 2144 из Lecture Notes in Computer Science, страницы 58–70, 2001.
  • Настройка SAT-контролеров для проверки ограниченной модели . Международная конференция по компьютерной верификации (CAV), 2000, стр. 480–494.

Ссылки

  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.
  • Страница Офера Стрихмана, Технион
  • Страница Офера Стрихмана, dblp
Взято с "https://en.wikipedia.org/w/index.php?title=Ofer_Strichman&oldid=1226042169"