I agree, TypeState seems especially interesting. This paper from one of the comments does a good job describing it: http://www.cs.cmu.edu/~aldrich/papers/classic/tse12-typestat...