Les systèmes informatiques occupent une place grandissante dans notre société actuelle hautement informatisée. À mesure que les systèmes transactionnels traditionnels sont informatisés, une composante de confidentialité vient s'ajouter aux systèmes informatiques. Ces systèmes gagnant en complexité, la vérification manuelle par des êtres humains devient rapidement impraticable. Nous présentons des methods traditionnelles de verification automatique de la conformité d'un programme à une propriété de sécurité. Ensuite, nous présentons une approche originale de Hugues Chabot et al. utilisant des omega-automates, qui permettent de verifier des programmes pour lesquels une execution peut ne jamais se terminer. Nous proposons quelques optimisations puis procédons a son implantation pour en mesurer la performance. Nous présentons finalement une approche alternative, base sur la théorie des transactions logicielles, qui permet de corriger un programme deviant plutôt que de le rejetter. Nous terminons en posant un regrard critique sur le travail accompli.