Abstract
This dissertation is a case study of type safety with respect to the C programming
language. In short, C is not type safe, as its integer data types are not protected against
entering one of several possible error conditions. Once a single integer error occurs,
an entire system is potentially at risk to fail or is vulnerable to hostile takeover. The
consequence of error can be devastating, depending on the critical nature of the system.
At worst, the losses could have major implications on national security.
Contained within, the problem space is explored after dening the concepts behind
type safety. Then, a syntax like typing specication for the language is introduced and a
simplied static typing semantics for its expressions and statements are expressed before
a solution is oered with a prototype tool that statically analyzes an abstraction of the
original C source code for type safety violations. Algorithms for the tool are based on an
enumeration of the likely causes to enter an integer error, a formalization of the static
typing semantics of C, and the requirements for safe C language constructs. Because of
the tool's underling language and by using the aforementioned formalizations, the tool
has the ability to prove that its reasoning about the code it is analyzing is correct.