George_C.__Necula
A scalable architecture for proof-carrying code
CCured: Type-Safe Retrofitting of Legacy Code
CIL: Intermediate language and tools for analysis and transformation of C programs
Efficient representation and validation of proofs
Proof generation in the touchstone theorem prover
Proof-carrying code
Safe kernel extensions without run-time checking
The design and implementation of a certifying compiler
Translation Validation for an Optimizing Compiler