Modularity and code reuse are two important features of object-oriented programming. Modularity means that adding new components does not require reverification or respecification of existing components. A common form of reuse in object-oriented programs is to add new subtypes to existing types and to invoke already existing procedures with objects of these new types. In such cases, behavior of programs that contain these procedures also depend on the behavior of the new subtype objects. Reverifying the code that uses existing procedures whenever new types are added is not practical and is not modular. Thus, a notion of behavioral subtyping that allows sound modular reasoning is important for object-oriented programming;In this dissertation, we study behavioral subtyping for arbitrary abstract data types in the prescence of mutation and aliasing. We propose two notions of behavioral subtyping. Strong behavioral subtypes have objects that act like supertype objects in all cases, whereas as weak behavioral subtypes have objects that only need to act like supertype objects when manipulated as supertype objects. Both these notions allow sound modular reasoning based on the static types of variables in programs. Weak behavioral subtyping allows conclusions about programs based on the effects of individual procedures but restricts certain forms of aliasing. Strong behavioral subtyping allows all forms of aliasing but permits conclusions based only on the history constraints of the types. History constraints are the reflexive and transitive properties preserved by objects of a type across different states of a program. We prove that both these behavioral subtype notions are sufficient for sound modular reasoning.