Différentiation automatique et formes de Taylor en analyse statique de programmes numériques
| Autor: | Matthieu Martel, Alexandre Chapoutot |
|---|---|
| Přispěvatelé: | Laboratoire Modélisation et Analyse de Systèmes en Interaction (LMeASI), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Chapoutot, Alexandre, Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval |
| Jazyk: | francouzština |
| Rok vydání: | 2009 |
| Předmět: |
Floating point
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Relation (database) Automatic differentiation 020207 software engineering Context (language use) 02 engineering and technology Interval (mathematics) Static analysis Abstract interpretation [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL] Program analysis 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Algorithm ComputingMilieux_MISCELLANEOUS Mathematics |
| Zdroj: | Revue des Sciences et Technologies de l'Information-Série TSI : Technique et Science Informatiques Revue des Sciences et Technologies de l'Information-Série TSI : Technique et Science Informatiques, Lavoisier, 2009, 28 (4), pp.503-531. ⟨10.3166/tsi.28.503-531⟩ Revue des Sciences et Technologies de l'Information-Série TSI : Technique et Science Informatiques, 2009, 28 (4), pp.503-531. ⟨10.3166/tsi.28.503-531⟩ Conférence sur les Approches Formelles dans l'Assistance au Développement de Logiciels Conférence sur les Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2007, Namur, Belgique. pp.261-280 |
| ISSN: | 0752-4072 2116-5920 |
| DOI: | 10.3166/tsi.28.503-531⟩ |
| Popis: | International audience; Des travaux récents sur l'analyse statique de programmes numériques ont montré que les techniques d'interprétation abstraite étaient adaptées à la validation de la précision des calculs en arithmétique flottante. L'utilisation des intervalles comme domaine numérique, même avec des méthodes de subdivision, induit une sur-approximation des résultats en particulier par l'existence de l'effet enveloppant (wrapping effect). Une solution utilisée pour éviter ce problème est la définition de domaines relationnels étroitement liés aux propriétés à valider. Nous allons montrer dans cet article comment des techniques de différentiation automatique peuvent être utilisées pour définir des formes de Taylor permettant de définir une nouvelle analyse statique. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|