Modélisation de programmes C en expressions régulières

Authors: Mahbouli, Hatem
Advisor: Ktari, Béchir
Abstract: 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é.
Document Type: Mémoire de maîtrise
Issue Date: 2011
Open Access Date: 17 April 2018
Permalink: http://hdl.handle.net/20.500.11794/22510
Grantor: Université Laval
Collection:Thèses et mémoires

Files in this item:
SizeFormat 
28220.pdf3.35 MBAdobe PDFView/Open
All documents in CorpusUL are protected by Copyright Act of Canada.