Parcours IL / Orientation IL & MFLS
Cette UE introduit les principaux concepts et techniques de vérification algorithmique qui visent la vérification automatique d’algorithmes et systèmes informatiques, en particulier concurrents et distribués. S’appuyant sur des bases logiques et algorithmiques, ces techniques sont largement utilisées pour la validation de circuits, de protocoles de réseaux et d’algorithmes répartis. Elles font partie de la boite à outils d’ingénieurs de vérification et de certification de systèmes.
Prérequis
- Connaissances de base en logique.
Acquis d’apprentissage
- Systèmes de transitions et logiques temporelles.
- Graphe d’états accessibles.
- Algorithme de vérification explicite et à la volée de formules LTL.
- Algorithme de vérification par points fixes de formules CTL.
- BDD et model checking symbolique.
- Vérification bornée par encodage SAT.
- Automates temporisés et comment les vérifier.
Compétences visées
- Modéliser un algorithme ou système concurrent, ou réparti éventuellement temporisé.
- Exprimer des propriétés de ces systèmes par des formules logiques.
- Utiliser sur des cas concrets des outils mettant en œuvre la vérification algorithmique.