Terminator est un projet de recherche de Microsoft ayant pour objet le développement d'algorithmes destinés à prouver la bonne terminaison d'un programme et ses conditions générales de viabilité (relayé par internetnews).