Over the past decade, much research has been devoted on obtaining robust and 
safe programs with respect to some desired properties. Researchers have been 
using a variety of techniques, including model checking, static analysis, 
formal methods, and also type systems to eliminate bugs early in the software 
development cycle. Methods based on type systems are both lightweight and 
formal, providing guarantees on two fronts - scalability and soundness. They 
typically rely on a tractable syntactic system with formal links to the 
underlying semantics of programs.

In object oriented languages, /null/ values are used to denote the absence of 
objects, and are typically the default when variables are not initialized to 
point to objects. Errors due to dereferencing null pointers are extremely 
common, if not the most common. However, most current type systems do not 
capture nullness information. In this thesis, a framework is described that 
translates C# programs to a new proposed type system that captures nullness 
information. Nullness checking rules use mainly aliasing controls together 
with specific preconditions and postconditions to validate methods.

The translation provided by the framework preserves functionality of original 
code and stores information about the original program structure that allows 
future reverse translation after any possible optimization is applied. Having 
a translation to a simpler language reduces the number of alias and nullness 
checking rules used in runtime program verification. Alias annotations added 
to the type system are partially verified inside the framework. The framework 
is able to identify contradictions in alias annotations, in the light of the 
next steps that identify dereferencing of null pointers.