| Attributes | Values |
|---|
| type
| |
| Thesis advisor
| |
| Author
| |
| alternative label
| - From imperative programs to equational logic for correctness verification
|
| dc:subject
| - Thèses et écrits académiques
- Logiciels -- Développement
- Méthodes formelles (informatique)
- Logiciels -- Vérification
- Réécriture, Systèmes de (informatique)
|
| preferred label
| - Des programmes impératifs vers la logique équationnelle pour la vérification
|
| Language
| |
| Subject
| |
| dc:title
| - Des programmes impératifs vers la logique équationnelle pour la vérification
|
| Degree granting institution
| |
| note
| - Omnipresence of computer systems in modern technological applications makes the question of their reliability essential. In this thesis, we investigate equational logic as a foundation for the verification of programs written in an imperative language. Our approach aims at automating the verification of program properties while offering a formalism suited to software developers for reasoning about programs. Precisely, our work addresses the automatic translation of imperative programs into equational logic in order to verify their correctness. We studied two classes of programs. In the first class, assignment is the sole language statement with side effect. We developed an algorithm to translate the programs in this class into a set of equations. This algorithm is expressed as a rewrite system defining the language's semantics. We showed, with a theorem prover, the convergence of our rewrite system. The second class is defined by adding to the programming language call-by-reference parameter passing mode and mutable lists. These mechanisms introduce the ability of handling aliases in programs. We define restrictions on the use of aliases which allow us to propose an algorithm for the translation into equations of the programs in the new class. The equational definition we obtain does not involve an explicit model of the program's memory. The equations produced by the translation of a program can then be used in proof systems in order to verify properties of the program. The properties are also expressed as equations. We validate our approach by implementing the translation algorithms and by proving interesting program properties from the equations produced by our method.
- Nous nous sommes intéressé à la logique équationnelle en tant que support de la vérification des programmes impératifs. Notre approche vise le double objectif d'automatiser la vérification des propriétés de programmes et de proposer un formalisme pour raisonner sur les programmes adapté aux acteurs du développement des logiciels. Précisément, les travaux de cette thèse portent sur la traduction automatique des programmes impératifs vers la logique équationnelle. Nous avons considéré deux classes de programmes. Dans la première, la seule instruction avec effet de bord du langage est l'affectation. Nous présentons l'algorithme de traduction d'un programme en un ensemble d'équations sous la forme d'un système de réécriture définissant la sémantique du langage. Nous montrons la convergence du système de réécriture à l'aide d'un démonstrateur de théorèmes. Pour la seconde classe, nous ajoutons au langage appel par référence et listes mutables. Ces deux mécanismes introduisent la possibilité de manipuler des alias dans les programmes. Nous énonçons des restrictions sur l'utilisation des alias moyennant lesquelles nous proposons un algorithme pour la traduction en équations des programmes de cette seconde classe. La définition équationnelle obtenue ne s'appuie pas sur un modèle de la mémoire. Les équations produites par la traduction d'un programme peuvent alors être utilisées dans des systèmes de preuve afin de vérifier des propriétés du programme, elles-mêmes exprimées par des équations. Nous validons notre approche par une implantation des algorithmes et par la preuve de propriétés de programmes non triviales à l'aide des équations produites par notre méthode.
|
| dc:type
| |
| http://iflastandar...bd/elements/P1001
| |
| rdaw:P10219
| |
| has content type
| |
| is primary topic
of | |
| is rdam:P30135
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
