Share to: share facebook share twitter share wa share telegram print page

Ofer Strichman

Ofer Strichman
Born (1968-09-04) 4 September 1968 (age 56)
Haifa, Israel
NationalityIsraeli
Alma materTechnion
Weizmann Institute
Scientific career
FieldsComputer Science, computational logic
InstitutionsTechnion
Thesis Efficient decision procedures for validation  (2001)
Doctoral advisorAmir Pnueli

Ofer Strichman (Hebrew: עופר שטרייכמן, born: 4 September 1968) is a professor of computational logic and computer science at the Davidson Industrial Engineering and Management, Technion – Israel Institute of Technology. He holds the Joseph Gruenblat chair in production engineering.[1]

Early life and education

Ofer Strichman was born and raised in Haifa. He graduated from Alliance high-school in 1986 and joined the academic reserve program of the IDF. He received his BSc in Industrial Engineering (specializing in operations research and information systems) from the Technion in 1991. He then served for six years in the IDF, while studying for an MSc degree in operations research and information systems at the Technion.[1]

After leaving the IDF, he started a PhD program in 1997 at the Weizmann Institute in Rehovot, Israel, under the supervision of Prof. Amir Pnueli.[2] He specialized in formal methods and computational logic, and specifically in translation validation for compilers, Bounded Model Checking, and decision procedures. His thesis title was ‘Efficient decision procedures for validation’. In 2001 he started a post-doc position at Carnegie Mellon University, under the sponsorship of Prof. Edmund Clarke, where he specialized in model checking.[3]

Academic career

Strichman joined the information systems group at the faculty of data and decisions science at the Technion in 2003, as a senior lecturer. He was promoted to an associate professor in 2009 and to a full professor in 2017. In 2020 he was awarded the Joseph Gruenblat chair in production engineering.[1]

During each summer in the years 2003–2015, Strichman was a visiting scientist at the Software Engineering Institute in Pittsburgh.[4] He was a consultant of IBM Research for 6 years, as of 2004. In 2010 he was a visiting scientist at Microsoft Research in Redmond, Washington, as part of a sabbatical.[3]

Research

Prof. Strichman's main research areas are formal verification and computational logic. He, along with fellow Israeli scientist Benny Godlin, is known for coining the term ‘regression verification’ to describe a technique for proving the equivalence of recursive programs, and for developing various decision procedures (mostly for equalities with uninterpreted functions).[5][6] He also had contributions in SAT solving, such as incremental satisfiability.[7]


Honors and awards

Strichman won the Technion's Gutwirth award in 2010, and in 2021 the CAV award for "pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT)”.[8][9] Several software tools (a SAT solver, and a CSP solver) that were developed by his students under his supervision won gold and silver medals in international competitions.[10][11][12][13]

Publications

Books

Selected articles

  • 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), vol. 13, 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.

References

  1. ^ a b c "Ofer Strichman". Technion.
  2. ^ "Ofer Strichman". Mathematics Genealogy Project.
  3. ^ a b "Resume" (PDF). Technion.
  4. ^ "Publications by Ofer Strichman". Software Engineering Institute.
  5. ^ Müller, Peter; Schaefer, Ina (2018-10-23). Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday. Springer. ISBN 978-3-319-98047-8.
  6. ^ "Karlsruhe Reports in Informatics 2015,6 - Regression Verification for Programmable Logic Controller Software". Karlsruhe Institute of Technology, Germany. Retrieved 2022-04-20.
  7. ^ Strichman, Ofer (2001). Pruning Techniques for the SAT-Based Bounded Model Checking Problem. Springer. ISBN 978-3-540-44798-6.
  8. ^ "2021 CAV Award". CAV.
  9. ^ "Prof. Ofer Strichman received the CAV (Computer Aided Verification) 2021 Award". Technion. 4 August 2021.
  10. ^ "SAT 2011 Competition: group-oriented MUS track: list of solvers". University of Artois.
  11. ^ "SAT 2011 Competition: plain MUS track: ranking of solvers". University of Artois.
  12. ^ "HCSP - A CSP solver with non-clausal learning". MiniZinc.
  13. ^ "The MiniZinc Challenge". MiniZinc.
  14. ^ Monahan, Rosemary (2018). "Daniel Kroening and Ofer Strichman: Decision procedures" (PDF). Formal Aspects of Computing. 30 (6): 759. doi:10.1007/s00165-018-0466-2. S2CID 51905876.
  15. ^ Efficient Decision Procedures for Validation: Translation Validation, decision procedures for equality logic, and SAT tuning for Bounded Model Checking. LAP Lambert Academic Publishing. 15 May 2010. ISBN 978-3838300825.
Kembali kehalaman sebelumnya