Ofer Strichman

Ofer Strichman
Born	(1968-09-04) 4 September 1968 (age 56) Haifa, Israel
Nationality	Israeli
Alma mater	Technion Weizmann Institute
Scientific career
Fields	Computer Science, computational logic
Institutions	Technion
Thesis	Efficient decision procedures for validation  (2001)
Doctoral advisor	Amir 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]

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]

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]

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]

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]}

• Decision Procedures - an algorithmic point of view Together with Daniel Kroening. Springer-Verlag, 2008.^[14]
• Efficient Decision Procedures for Validation (a re-edited collection of Strichman's PhD publications). LAP Lambert Academic Publishing, 2010.^[15]

• 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.

• Ofer Strichman's page, Technion
• Ofer Strichman's page, dblp