Vous pouvez vérifier du code par model checking sans apprendre la temporal logic
Les bounded model checkers comme Kani et les relational model finders comme Alloy permettent de vérifier des propriétés avec des assertions et des contraintes ordinaires. Vous renoncez aux preuves de liveness pour une courbe d'apprentissage mesurée en heures.
