Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs - Archive ouverte HAL Access content directly
Conference Papers Year : 2023

Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs

(1) , (2) , (3)
1
2
3

Abstract

Afin de prévenir les erreurs de programmation, des analyseurs statiques ont été développés pour de nombreux langages ; cependant, aucun analyseur mature ne cible l'analyse de valeurs pour un langage fonctionnel à la ML. Des outils de vérification pour ces langages existent, tels les systèmes de types classiques ou les méthodes déductives, mais le raisonnement automatique sur des programmes numériques a jusqu'alors été peu exploré. Cet article décrit un analyseur statique de valeurs par interprétation abstraite pour un langage fonctionnel typé du premier ordre, approche sûre et automatique pour garantir l'absence d'erreurs à l'exécution. En se basant sur des domaines abstraits relationnels et en réalisant des résumés des champs récursifs des types algébriques, cette approche permet d'analyser des fonctions récursives manipulant des types algébriques récursifs et d'inférer dans un domaine abstrait leur relation entrée-sortie. Une implémentation est en cours sur la plateforme d'analyse multilangage MOPSA et analyse avec succès de courts programmes de quelques lignes. Ce travail ouvre ainsi la voie vers une analyse de valeurs précise et relationnelle basée sur l'interprétation abstraite pour les langages fonctionnels d'ordre supérieur à la ML.
Fichier principal
Vignette du fichier
jfla23_paper_4105_v2.pdf (582.49 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03936718 , version 1 (12-01-2023)
hal-03936718 , version 2 (27-01-2023)

Identifiers

  • HAL Id : hal-03936718 , version 2

Cite

Milla Valnet, Raphaël Monat, Antoine Miné. Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs. JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.211-242. ⟨hal-03936718v2⟩
0 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More