A Local Shape Analysis Based on Separation Logic: Detailed Presentation and Soundness Proof

Hosted on KU Leuven Library (lirias) Technical Report
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.
  • Links: .pdf Lirias
  • Keywords: shape analysis, separation logic, static analysis, soundness
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.

BibTeX
@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}
}