Офер Стрихман
Офер Стрихман (Офер Штрихман, англ. Ofer Strichman, ивр. עופר שטרייכמן) — израильский учёный, профессор вычислительной логики и компьютерных наук в Технионе[1].
Биография[править]
Родился 4 сентября 1968 года в Хайфе.
Окончил среднюю школу Альянса в 1986 году и присоединился к программе академического резерва Армии Обороны Израиля. Получил степень бакалавра в области промышленного инжиниринга (специализируется на исследованиях операций и информационных системах) в Технионе в 1991 году. Затем 6 лет служил в Армии Обороны Израиля, одновременно получая степень магистра в области исследований операций и информационных систем в Технионе.
После ухода из армии поступил аспирантуру в 1997 году в Институт Вейцмана, где под руководством проф. Амир Пнуэли защитил докторскую диссертацию по теме ‘Efficient decision procedures for validation’.
В 2003 году присоединился к группе информационных систем факультета промышленной инженерии и менеджмента Техниона в качестве старшего преподавателя. Был повышен до адъюнкт-профессора в 2009 году и до полного профессора в 2017 году.
Летом в 2003-2015 годах был приглашенным ученым в Институте разработки программного обеспечения в Питтсбурге. Был консультантом IBM Research в течение 6 лет, начиная с 2004 года. В 2010 году был приглашенным научным сотрудником в Microsoft Research в Редмонде, штат Вашингтон.
Области исследований: формальная верификация и вычислительная логика. Вместе с другим израильским ученым, Бени Годлином, ввёл термин ‘regression verification’ для описания метода доказательства эквивалентности рекурсивных программ и для разработки различных процедур принятия решений (в основном для равенств с неинтерпретированными функциями).
Труды[править]
- Книги
- Decision Procedures - an algorithmic point of view Together with Daniel Kroening. Springer-Verlag, 2008.
- Efficient Decision Procedures for Validation (a re-edited collection of Strichman's PhD publications). LAP Lambert Academic Publishing, 2010.
- Избранные статьи
- Ultimately Incremental SAT. Proc. of the 17th International conference on theory and applications of satisfiability testing (SAT’14). Together with Alexander Nadel and Vadim Ryvchin, 2014.
- Efficient MUS extraction with Resolution. Proc. of the 13th conference on Formal Methods in Computer Aided Design (FMCAD’13). Together with Vadim Ryvchin and Alexander Nadel, 2013.
- Regression verification: Proving the equivalence of similar programs. Software Testing, Verification and Reliability, 23(3) 241–258, 2013. Together with Benny Godlin, 2013.
- Proving mutual termination of programs. Proc. of the eighth Haifa Verification Conference (HVC’12). Together with Dima Elenbogen and Shmuel Katz, 2012.
- Reducing the Size of Resolution Proofs in Linear Time. Journal on Software Tools and Technology Transfer (STTT),vol13, issue 3, page 263, 2011. Together with Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory and Ohad Shacham, 2011.
- A proof producing CSP solver. Proc. of the 24thconference of the Association for the Advancement of Artificial Intelligence (AAAI’10). Together with Michael Veksler, 2010.
- Three optimizations for Assume-Guarantee reasoning with L*. Formal Methods in Systems Design, Vol. 32, number 3, pages 267–284, 2008. Together with Sagar Chaki, 2008.
- Pruning techniques for the SAT-based bounded model checking problem. Proc. of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01), vol. 2144 of Lecture Notes in Computer Science, pages 58 – 70, 2001.
- Tuning SAT checkers for bounded model checking. International Conference on Computer Aided Verification (CAV), 2000, pages 480–494.