History Effects and Verification

9 years 2 months ago
History Effects and Verification
This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher-order programs. The properties verified are based on the ordered sequence of events that occur during program execution--an event history. Our type and effect systems automatically infer conservative approximations of the event histories arising at run-time, and model-checking techniques are used to verify logical properties of these histories. Our language model is based on the -calculus. Technical results include a powerful type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the history effects inferred by the type inference algorithm, allowing static enforcement of history- and stackbased security mechanisms.
Christian Skalka, Scott F. Smith
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Authors Christian Skalka, Scott F. Smith
Comments (0)