Voir le reportage
20210159_0002
© Christian MOREL / IRIF / CNRS Photothèque

Discussion autour d’une technique issue de la théorie des automates, pour la vérification de programme

Référence

20210159_0002

Année de production

2021

Taille maximale

48.14 x 32.1 cm / 300 dpi

Légende

Discussion autour d’une technique issue de la théorie des automates pour la vérification de programmes informatiques. La figure au premier plan décrit le comportement d'un algorithme de saturation. Les scientifiques souhaitent déterminer si un programme informatique peut au cours d'une exécution atteindre une configuration d'erreur. Pour cela ils calculent de proche en proche une représentation des états du programme depuis lesquels une configuration d'erreur peut être atteinte. Le principal avantage d'une telle approche est qu'elle conduit à des algorithmes qui dans de nombreuses situations terminent plus rapidement que les méthodes classiques. La figure sur l'ordinateur au second plan décrit le principe général d'un algorithme. Partant d'un programme informatique écrit dans un langage autorisant de la récursion d'ordre supérieur (un paradigme présent dans tous les langages de programmation moderne) et d'une spécification que le programme doit vérifier, cet algorithme construit un nouveau programme informatique qui raffine le premier, tout en vérifiant (si cela est possible) la spécification.

Institut(s)

Délégation(s)

Thématiques scientifiques

CNRS Images,

Nous mettons en images les recherches scientifiques pour contribuer à une meilleure compréhension du monde, éveiller la curiosité et susciter l'émerveillement de tous.