East London Massive


     The East London Massive was a loose collective of people interested in program logic, semantics, and analysis. It started around the turn of the millennium when we were working on the (at the time) new theory of separation logic. The main activity of the Massive was numerous "yak sessions" usually prefixed  by lunch and postfixed by a visit to an east end pub.  Over the years the collective massively spread out from its East London roots, as Josh went to MSR Cambridge, Cris went to IC, Richard went to Middlesex, Byron and Matthew joined from Camb, etc. Although stuff was still happening (e.g., bi-abduction, jStar..), at the end of the noughties it seemed natural to declare an end-point, and move on to other adventures, sort of like when Bowie retired Ziggy, IYSWIM.


Attacking Large Industrial Code with Bi-Abductive Inference , Dino Distefano, FMICS'09 Invited Paper

Viktor Vafeiadis wins ACM/SIGPLAN Doctoral Dissertation Award. May 2009. Way to go Viktor.

Byron Cook wins BCS Roger Needham Award. Mar 2009. Way to go Byron!

Compositional Shape Analysis by means of Bi-Abduction
C Calcagno, D Distefano, PW O'Hearn and H Yang.
Bi-Abduction displays abductive inference as a kind of inverse of the frame problem, and gives you a way to discover "small specs" for procedures, without knowing any preconditions or the procedure's callers. Oh, as a side effect, it lets you apply shape analysis to way bigger programs than before (> 1M LOC), with way less lead-up time to get the analysis ready.

•16 Sept, 2008. East London Massive releases SpaceInvader v1.0

jStar: Towards Practical Verification for Java
Dino Distefano and Matthew Parkinson,

Tutorial on Separation Logic.
CAV Invited Tutorial, July 2008, Princeton

Space Invading Systems Code.
LOPSTR Invited Talk, July 2008, Valencia

Scalable Shape Analysis for Systems Code
H Yang, O Lee, J Berdine, C Calcagno, B Cook, D Distefano and P O'Hearn. In CAV'08
We achieve the milestone of the first automatic proofs of pointer usage in entire industrial programs, Microsoft and Linux device drivers of up to 10K LOC.

•(Feb'08) James Brotherston has been awarded an EPSRC Postdoctoral Research Fellowship. Way to go, James!

Class Invariants: The End of the Road?
a short position paper by Matthew Parkinson given at IWACO'07. It contains a radical point of view that provides simple solutions to some old conundrums in OO verification.

•(April'07) Dino Distefano has been awarded a Royal Academy of Engineering/EPSRC 5-year Research Fellowship. Way to go, Dino!

•(May'07) Hongseok Yang has been awarded an EPSRC Advanced Fellowship. Way to go, Hongseok!