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.