Outils pour utilisateurs
if-sv
Différences
Ci-dessous, les différences entre deux révisions de la page.
| if-sv [2020/10/07 14:14] – créée vpenelle | if-sv [2020/10/07 14:24] (Version actuelle) – vpenelle | ||
|---|---|---|---|
| Ligne 9: | Ligne 9: | ||
| Ce cours a pour but principal d’introduire des techniques classiques de vérification et de les implémenter dans un vérificateur de programmes (simples). L’outil réalisé au cours du semestre est capable de détecter des violation d’assertions sur des programmes dans un sous-langage du C (uniquement des entiers et pas de pointeurs) sans que l’utilisateur ait à fournir d’autres information que le programme. | Ce cours a pour but principal d’introduire des techniques classiques de vérification et de les implémenter dans un vérificateur de programmes (simples). L’outil réalisé au cours du semestre est capable de détecter des violation d’assertions sur des programmes dans un sous-langage du C (uniquement des entiers et pas de pointeurs) sans que l’utilisateur ait à fournir d’autres information que le programme. | ||
| - | La partie 1, enseignée par Vincent Penelle, présente le cadre général du vérificateur (notamment le langage vérifié et sa sémantique), | + | La [[https:// |
| La partie 2, enseignée par Grégoire Sutre, présente la technique de l’interprétation abstraite, qui consiste à regarder des abstractions de l’ensemble des exécutions d’un programme dans un domaine mathématique bien ordonné plus simple. Durant cette partie, plusieurs domaines abstraits simples sont implémentés. | La partie 2, enseignée par Grégoire Sutre, présente la technique de l’interprétation abstraite, qui consiste à regarder des abstractions de l’ensemble des exécutions d’un programme dans un domaine mathématique bien ordonné plus simple. Durant cette partie, plusieurs domaines abstraits simples sont implémentés. | ||
| La partie 3, enseignée par Jérôme Leroux, présente la technique du raffinement d’abstraction guidé par contre-exemple (CEGAR) et quelques bases sur les réseaux de Petri. | La partie 3, enseignée par Jérôme Leroux, présente la technique du raffinement d’abstraction guidé par contre-exemple (CEGAR) et quelques bases sur les réseaux de Petri. | ||
if-sv.1602080052.txt.gz · Dernière modification : 2020/10/07 14:14 de vpenelle
Outils de la page
Sauf mention contraire, le contenu de ce wiki est placé sous les termes de la licence suivante : CC Attribution-Share Alike 4.0 International
