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.
Short bio
Peter O'Hearn is a Professor of Computer Science at Queen Mary,
University of London.
O'Hearn's research is in the logic and semantics of computation.
Throughout the 1990s, he worked on denotational semantics of programs.
Then, around the turn of the millennium, he and John Reynolds discovered
Separation Logic, which addressed the 30 year-old problem of efficient
reasoning about linked data structures in memory. He went on to develop
a Concurrent Separation Logic, which provides a modular proof method for
shared-memory concurrent programs. Recently, with a vibrant community of
researchers in the southeast of England, he has been tackling the
problem of automatic verification and analysis of programs' use of the
heap, as well as automatic program-termination analysis. This
particularly involves the SpaceInvader team (Cristiano Calcagno, Dino
Distefano, Hongseok Yang and O'Hearn) in London and their
SLAyer/TERMINATOR colleagues at Microsoft Cambridge (Josh Berdine, Byron Cook).
Resources
This will be shown to users with no Flash or Javascript.
|
