author = {Cowan, Crispan and Po, Calton and Maier, Dave and Walpole, Jonathan
and Bakke, Peat and Beattie, Steve and Grier, Aaron and Wagle, Perru and
Yhang, Qian},
booktitle = {7th USENIX Security Symposium},
title = {{StackGuard: Automatic Adaptive Detection and Prevention of
Buffer-Overflow Attacks}},
year = {1998}
}
@InProceedings{Dep2007,
author={Condit, Jeremy
and Harren, Matthew
and Anderson, Zachary
and Gay, David
and Necula, George C.},
editor={De Nicola, Rocco},
title={Dependent Types for Low-Level Programming},
booktitle={Programming Languages and Systems},
year={2007},
publisher={Springer Berlin Heidelberg},
address={Berlin, Heidelberg},
pages={520--535},
abstract={In this paper, we describe the key principles of a dependent type system for low-level imperative languages. The major contributions of this work are (1) a sound type system that combines dependent types and mutation for variables and for heap-allocated structures in a more flexible way than before and (2) a technique for automatically inferring dependent types for local variables. We have applied these general principles to design Deputy, a dependent type system for C that allows the user to describe bounded pointers and tagged unions. Deputy has been used to annotate and check a number of real-world C programs.},