Z3

Tout droit sorti des laboratoires Microsoft Research, le logiciel Z3 propose un solveur SMT (Satisfied Modulo Theories) efficace qui combine une multitude de solveurs théoriques dans un framework combiné. Z3 peut s'employer pour prouver des théorèmes et pour trouver des contres exemples invalidants un possible théorème. En effet, Z3 propose un vérificateur automatique de satisfiabilité pour plusieurs types triés de logique du premier ordre incluant le support des quantificateurs. L'application intègre deux exécutables, un pour système 32 bits, l'autre 64 bits, et s'exécute en mode console.