exécution

En informatique, l'exécution est le processus par lequel un ordinateur ou une machine virtuelle met en œuvre les instructions d'un programme. Les instructions du programme entraînent des séquences d'actions élémentaires sur la machine d'exécution. Les effets qu'entraînent ces actions sont conformes à la sémantique des instructions du programme. Un programme en cours d'exécution est appelé un processus. L’exécution symbolique permet d'explorer les chemins d'exécution possibles d'un programme informatique à partir des symboles contenus dans son code source. Elle diffère de l’exécution concrète qui ne suit qu'un seul des chemins possibles. Alors que l’exécution concrète met directement à jour les variables en mémoire, l’exécution symbolique enregistre les formules logiques liant les variables entre elles. Le but est d'analyser statiquement un programme pour trouver des bugs ou prouver certaines propriétés du programme. Il s'agit d'une interprétation abstraite d'un programme.