Ofer Strichman

Ofer Strichman (; born: 4 September 1968) is a professor of computational logic and computer science at the Faculty of Data and Decision Sciences, Technion – Israel Institute of Technology. He holds the Joseph Gruenblat chair in production engineering.

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

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. 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. He also had contributions in SAT solving, such as incremental satisfiability.

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)”. 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.

Publications Books 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.

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.