Typestates are useful programming language concepts to model software protocols. In this thesis we provide programming language based approaches for analysis, checking and verification of rich typestate properties over complex programs. Firstly, we use known typestate analysis approaches to capture crucial API protocol violations in Android applications. The complex control flow semantics of these programs makes the task challenging, while the excessive usage of resources and other APIs by Android makes it important. Secondly, we tackle the expressive limitations associated with typestates, and present a generalized notion of typestate using the expressive power of dependent types. These expressive typestates, which we term as Beyond-Regular Typestate (BR-typestate), are expressive enough to model many important non-regular properties (typestates can only express regular program properties), and yet have decidable type-checking, and even a decidable type-inference in certain cases. We further present a practical typestate oriented, dependently typed language incorporating these BR-typestates and present soundness results about the type system. For both the parts of the work, we create prototype systems to empirically evaluate the concepts discussed.