Trace Effects and Object Orientation
Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. They are sufficiently expressive to statically enforce language-based security policies such as stack inspection. In this talk I describe a type and effect analysis for obtaining trace effects of Object Oriented programs in a subset of Java. I show how the analysis is significantly complicated by the interaction of trace behavior with inheritance and other Object Oriented features, especially overridden methods, dynamic dispatch, and downcasting. To address these issues, I describe an expressive type and effect inference algorithm combining polymorphism and subtyping/subeffecting constraints which is able to obtain a flexible trace effect analysis in an Object Oriented setting.