Abstraction of Optional Numerical Values

Jiangchao Liu 1 Xavier Rival 2, 1
2 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
Abstract : We propose a technique to describe properties of numerical stores with optional values, that is, where some variables may have no value. Properties of interest include numerical equalities and inequalities. Our approach lifts common linear inequality based numerical abstract domains into abstract domains describing stores with optional values. This abstraction can be used in order to analyze languages with some form of option scalar type. It can also be applied to the construction of abstract domains to describe complex memory properties that introduce symbolic variables, e.g., in order to summarize unbounded sets of program variables, and where these symbolic variables may be undefined, as in some array or shape analyses. We describe the general form of abstract states, and propose sound and automatic static analysis algorithms. We evaluate our construction in the case of an array abstract domain.
Type de document :
Communication dans un congrès
Xinyu Feng and Sungwoo Park. Programming Languages and Systems - 13th Asian Symposium, , Nov 2015, Pohang, South Korea. Springer, Programming Languages and Systems - 13th Asian Symposium, Lecture Notes in Computer Science (9458), 〈10.1007/978-3-319-26529-2_9〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01256116
Contributeur : Alain Monteil <>
Soumis le : jeudi 14 janvier 2016 - 13:56:52
Dernière modification le : vendredi 25 mai 2018 - 12:02:07

Identifiants

Collections

Citation

Jiangchao Liu, Xavier Rival. Abstraction of Optional Numerical Values. Xinyu Feng and Sungwoo Park. Programming Languages and Systems - 13th Asian Symposium, , Nov 2015, Pohang, South Korea. Springer, Programming Languages and Systems - 13th Asian Symposium, Lecture Notes in Computer Science (9458), 〈10.1007/978-3-319-26529-2_9〉. 〈hal-01256116〉

Partager

Métriques

Consultations de la notice

108