Ait Mohamed, Otmane

Avec les récents progrès des fonderies de technologie du silicium, qui continuent à réduire agressivement les dimensions physiques des structures de silicium, et les progrès des technologies de conception, qui permettent aux ingénieurs de construire des conceptions plus grandes et plus complexes, la preuve de l’exactitude de ces systèmes devient le plus grand défi à relever. Dans le cadre de ce programme de recherche, nous nous intéressons au développement de techniques et d’outils permettant d’améliorer l’utilité de la vérification formelle pour l’analyse et la vérification de systèmes à grande échelle. Par exemple, nous nous intéressons au lien entre l’approche basée sur la simulation et l’approche de vérification de modèle. En ajoutant à la conception un ensemble d’assertions qui définissent le comportement souhaité de chaque bloc de la conception, nous pouvons synthétiser des moniteurs pour vérifier la validité de la conception d’une part, et dériver des contraintes d’autre part. Ces contraintes peuvent être utilisées avec un vérificateur de modèle.