- 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.
Benchmarks: difficult benchmarks in CNF, OPB, SMT2, WCNF, MOD (cplex) and MZN (miniZinc) formats, resulting from university scheduling (time-tabling) problems, are available here.