IRILL - Research and Innovation on Free Software La vérification et la validation des systèmes logiciel critiques est une tâche ardue, pour laquelle les méthodes formelles sont de plus en plus recommandés par des standards industriel de référence, comme le DO-178C (avionique) et l'ISO 26262 (automobile).
Dans cet exposé, qui a été conçu spécifiquement pour une audience industrielle, nous présentons une introduction à trois classes de méthodes, adaptées à la spécification, l'analyse et la vérification de propriétés: les approches déductives, le model checking et l'interprétation abstraite.
On s'appuyera dans le cours de l'exposé sur des exemples et des applications qui permettront de saisir plus facilement les concepts fondamentaux de chaque classe de méthodes.