Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

You searched for subject:(Ghost code). One record found.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters

1. Gondelman, Léon. Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification.

Degree: Docteur es, Informatique, 2016, Paris Saclay

Cette thèse se place dans le contexte de la vérification déductive des programmes et a pour objectif de formaliser un certain nombre de concepts qui sont mis en œuvre dans l'outil de vérification Why3.L'idée générale est d'explorer des solutions qu'une approche à base de systèmes de types peut apporter à la vérification. Nous commençons par nous intéresser à la notion du code fantôme, une technique implantée dans de nombreux outils de vérification modernes, qui consiste à donner à des éléments de la spécification les apparences d'un code opérationnel. L'utilisation correcte du code fantôme requiert maintes précautions puisqu'il ne doit jamais interférer avec le reste du code. Le premier chapitre est consacré à une formalisation du code fantôme, en illustrant comment un système de types avec effets en permet une utilisation à la fois correcte et expressive. Puis nous nous intéressons à la vérification des programmes manipulant des pointeurs. En présence d'aliasing, c'est-à-dire lorsque plusieurs pointeurs manipulés dans un programme dénotent une même case mémoire, la spécification et la vérification deviennent non triviales. Plutôt que de nous diriger vers des approches existantes qui abordent le problème d'aliasing dans toute sa complexité, mais sortent du cadre de la logique de Hoare, nous présentons un système de types avec effets et régions singletons qui permet d'effectuer un contrôle statique des alias avant même de générer les obligations de preuve. Bien que ce système de types nous limite à des pointeurs dont l'identité peut être connue statiquement, notre observation est qu'il convient à une grande majorité des programmes que l'on souhaite vérifier. Enfin, nous abordons les questions liées à la vérification de programmes conçus de façon modulaire. Concrètement, nous nous intéressons à une situation où il existe une barrière d'abstraction entre le code de l'utilisateur et celui des bibliothèques dont il dépend. Cela signifie que les bibliothèques fournissent à l'utilisateur une énumération de fonctions et de structures de données manipulées, sans révéler les détails de leur implémentation. Le code de l'utilisateur ne peut alors exploiter ces données qu'à travers un ensemble de fonctions fournies. Dans une telle situation, la vérification peut elle-même être modulaire. Du côté de l'utilisateur, la vérification ne doit alors s'appuyer que sur des invariants de type et des contrats de fonctions exposés par les bibliothèques. Du côté de ces dernières, la vérification doit garantir que la représentation concrète raffine correctement les entités exposées, c'est-à-dire en préservant les invariants de types et les contrats de fonctions. Dans le troisième chapitre nous explorons comment un système de types permettant le contrôle statique des alias peut être adapté à la vérification modulaire et le raffinement des structures de données.

This thesis is conducted in the framework of deductive software verification.is aims to formalize some concepts that are implemented in the verification tool Why3. The main idea is to…

Advisors/Committee Members: Filliâtre, Jean-Christophe (thesis director).

Subjects/Keywords: Vérification déductive des programmes; Why3; Raffinement de données; Système de types; Code fantôme; Deductive Software Verification; Why3; Data refinement; Type systems; Ghost code

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Gondelman, L. (2016). Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification. (Doctoral Dissertation). Paris Saclay. Retrieved from http://www.theses.fr/2016SACLS583

Chicago Manual of Style (16th Edition):

Gondelman, Léon. “Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification.” 2016. Doctoral Dissertation, Paris Saclay. Accessed June 04, 2020. http://www.theses.fr/2016SACLS583.

MLA Handbook (7th Edition):

Gondelman, Léon. “Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification.” 2016. Web. 04 Jun 2020.

Vancouver:

Gondelman L. Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification. [Internet] [Doctoral dissertation]. Paris Saclay; 2016. [cited 2020 Jun 04]. Available from: http://www.theses.fr/2016SACLS583.

Council of Science Editors:

Gondelman L. Un système de types pragmatique pour la vérification déductive des programmes : A Pragmatic Type System for Deductive Software Verification. [Doctoral Dissertation]. Paris Saclay; 2016. Available from: http://www.theses.fr/2016SACLS583

.