A Relational Shape Abstract Domain

Hugo Illous 1, 2 Matthieu Lemerre 1 Xavier Rival 2
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
2 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria de Paris
Abstract : Static analyses aim at inferring semantic properties of programs. While many analyses compute an over-approximation of reachable states, some analyses compute a description of the input-output relations of programs. In the case of numeric programs, several analyses have been proposed that utilize relational numerical abstract domains to describe relations. On the other hand, designing abstractions for relations over memory states and taking shapes into account is challenging. In this paper, we propose a set of novel logical connectives to describe such relations, which are inspired by separation logic. This logic can express that certain memory areas are unchanged, freshly allocated, or freed, or that only part of the memory was modified. Using these connectives, we build an abstract domain and design a static analysis that over-approximates relations over memory states containing inductive structures. We implement this analysis and report on the analysis of a basic library of list manipulating functions.
Type de document :
Communication dans un congrès
NFM 2017 - 9th NASA Formal Methods Symposium, Apr 2017, Moffett Field, United States. Springer, 10227, pp.212-229, LNCS. 〈10.1007/978-3-319-57288-8_15〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01648681
Contributeur : Xavier Rival <>
Soumis le : lundi 27 novembre 2017 - 02:10:04
Dernière modification le : lundi 24 septembre 2018 - 11:34:02

Fichier

nfm.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Hugo Illous, Matthieu Lemerre, Xavier Rival. A Relational Shape Abstract Domain. NFM 2017 - 9th NASA Formal Methods Symposium, Apr 2017, Moffett Field, United States. Springer, 10227, pp.212-229, LNCS. 〈10.1007/978-3-319-57288-8_15〉. 〈hal-01648681〉

Partager

Métriques

Consultations de la notice

134

Téléchargements de fichiers

31