Interprocedural Shape Analysis Using Separation Logic-based Transformer Summaries - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

Interprocedural Shape Analysis Using Separation Logic-based Transformer Summaries

Résumé

Shape analyses aim at inferring semantic invariants related to the data-structures that programs manipulate. To achieve that, they typically abstract the set of reachable states. By contrast, abstractions for transformation relations between input states and output states not only provide a finer description of program executions but also enable the composition of the effect of program fragments so as to make the analysis modular. However, few logics can efficiently capture such transformation relations. In this paper, we propose to use connectors inspired by separation logic to describe memory state transformations and to represent procedure summaries. Based on this abstraction, we design a top-down interprocedural analysis using shape transformation relations as procedure summaries. Finally, we report on implementation and evaluation.
Fichier principal
Vignette du fichier
sas.pdf (628.37 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03081558 , version 1 (18-12-2020)

Identifiants

  • HAL Id : hal-03081558 , version 1

Citer

Hugo Illous, Matthieu Lemerre, Xavier Rival. Interprocedural Shape Analysis Using Separation Logic-based Transformer Summaries. SAS 2020 - 27th Static Analysis Symposium, Nov 2020, Chicago / Virtual, United States. ⟨hal-03081558⟩
78 Consultations
485 Téléchargements

Partager

Gmail Facebook X LinkedIn More