Sciweavers

Share
APLAS
2004
ACM

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
Where APLAS
Authors Christian Skalka, Scott F. Smith
Comments (0)
books