Stephanie Weirich http://www.cs.cornell.edu/sweirich Run-time type analysis for program verification Modern typed programming languages support type polymorphism: A function may be called without knowing the exact type of the argument. For example, in Java, the actual class of a method argument may be a subclass of the expected argument. In ML or Haskell, functions may be defined to operate over arguments of any type. Furthermore, many of these languages support the ability to determine the actual type of a value during the execution, if that type has been hidden. For example, in Java, the keyword "instanceof" determines if the actual class of an object is a subclass of the given type. At the same time, advanced type systems allow the user to express and verify a large number of properties about her program. These properties might include checking that the code follows locking protocols, that the code uses a limited number of resources, that the code deallocates all of the memory that it allocates, or that all array accesses are within range. However, these properties are difficult to verify statically, and many programs may needlessly be rejected. In this talk, I will describe how technology for run-time type analysis can be used in a system for verifying program execution time.