Résumé
La phase de validation d’un logiciel occupe une partie importante du temps consacré à sa conception. Afin d’optimiser ce processus, plusieurs langages proposent d’intégrer des constructions linguistiques qui aident à la vérification formelle de propriétés de sûreté et de sécurité. L’exposé est revenu sur les contrats de logiciels comme ceux utilisés dans le langage Spec#, a comparé les vérifications dynamiques et statiques de contrats de logiciels, et a examiné des propositions plus récentes sur la vérification de propriétés de sécurité en Java issues de spécifications formelles.
