We present the article “Shape analysis by means of bi-abduction” by Cristiano Calcagno, Dino Distefano, Peter O’Hearn, Hongseok Yang published at POPL in 2009.
This article addresses the problem of pre- & post-condition generation and verification for function analysis. In order to resolve this problem, the authors introduce the notion of bi-abduction, which allows, using the contracts of functions already analyzed, to complete the pre- & post-conditions of calling functions. This analysis has been implemented in the analysis tool “Abductor” and has been applied to a large database of programs.
