Toward proving program manipulating
Separation logic-based shape analyses aim to infer properties of heap manipulating programs. These analyses abstract the heap using separation logic including inductive summarizing predicates. Whereas they have been successfully applied to prove properties of data structures layout, they usually abstract away some properties of the data structures contents. As a…
