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

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

Офер Стрихман (иврит: עופר שטרייכמן, родился: 4 сентября 1968 г.) — профессор вычислительной логики и информатики в Дэвидсоновском институте промышленной инженерии и менеджмента Техниона — Израильского технологического института. Он занимает должность Йозефа Грюнблата в области технологии производства. ^[1]

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

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

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

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

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

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

Исследовать

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

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

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

Публикации

Книги

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

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

В конечном счете, дополнительный 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* . Формальные методы в проектировании систем, Vol. 32, номер 3, страницы 267–284, 2008 г. Совместно с Сагаром Чаки, 2008 г.
Методы сокращения для задачи проверки ограниченной модели на основе SAT . Учеб. 11-й рабочей конференции перспективных исследований по правильному проектированию и методам проверки аппаратного обеспечения (CHARME'01), том. 2144 Конспектов лекций по информатике, страницы 58–70, 2001 г.
Настройка средств проверки SAT для проверки ограниченной модели . Международная конференция по компьютерной проверке (CAV), 2000 г., страницы 480–494.

Ссылки

^ Jump up to: ^а ^б ^с «Офер Стрихман» . Технион.
^ «Офер Стрихман» . Проект математической генеалогии .
^ Jump up to: ^а ^б «Резюме» (PDF) . Технион.
^ «Публикации Офера Стрихмана» . Институт программной инженерии.
^ Мюллер, Питер; Шефер, Ина (23 октября 2018 г.). Принципиальная разработка программного обеспечения: очерки, посвященные Арнду Петч-Хеффтеру по случаю его 60-летия . Спрингер. ISBN 978-3-319-98047-8 .
^ «Отчеты Карлсруэ по информатике 2015,6 — Регрессионная проверка для программного обеспечения программируемого логического контроллера» . Технологический институт Карлсруэ, Германия . Проверено 20 апреля 2022 г.
^ Стрихман, Офер (2001). Методы сокращения для задачи проверки ограниченной модели на основе SAT . Спрингер. ISBN 978-3-540-44798-6 .
^ «Премия CAV 2021» . КАВ.
^ «Профессор Офер Стрихман получил награду CAV (компьютерная верификация) 2021» . Технион. 4 августа 2021 г.
^ «Конкурс SAT 2011: групповой трек MUS: список решателей» . Университет Артуа .
^ «Конкурс SAT 2011: простой трек MUS: рейтинг решателей» . Университет Артуа.
^ «HCSP — решатель CSP с неклаузальным обучением» . МиниЦинк .
^ «Вызов миницинка» . МиниЦинк.
^ Монахан, Розмари (2018). «Даниэль Кренинг и Офер Стрихман: процедуры принятия решений» (PDF) . Формальные аспекты вычислений . 30 (6): 759. doi : 10.1007/s00165-018-0466-2 . S2CID 51905876 .
^ Эффективные процедуры принятия решений для проверки: проверка перевода, процедуры принятия решений для логики равенства и настройка SAT для проверки ограниченной модели . Академическое издательство LAP Lambert. 15 мая 2010 г. ISBN 978-3838300825 .

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

Страница Офера Стрихмана , Технион
Страница Офера Стрихмана , dblp

[cv-1] Jump up to: ^а ^б ^с «Офер Стрихман» . Технион.

[2] «Офер Стрихман» . Проект математической генеалогии .

[full_cv-3] Jump up to: ^а ^б «Резюме» (PDF) . Технион.

[4] «Публикации Офера Стрихмана» . Институт программной инженерии.

[5] Мюллер, Питер; Шефер, Ина (23 октября 2018 г.). Принципиальная разработка программного обеспечения: очерки, посвященные Арнду Петч-Хеффтеру по случаю его 60-летия . Спрингер. ISBN 978-3-319-98047-8 .

[6] «Отчеты Карлсруэ по информатике 2015,6 — Регрессионная проверка для программного обеспечения программируемого логического контроллера» . Технологический институт Карлсруэ, Германия . Проверено 20 апреля 2022 г.

[7] Стрихман, Офер (2001). Методы сокращения для задачи проверки ограниченной модели на основе SAT . Спрингер. ISBN 978-3-540-44798-6 .

[8] «Премия CAV 2021» . КАВ.

[9] «Профессор Офер Стрихман получил награду CAV (компьютерная верификация) 2021» . Технион. 4 августа 2021 г.

[10] «Конкурс SAT 2011: групповой трек MUS: список решателей» . Университет Артуа .

[11] «Конкурс SAT 2011: простой трек MUS: рейтинг решателей» . Университет Артуа.

[12] «HCSP — решатель CSP с неклаузальным обучением» . МиниЦинк .

[13] «Вызов миницинка» . МиниЦинк.

[14] Монахан, Розмари (2018). «Даниэль Кренинг и Офер Стрихман: процедуры принятия решений» (PDF) . Формальные аспекты вычислений . 30 (6): 759. doi : 10.1007/s00165-018-0466-2 . S2CID 51905876 .

[15] Эффективные процедуры принятия решений для проверки: проверка перевода, процедуры принятия решений для логики равенства и настройка SAT для проверки ограниченной модели . Академическое издательство LAP Lambert. 15 мая 2010 г. ISBN 978-3838300825 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

Базы данных авторитетного контроля
Международный	ВИАФ
Национальный	Германия Израиль
академики	ДБЛП Google Академика MathSciNet Проект математической генеалогии ОРЦИД