Verifying event-driven programs using ramified frame properties

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. These bidirectional linkages pose a serious challenge to verification, because their correctness relies upon a global invariant over the object graph. We show how to modularly verify programs written using dynamically-generated bidirectional dependency information. The critical idea is to distinguish between the footprint of a command, and the state whose invariants depends upon the footprint. To do so, we define an application-specific semantics of updates, and introduce the concept of a ramification operator to explain how local changes can alter our knowledge of the rest of the heap. We illustrate the applicability of this style of proof with a case study from functional...

• Type: Conference
• Year: 2010
• Where: TLDI
• Authors: Neel R. Krishnaswami, Lars Birkedal, Jonathan Aldrich
• Keywords: Bidirectional Dependency Information, Dependency Information, Formal Methods, Functional Reactive Programming, TLDI 2010