Assas Recherche | Vérification automatique de programmes par inférence de modèles relationnels

Vérification automatique de programmes par inférence de modèles relationnels (Document en Anglais)

Accès au(x) document(s)

Accéder au(x) document(s) :

Ce document est protégé en vertu du Code de la Propriété Intellectuelle.

Modalités de diffusion de la thèse :

Thèse consultable sur internet, en texte intégral.

Informations sur les contributeurs

Auteur : Losekoot Théo

Losekoot, Théo

Nom

Losekoot

Prénom

Théo

Nationalité

Français

Date de soutenance : 17-12-2024

Directeur(s) de thèse : Genet Thomas

Genet, Thomas

Nom

Genet

Prénom

Thomas

- Jensen Thomas

Jensen, Thomas

Nom

Jensen

Prénom

Thomas

Etablissement de soutenance : Université de Rennes (2023-....)

Université de Rennes (2023-....)

Nom

Université de Rennes (2023-....)

Laboratoire : IRISA

IRISA

Nom

IRISA

- IRISA

IRISA

Nom

IRISA

- EPICURE

EPICURE

Nom

EPICURE

Ecole doctorale : MATISSE

MATISSE

Nom

MATISSE

Informations générales

Discipline : Informatique
Classification : Informatique

Mots-clés libres : Vérification formelle, Propriétés relationnelles, Données algébriques, Inférence de modèle
Mots-clés :

Programmation fonctionnelle (informatique)
Approximation, Théorie de l'
Vérification de modèles (informatique)

Résumé : Cette thèse porte sur la preuve automatique de propriétés concernant la relation entrée/sortie de programmes fonctionnels manipulant des types de données algébriques (ADT). De récents résultats montrent comment approximer un programme fonctionnel en utilisant un automate d'arbre. Bien qu'expressives, ces techniques ne peuvent pas prouver de propriété reliant l'entrée et la sortie d'une fonction, par exemple qu'inverser une liste préserve sa longueur. Dans cette thèse, nous nous appuyons sur ces résultats et définissons une procédure pour calculer ou sur-approximer une telle relation. Formellement, le problème de la vérification de programmes se réduit à la satisfiabilité de clauses, que nous résolvons en exhibant un modèle. Dans cette thèse, nous proposons deux représentations relationnelles de ces modèles de Herbrand : les automates d'arbres convolués et les shallow Horn clauses. Les automates d'arbres convolués généralisent les automates d'arbres et sont généralisés par les shallow Horn clauses. Le problème d'inférence du modèle de Herbrand découlant de la vérification relationnelle étant indécidable, nous proposons une procédure d'inférence incomplète mais correcte. Les expériences montrent que cette procédure est performante en pratique par rapport aux outils actuels, à la fois pour la vérification des propriétés et pour la recherche de contre-exemples.

Informations techniques

Type de contenu : Text
Format : PDF

Informations complémentaires

Entrepôt d'origine :

STAR : dépôt national des thèses électroniques françaises

Identifiant : 2024URENS102
Type de ressource : Thèse