Author:

Keywords:

iMinds

Abstract:

Shape analysis is a static analysis of the source code of a program to determine shapes and manipulations of the dynamically allocated data structures at each point which that program can reach in an execution. In this report, we give a detailed presentation and soundness proof of a shape analysis method which uses separation logic to represent program memory.