VCC est un vérificateur mécanique pour les programmes C concurrents. VCC prend un programme C, annoté avec les spécifications de fonction, invariants de données, des invariants de boucle ... et tente de prouver que ces annotations sont correctes.
Télécharger VCC .
