Ofer Strichman Official Site

Prof. Ofer Strichman earned his Ph.D in 2001 from the Weizmann Institute, where he worked, under the supervision of Amir Pnueli, on translation validation for compilers, Bounded Model Checking, and other topics in formal verification. He then was a post-doc in Carnegie Mellon University in Ed Clark’s group, where he mostly worked on model-checking, learning, predicate abstraction and decision procedures.

Prof. Strichman published two books: “Decision procedures – an algorithmic point of view” together with Daniel Kroening, and “Efficient decision procedures for validation”, edited two others and coauthored more than 100 peer-reviewed articles, mostly in formal verification and SAT. In the SAT field he is mostly known for his contributions to linear-time proof manipulations, exploiting symmetries and incremental satisfiability. In formal verification he is mostly known for his invention of ‘regression verification’ and various decision procedures, mostly for equalities with uninterpreted functions.

Prof. Strichman won the 2021 CAV award “for pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT)”.