Prof. 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 and learning.
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 95 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 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.
New: 2nd edition of 'Decision Procedures - an algorithmic point of view' (Jan 2017). You can get it here.
(Note: due to a printing error of the publisher, several dozen copies were distributed where it says 'editors' near our names. Not that interesting, but if you really have nothing better to do then you can read about it here).
The first edition of this book was #1 best seller of Springer/CS in the 'theoretical computer science' series in the last decade, and one of the best sellers in all of Springer/CS's publications.
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.
- EduSAT: a SAT solver for educational purposes.
- The Regression Verification Tool (RVT) - proving the equivalence of programs.
- pv - program visualizer. Builds an automata that represents a program's behavior, or traces that lead to an error.
- TVS: A translation validation tool from Simulink to C.
You may want to see the presentations of the Haifa SAT/SMT seminar.
Benchmarks: difficult benchmarks in CNF, OPB, SMT2, WCNF, MOD (cplex) and MZN (miniZinc) formats, resulting from university scheduling (time-tabling) problems, are available here.
Selected conference activities:
I PC-chaired HVC-2017.
I will co-chair FMCAD 2020. It will be held in Haifa.
My publications page can be found here
My PhD, republished here:
(as an editor):
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 veriﬁcation of ﬁnite-state systems, model-checking and bounded model-checking. Decision procedures for ﬁrst-order theories in the Satisﬁability Modulo Theories (SMT) framework; SAT and CSP; Program equivalence checking
Current M.Sc. / Ph.D. Students and their projects
- Ofer Guthman - SMT minimal core, and SAT techniques.
- Dor Cohen - Synthesis of correct Neural Networks
- Chaked Seydoff - Regression verification meets weakest precondition
- Yair Nof (2018) - Real Time Solving of Discrete Optimization Problems. See Yair's thesis.
Maor Weizmann (2016) - new proof methods for regression verification. See Maor's thesis.
- Michael Veksler (2014) - Constraints Satisfaction Problem (CSP) solver based on multi-valued SAT techniques. See Michael's thesis.
- Nir Drucker (2014) - Cyclic Routing of Unmanned Aerial Vehicles. See Nir's thesis.
- Vadim Ryvchin (2014) - Core algorithms for SAT and SAT-related problems. See Vadim's thesis.
- Dima Elenbogen (2014) - Proving mutual termination of programs. See Dima's thesis.
- Radislav (Slava) Vaisman (2013) (mostly supervised by Reuven Rubinstein) - Stochastic Enumeration Methods for Counting, Rare-events and Optimization
- Moshe Emmer (2013) - Bounded model checking at word-level via Encodings into Efficient Propositional Logic (co-supervised with Y. Moses and M. Khasidashvili)
- Mirron Rozanov (2011)- 1) developed an efficient decision procedure for Equality Logic. 2) developed a method for approximated model-counting. See Mirron's thesis.
- Michael Ryabtsev (2009) - developed : a Translation-Validation tool from Matlab's Simulink to C. See Michael's thesis.
- Katya Kuchi (2008) - A probabilistic analysis of coverage methods. See Katya's thesis.
- Dan Goldwasser (2008) - A theory-based decision heuristic for disjunctive linear arithmetic. See Dan's thesis.
- Benny Godlin (2008) - Regression verification: theoretical and implementation aspects. See Benny's thesis and our joint Position paper about it. See also my invited about this work in CAV'09. Also see Benny's HRDAG's project, and his home page.
- Roman Gershman (2007) - Improvements of SAT solving techniques. See Roman's thesis and the powerful SAT solver HaifaSat that he developed as part of his thesis.
- Maya Koifman (2006) - Minimizing unsatisfiable cores with Dominators. See Maya's thesis, and link to Core-Trimmer.
- Orly Meir (2005) - A graph-based decision procedure for Equality Logic. See Orly's thesis.