Sites Inria

English version

Séminaire des équipes de recherche

Hugo Illous : A Relational Shape Abstract Domain

© INRIA Sophie Auvin - G comme Grille

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.

  • Date : 5/03/2018
  • Lieu : Inria de Paris- 2 rue Simone Iff- 75012
  • Intervenant(s) : Hugo Illous- ENS

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 memorystates containing inductive structures. We implement this analysis and report on the analysis of a basic library of list manipulating functions.

Mots-clés : Séminaire Gallium Equipe de recherche Inria Paris

Haut de page

Suivez Inria