Ofer Strichman

Ofer Strichman
Urodzić się	( 04.09.1968 ) 4 września 1968 Hajfa , Izrael
Narodowość	izraelski
Alma Mater	Instytut Technion Weizmanna
Kariera naukowa
Pola	Informatyka , logika obliczeniowa
Instytucje	Technion
Praca dyplomowa	Efektywne procedury decyzyjne do walidacji (2001)
Doradca doktorski	Amira Pnueli

Ofer Strichman ( hebrajski : עופר שטרייכמן , urodzony: 4 września 1968) jest profesorem logiki obliczeniowej i informatyki w Davidson Industrial Engineering and Management , Technion - Israel Institute of Technology . Zajmuje katedrę Josepha Gruenblata w inżynierii produkcji.

Wczesne życie i edukacja

Ofer Strichman urodził się i wychował w Hajfie . Ukończył liceum Alliance w 1986 roku i dołączył do programu rezerw akademickich IDF . Uzyskał tytuł licencjata w dziedzinie inżynierii przemysłowej (ze specjalizacją w badaniach operacyjnych i systemach informacyjnych ) w Technion w 1991 roku. Następnie służył przez sześć lat w IDF, jednocześnie studiując w Technion, aby uzyskać tytuł magistra w dziedzinie badań operacyjnych i systemów informacyjnych.

Po odejściu z IDF rozpoczął studia doktoranckie w 1997 roku w Instytucie Weizmanna w Rehovot w Izraelu pod kierunkiem prof. Amira Pnueli . Specjalizował się w metodach formalnych i logice obliczeniowej, aw szczególności w walidacji tłumaczeń dla kompilatorów , Bounded Model Checking i procedurach decyzyjnych. Jego praca dyplomowa brzmiała „Wydajne procedury decyzyjne do walidacji”. W 2001 roku rozpoczął staż podoktorancki na Carnegie Mellon University pod patronatem prof. Edmunda Clarke'a , gdzie specjalizował się w sprawdzanie modeli .

Kariera akademicka

Strichman dołączył do grupy systemów informatycznych na Wydziale Inżynierii Przemysłowej i Zarządzania Technion w 2003 roku jako starszy wykładowca . Tytuł profesora nadzwyczajnego uzyskał w 2009 r., a profesora zwyczajnego w 2017 r. W 2020 r. otrzymał katedrę im. Josepha Gruenblata na wydziale inżynierii produkcji.

Każdego lata w latach 2003-2015 Strichman był naukowcem wizytującym w Software Engineering Institute w Pittsburghu . Był konsultantem IBM Research przez 6 lat, począwszy od 2004 r. W 2010 r. był naukowcem wizytującym w Microsoft Research w Redmond w stanie Waszyngton w ramach urlopu naukowego .

Badania

Główne obszary badawcze prof. Strichmana to weryfikacja formalna i logika obliczeniowa. On, wraz z innym izraelskim naukowcem Bennym Godlinem, jest znany z ukucia terminu „weryfikacja regresji” w celu opisania techniki udowadniania równoważności programów rekurencyjnych oraz z opracowywania różnych procedur decyzyjnych (głównie dla równości z niezinterpretowanymi funkcjami).

Honory i nagrody

Strichman zdobył nagrodę Gutwirth firmy Technion w 2010 r., Aw 2021 r. nagrodę CAV za „pionierski wkład w podstawy teorii i praktyki teorii modulo spełnialności (SMT)”. Kilka narzędzi programowych (solwer SAT i solver CSP), które opracowane przez jego uczniów pod jego kierunkiem zdobyły złote i srebrne medale w międzynarodowych konkursach.

Publikacje

Książki

• Procedury decyzyjne - algorytmiczny punkt widzenia Wspólnie z Danielem Kroeningiem. Springer-Verlag , 2008.
• Efektywne procedury decyzyjne do walidacji (ponownie zredagowany zbiór publikacji doktoranckich Strichmana). Wydawnictwo akademickie LAP Lambert , 2010.

Wybrane artykuły

• Ostatecznie przyrostowy SAT . proc. XVII Międzynarodowej Konferencji Teorii i Zastosowań Testów Spełnialności (SAT'14). Razem z Aleksandrem Nadelem i Vadimem Ryvchinem, 2014.
• Wydajna ekstrakcja MUS z rozdzielczością . proc. 13. Konferencji Formalne Metody Komputerowego Wspomagania Projektowania (FMCAD'13). Razem z Vadimem Ryvchinem i Alexandrem Nadelem, 2013.
• Weryfikacja regresji: udowodnienie równoważności podobnych programów . Testowanie, weryfikacja i niezawodność oprogramowania, 23(3) 241–258, 2013. Wspólnie z Bennym Godlinem, 2013.
• Udowodnienie wzajemnego zakończenia programów . proc. ósmej konferencji weryfikacyjnej w Hajfie (HVC'12). Razem z Dimą Elenbogenem i Shmuelem Katzem, 2012.
• Zmniejszanie rozmiaru dowodów rozdzielczości w czasie liniowym . Journal on Software Tools and Technology Transfer (STTT), tom 13, wydanie 3, strona 263, 2011. Wraz z Omerem Bar-Ilanem, Odedem Fuhrmannem, Shlomo Hoory i Ohadem Shachamem, 2011.
• Dowód produkujący solver CSP . proc. 24.konferencji Association for the Advancement of Artificial Intelligence (AAAI'10). Razem z Michaelem Vekslerem, 2010.
• Trzy optymalizacje dla rozumowania zakładającego gwarancję z L* . Metody formalne w projektowaniu systemów, tom. 32, nr 3, strony 267–284, 2008. Razem z Sagarem Chakim, 2008.
• Techniki przycinania dla problemu sprawdzania ograniczonego modelu opartego na SAT . proc. z 11. Konferencji Roboczej ds. Zaawansowanych Badań nt. Poprawnego Projektowania Sprzętu i Metod Weryfikacji (CHARME'01), tom. 2144 notatek z wykładów z informatyki, strony 58 – 70, 2001.
• Dostrajanie kontrolerów SAT do sprawdzania ograniczonego modelu . Międzynarodowa konferencja na temat weryfikacji wspomaganej komputerowo (CAV), 2000, strony 480–494.

Linki zewnętrzne

• Strona Ofera Strichmana , Technion
• Strona Ofera Strichmana , dblp