Pointer Analysis and Separation Logic.

Analyses de Pointeurs et Logique de Séparation.

Elodie-Jane Sims (1)

1 CIS@K-STATE - Department of Computing and Information Sciences [Kansas]

We are interested in modular static analysis to analyse softwares automatically. We focus on programs with data structures, and in particular, programs with pointers. The final goal is to find errors in a program (problems of dereferencing, aliasing, etc) or to prove that a program is correct (regarding those problems) in an automatic way. Isthiaq, Pym, O'Hearn and Reynolds have recently developed separation logics, which are Hoare logics with assertions and predicates language that allow to prove the correctness of programs that manipulate pointers. The semantics of the logic's triples ({P}C{P

Le cadre de cette thèse est l'analyse statique modulaire par interprétation abstraite de logiciels en vue de leur vérification automatique. Nous nous intéressons en particulier aux programmes comportant des objets alloués dynamiquement sur un tas et repérés par des pointeurs. Le but final étant de trouver des erreurs dans un programme (problèmes de déréférencements et d'alias) ou de prouver qu'un programme est correct (relativement à ces problèmes) de façon automatique. Isthiaq, Pym, O'Hearn et Reynolds ont développé récemment des logiques de fragmentation (separation logics) qui sont des logiques de Hoare avec un langage d'assertions/de prédicats permettant de démontrer qu'un programme manipulant des pointeurs sur un tas est correct. La sémantique des triplets de la logique ({P}C{P

Mots clés: Static analysis; Pointer analysis; Separation logic; Abstract interpretation; Shape analysis

Mots clés: Analyse statique; Analyse de pointeurs; Logique de séparation; Interprétation abstraite

Domaines: Informatique [cs]

Elodie-Jane Sims. Pointer Analysis and Separation Logic.. Computer Science [cs]. Ecole Polytechnique X, 2007. English. ⟨NNT : ⟩. ⟨pastel-00003506⟩