Les systèmes informatiques ont un rôle essentiel dans la vie moderne. Ils gèrent des tâches extrêmement importantes dans tous les domaines des activités humaines (communication, transport, santé, commerce, finance, armement, etc.), et leur fiabilité est par conséquent primordiale. Ces systèmes sont d'une grande complexité; ils doivent être conçus et vérifiés de manières rigoureuses afin d'assurer un grand degré de confiance dans leurs comportements. Le but de ce cours est d'introduire à certaines méthodes de conception et de vérification de programmes de différents types et d'étudier les principes de base pour leur preuve et pour leur vérification algorithmique.

1. Raisonnement sur les données, types abstraits
2. Définition inductive de fonctions,
3. Spécification logique, preuve de programmes fonctionnels
4. Spécification de programmes impératifs, invariants, pré/post conditions
5. Preuve de programmes impératifs, Logique de Hoare, correction partielle, terminaison
6. Spécification de systèmes réactifs, model-checking
7. Vérification symbolique de systèmes
8. Abstraction et raffinement d'abstraction guidée par les contre-exemples

1. Logique (propositionnelle, premier ordre)
2. Algorithmes de parcours de graphes