Shape Analysis via Second-Order Bi-Abduction
CAV, pp. 52-68, 2014.
We present a new modular shape analysis that can synthesize heap memory specification on a per method basis. We rely on a second-order biabduction mechanism that can give interpretations to unknown shape predicates. There are several novel features in our shape analysis. Firstly, it is grounded on second-order bi-abduction. Secondly, we d...More
PPT (Upload PPT)