stringtranslate.com

Ofer Strichman

Ofer Strichman (hebreo: עופר שטרייכמן, nacido el 4 de septiembre de 1968) es profesor de lógica computacional y ciencias de la computación en Davidson Industrial Engineering and Management , Technion – Instituto Tecnológico de Israel. Ocupa la cátedra Joseph Gruenblat en ingeniería de producción. [1]

Vida temprana y educación

Ofer Strichman nació y creció en Haifa . Se graduó de la escuela secundaria Alliance en 1986 y se unió al programa de reserva académica de las Fuerzas de Defensa de Israel . Recibió su licenciatura en Ingeniería Industrial (especializada en investigación de operaciones y sistemas de información ) del Technion en 1991. Luego sirvió durante seis años en las Fuerzas de Defensa de Israel, mientras estudiaba para obtener una maestría en investigación de operaciones y sistemas de información en el Technion. [1]

Después de dejar la IDF, comenzó un programa de doctorado en 1997 en el Instituto Weizmann en Rehovot , Israel, bajo la supervisión del profesor Amir Pnueli . [2] Se especializó en métodos formales y lógica computacional, y específicamente en validación de traducción para compiladores , verificación de modelos acotados y procedimientos de decisión. El título de su tesis fue 'Procedimientos de decisión eficientes para validación'. En 2001 comenzó un puesto de posdoctorado en la Universidad Carnegie Mellon , bajo el patrocinio del profesor Edmund Clarke , donde se especializó en verificación de modelos . [3]

Carrera académica

Strichman se incorporó al grupo de sistemas de información de la facultad de ciencia de datos y decisiones del Technion en 2003 como profesor titular . Fue ascendido a profesor asociado en 2009 y a profesor titular en 2017. En 2020 recibió la cátedra Joseph Gruenblat de ingeniería de producción. [1]

Durante cada verano de los años 2003 a 2015, Strichman fue científico visitante en el Instituto de Ingeniería de Software en Pittsburgh . [4] Fue consultor de IBM Research durante 6 años, a partir de 2004. En 2010 fue científico visitante en Microsoft Research en Redmond, Washington , como parte de un año sabático . [3]

Investigación

Las principales áreas de investigación del profesor Strichman son la verificación formal y la lógica computacional. Él, junto con su colega científico israelí Benny Godlin, es conocido por acuñar el término "verificación de regresión" para describir una técnica para demostrar la equivalencia de programas recursivos y por desarrollar varios procedimientos de decisión (principalmente para igualdades con funciones no interpretadas). [5] [6] También realizó contribuciones en la resolución de problemas SAT, como la satisfacibilidad incremental. [7]


Honores y premios

Strichman ganó el premio Gutwirth del Technion en 2010, y en 2021 el premio CAV por "contribuciones pioneras a los fundamentos de la teoría y la práctica de las teorías de módulo de satisfacibilidad (SMT)". [8] [9] Varias herramientas de software (un solucionador SAT y un solucionador CSP) que fueron desarrolladas por sus estudiantes bajo su supervisión ganaron medallas de oro y plata en competiciones internacionales. [10] [11] [12] [13]

Publicaciones

Libros

Artículos seleccionados

Referencias

  1. ^ abc "Ofer Strichman". Technion.
  2. ^ "Ofer Strichman". Proyecto de genealogía matemática .
  3. ^ ab "Resumen" (PDF) . Technion.
  4. ^ "Publicaciones de Ofer Strichman". Instituto de Ingeniería de Software.
  5. ^ Müller, Peter; Schaefer, Ina (23 de octubre de 2018). Desarrollo de software basado en principios: ensayos dedicados a Arnd Poetzsch-Heffter con motivo de su 60.º cumpleaños. Springer. ISBN 978-3-319-98047-8.
  6. ^ "Karlsruhe Reports in Informatics 2015,6 - Verificación de regresión para software de controlador lógico programable". Instituto Tecnológico de Karlsruhe, Alemania . Consultado el 20 de abril de 2022 .
  7. ^ Strichman, Ofer (2001). Técnicas de poda para el problema de verificación de modelos acotados basado en SAT. Springer. ISBN 978-3-540-44798-6.
  8. ^ "Premio CAV 2021". CAV.
  9. ^ "El profesor Ofer Strichman recibió el premio CAV (Computer Aided Verification) 2021". Technion. 4 de agosto de 2021.
  10. ^ "Competencia SAT 2011: vía MUS orientada a grupos: lista de solucionadores". Universidad de Artois .
  11. ^ "Competencia SAT 2011: pista MUS simple: clasificación de los solucionadores". Universidad de Artois.
  12. ^ "HCSP - Un solucionador de CSP con aprendizaje no clausal". MiniZinc .
  13. ^ "El desafío MiniZinc". MiniZinc.
  14. ^ Monahan, Rosemary (2018). "Daniel Kroening y Ofer Strichman: procedimientos de decisión" (PDF) . Aspectos formales de la informática . 30 (6): 759. doi : 10.1007/s00165-018-0466-2 . S2CID  51905876.
  15. ^ Procedimientos de decisión eficientes para la validación: validación de la traducción, procedimientos de decisión para la lógica de igualdad y ajuste de SAT para la verificación de modelos acotados . LAP Lambert Academic Publishing. 15 de mayo de 2010. ISBN 978-3838300825.

Enlaces externos