Bi-abductive inference for reasoning about heaps Seminars/Workshops

Abstract

Bi-abduction is a new inference technique which enables the "local reasoning" idea of separation logic to be realized in a program analysis. Local reasoning says that reasoning should concentrate on the cells that a program accesses (its footprint), and is basis of modular reasoning methods for heaps. Bi-abduction gives a way to infer these footprints. In this talk I will describe theoretical and pragmatic aspects of bi-abductive inference. This talk is based on the work in the POPL'09 paper "Compositional shape analysis by means of bi-abduction" by Calcagno, Distefano, Yang and I. In the talk I will highlight some of the issues that need to be considered when using bi-abduction in a program analysis, as well as its theoretical properties.