Assoc. Prof. Ofer Strichman

Information Management Engineering



Prof. Strichman has been active in the formal verification community as of 1999. He has published two books: "Decision procedures – an algorithmic point of view" together with Daniel Kroening, and "Efficient decision procedures for validation", edited a third one and coauthored over 90 peer-reviewed articles in this field. He is also active in the SAT (Boolean satisfiability) community, and co-chaired the main conference SAT in 2010. Prof. Strichman is mostly known for his contributions to SAT (e.g., incremental satisfiability, phase saving), linear-time proof manipulation and bounded model-checking.


Some links:

Publication list

Selected presentaions

Slides from courses that I teach


  • Please visit the Haifa solvers' suite for updated information on our solvers HaifaSAT, HaifaCSP, HMUC, HHLMUC, HSMTMUC and the benchmarking platform HBench.
  • TVS: A translation validation tool from Simulink to C. Developed by Michael Ryabtsev.

A list of Current and past students

Selected Publications

My publications page can be found here



Kroening Strichman cover small

My PhD, republished here: 

(as an editor): 

Selected publications:

Ultimately Incremental SAT Proc. of the17th International conference on theory and applications of satisfiability testing(SAT'14). Together with Alexander Nadel and Vadim Ryvchin.

Efficient MUS extraction with Resolution Proc. of the 13thconference on Formal Methods in Computer Aided Design (FMCAD'13). Together with Vadim Ryvchin and Alexander Nadel.

Proving mutual termination of programs. Proc. ofthe eighthHaifaVerification Conference (HVC'12). Together with Dima Elenbogen and Shmuel Katz.

A proof producing CSP solver.Proc. of the 24thconference of theAssociation for the Advancement of Artificial Intelligence (AAAI'10). Together with Michael Veksler.

Regression verification: Proving the equivalence of similar programs.Software Testing, Verification and Reliability, 23(3) 241–258, 2013.Together with BennyGodliln.

Reducing the Size of Resolution Proofs in Linear Time. Journal onSoftware Tools and Technology Transfer (STTT),vol13, issue 3, page 263, 2011.Together with Omer Bar-Ilan,OdedFuhrmann,ShlomoHooryand OhadShacham.

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.


Formal verification of finite-state systems, model-checking and bounded model-checking. Decision procedures for first-order theories in the Satisfiability Modulo Theories (SMT) framework; SAT and CSP; Program equivalence checking

Contact Info

email: ofers -the at sign-
Room 412 Bloomfield Building