L’analyse statique des programmes est une technique de vérification qui permet
de statuer si un programme est conforme à une propriété donnée. Pour l’atteinte de
cet objectif, il faudrait disposer d’une abstraction du programme à vérifier et d’une
définition des propriétés. Dans la mesure où l’outil de vérification prend place dans un
cadre algébrique, la définition des propriétés ainsi que la modélisation du programme
sont représentées sous la forme d’expressions régulières.
Ce mémoire traite en premier lieu de la traduction des programmes écrits en langage
C vers une abstraction sous forme d’expressions régulières. La méthode de traduction
proposée, ainsi que les différentes étapes de transformations y sont exposées.
Les premiers chapitres du présent mémoire énoncent les connaissances élémentaires de
la théorie des langages ainsi que de la compilation des programmes. Un bref aperçu des
différentes méthodes de vérification des programmes est présenté comme une mise en
contexte. Finalement, la dernière partie concerne la traduction des programmes ainsi
que la description de l’outil de traduction qui a été réalisé.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2011/28220 |
| Date | 04 1900 |
| Creators | Mahbouli, Hatem |
| Contributors | Ktari, Béchir |
| Publisher | Université Laval |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | application/pdf |
| Rights | © Hatem Mahbouli, 2011 |
Page generated in 0.0017 seconds