Necula's work on proof-carrying-code was more or less transformed into CCured which is nothing but memory management. It's from 2004. A lot of the interesting

Necula's work on proof-carrying-code was more or less transformed into CCured which is nothing but memory management. It's from 2004. A lot of the interesting stuff with separation logic was just getting started at that point in time. This branch led to Facebook's Infer and bi-abduction.