Skip to Main content Skip to Navigation

Pointer Analysis and Separation Logic.

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
Document type :
Complete list of metadatas

Cited literature [28 references]  Display  Hide  Download
Contributor : Ecole Polytechnique <>
Submitted on : Tuesday, July 27, 2010 - 2:39:02 PM
Last modification on : Wednesday, July 28, 2010 - 9:44:28 AM
Long-term archiving on: : Thursday, October 28, 2010 - 5:03:25 PM


  • HAL Id : pastel-00003506, version 1



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