A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code. - Robert R. Schneck; George C. Necula (CADE, 2002)

Proof-Carrying Code with Untrusted Proof Rules. - George C. Necula; Robert R. Schneck (ISSS, 2002)

A Sound Framework for Untrusted Verification-Condition Generators. - George C. Necula; Robert R. Schneck (LICS, 2003)

The open verifier framework for foundational verifiers. - Bor-Yuh Evan Chang; Adam Chlipala; George C. Necula; Robert R. Schneck (TLDI, 2005)

Type-based verification of assembly language for compiler debugging. - Bor-Yuh Evan Chang; Adam Chlipala; George C. Necula; Robert R. Schneck (TLDI, 2005)