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.

• Type: Conference
• Year: 2007
• Where: SAS
• Authors: Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
• Keywords: Algorithms Infer Descriptions, Analysis, Formal Methods, Infer, SAS 2007