Sciweavers

TLDI
2010
ACM

Verifying event-driven programs using ramified frame properties

13 years 3 months ago
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...
Neel R. Krishnaswami, Lars Birkedal, Jonathan Aldr
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where TLDI
Authors Neel R. Krishnaswami, Lars Birkedal, Jonathan Aldrich
Comments (0)