A Local Shape Analysis Based on Separation Logic: Detailed Presentation and Soundness Proof
Amin Timany and Bart Jacobs:
A Local Shape Analysis Based on Separation Logic: Detailed Presentation and Soundness Proof.
Hosted on
KU Leuven Library (lirias),
May 2014.
Technical Report
Technical Report
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.
The bibtex source for this publication:
@techreport{KULeuven-452375,
author= {Timany, Amin and Jacobs, Bart},
title = {{A Local Shape Analysis Based on Separation Logic: Detailed Presentation and Soundness Proof}},
year = {2014},
month = {May},
number = {CW661},
url = {https://lirias.kuleuven.be/handle/123456789/452375},
institution = {Department of Computer Science, KU Leuven},
type = {CW Reports}
}