Verifying event-driven programs using ramified frame properties
Neel Krishnaswami, Lars Birkedal, Jonathan Aldrich · 2010
Interactive programs, such as GUIs or spreadsheets, often maintain dependency information over dynamically-created networks of objects. That is, each imperative object tracks not only the objects its own invariant depends on, but also all of the objects which depend upon it, in order to notify them when it changes.