Stephanie Weirich <sweirich@CS.Cornell.EDU>
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.