Safe programming at the c level of abstraction

Memory safety and type safety are invaluable features for building robust software. However, most safe programming languages are at a high level of memory management. This control is one reason C remains the de facto standard for writing systems software or extending legacy systems already written in C. The Cyclone language aims to bring safety to C-style programming without sacrificing the programmer control necessary for low-level software. A combination of advanced compile-time techniques, run-time checks, and modern language features helps achieve this goal. This dissertation focuses on the advanced compile-time techniques. A type system with quantified types and effects prevents incorrect type casts, dangling-pointer dereferences, and data races. An intraprocedural flow analysis prevents dereferencing NULL pointers and uninitialized memory, and extensions to it can prevent proofs demonstrate that these compile-time techniques are sound: The safety violations they address become impossible. A less formal evaluation establishes two other design goals of equal importance. First, the language remains expressive. Although it rejects some safe programs, it permits many C idioms regarding generic code, manual memory management, lock-based synchronization, NULL-pointer checking, and data initialization. Second, the language represents a unified approach. A small collection of techniques addresses a range of problems, indicating that the problems are more alike than they originally seem.