Associate Professor Ofer Strichman

General Information

Research Summary

• Formal Methods in Software and Hardware Verification (e.g. Model-checking, Bounded Model-Checking, SAT, Translation Validation, Decision Procedures for first-order theories, satisfiability modulo theories (SMT). Regression verification)

PhD and PostDoc positions are now available (Starting date: Sep. 2011). Topic: Regression verification - proving the equivalence of similar C programs (see presentation and article to get an idea about the topic.

Requirements: experience in software development in C (preferably experience in the industry), and background in verification. Experience in program analysis / static analysis / software model-checking would be a major plus.

Current Research Projects

My M.Sc. / Ph.D. Students and their projects

• Vadim Ryvchin - develops various optimizations to SAT solvers.
• Michael Veksler - develops a  Constraints Satisfaction Problem (CSP) solver based on multi-valued SAT techniques.
• Dima Elenbogen - develops RVT (a regression verification tool), and a  method for proving mutual termination.

Students that already graduated

• Mirron Rozanov - 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 TVS: 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 presentation  about this work in CAV'09.
• 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.