Students

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

  • Yuval Kaner – Learning reductions.
  • Nikita Gaevoy – Analysis of a resolution-based proof system.

Past Students

  • Chaked Seydoff (2022) – Regression verification meets weakest precondition. See Chaked’s thesis.
  • Dor Cohen (2022)- Automated repair of Neural Networks.
  • Ofer Guthman (2018) – SMT minimal core, and SAT techniques. See our publication.
  • 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.