Programs are called stateful when they manipulate the state of a computer explicitly, for example, by assignment. The main theme of the thesis is reasoning about stateful programs.  In fact, for the past 30 years, significant efforts have been made to obtain good resoning principles for such programs.  However, reasoning techniques developed so far often result in significantly more complex verification than an informal argument; consequently, they don´t attract attention from real programmers.  In the thesis, we develop O´Hearn'sidea of local reasoning, which was recently proposed to overcome such complexity problem in reasoning.  The key observation of local rasoning is that most programs show conceptual locality in thier use of storage; even though a program is able to access all global variables and all heap data structures in principle, it usually uses only a few of them.  Local reasoning uses such an observation to simplify verification: one starts reasoning about a program considering only the accessed protion of storage so as to obtain a local fact; then, a global fact is inferred simply by conjoining as an invariant a property that only depends on the other portion of storage, which is not accessed by the program.  In the thesis, we formulate a rule which allows one to derive a gloval fact from a local one.  The rule is an extension of O´Hearn´s Frame Rule for programs with procedures.  The core of the rule is to specify requirements enough to ensure that a program phrase doesn´t alter the portion of the store that a conjoined property depends on.