ROSAEC center Seoul National University

Seminars & Workshops

Speaker:Peter O'Hearn , Queen Mary, University of London
Period:2009-05-12 16:00 ~ 2009-05-12 17:00
Place:Room 308, Bldg 302, SNU
Link:SNU CSE Distinguished Lecture Series - Peter O'Hearn


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).


© Copyright 2008-2010 ROSAEC Center, Seoul National University