Sciweavers

Share
SAS
2007
Springer

Footprint Analysis: A Shape Analysis That Discovers Preconditions

9 years 7 months ago
Footprint Analysis: A Shape Analysis That Discovers Preconditions
Existing shape analysis algorithms infer descriptions of data structures at program points, starting from a given precondition. We describe an analysis that does not require any preconditions. It works by attempting to infer a description of only the cells that might be accessed, following the footprint idea in separation logic. The analysis allows us to establish a true Hoare triple for a piece of code, independently of the context in which it occurs and without a whole-program analysis. We present experimental results for a range of typical list-processing algorithms, as well as for code fragments from a Windows device driver.
Cristiano Calcagno, Dino Distefano, Peter W. O'Hea
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where SAS
Authors Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
Comments (0)
books