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.

• Type: Conference
• Year: 2004
• Where: APLAS
• Authors: Christian Skalka, Scott F. Smith
• Keywords: APLAS 2004, Model-checking Techniques, Programming Languages, Type Effect System, Type Inference Algorithm