Associate Professor Ofer Strichman

General Information

Research Summary

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

I am currently looking for either an MSc student or a PhD student for an interesting software-verification research project.

Requirements: experience in software development in C (preferably experience in the industry), and background in verification.

Postdoc position : to work on the project "regression verification: proving the equivalence of similar C programs" (see relevant publications on this page). Requirements: experience in program analysis / static analysis / software model-checking.

Current Research Projects

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

• Yossi Levhari (Ph.D. student) - Continues the development of the Regrssion Verification Tool (RVT), a tool for proving the equivalence of similar C programs. The original version of the tool was developed by Benny Godlin (see below).
• Vadim Ryvchin - develops various optimizations to SAT solvers.
• Michael Veksler - develops a  Constraints Satisfaction Problem (CSP) solver based on multi-valued SAT techniques.
• Miron Rozanov - developed an efficient decision procedure for Equality Logic. Now works on the problem of model-counting.

Students that already graduated

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