CW Reports
Publication date:
2014-05-01
Publisher:
Department of Computer Science, KU Leuven; Leuven, Belgium
Author:
Timany, Amin
Jacobs, Bart
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.