Pointer Analysis and Separation Logic. - Archive ouverte HAL Access content directly
Theses Year : 2007

Pointer Analysis and Separation Logic.

Analyses de Pointeurs et Logique de Séparation.

(1)
1

Abstract

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
Fichier principal
Vignette du fichier
Sims_E_J.pdf (1.95 Mo) Télécharger le fichier
Loading...

Dates and versions

pastel-00003506 , version 1 (27-07-2010)

Identifiers

  • HAL Id : pastel-00003506 , version 1

Cite

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

Collections

PASTEL PARISTECH
110 View
635 Download

Share

Gmail Facebook Twitter LinkedIn More