Grace Murray Hopper Award
United States – 2001
CITATION

For his seminal work on the concept and implementation of Proof Carrying Code, which has had a great impact on the field of programming languages and compilers and has given a new direction to applications of theorem proving to program correctness, such as safety of mobile code and component-based software.


The key idea behind PCC is that an untrusted software program can be quickly verified that it is safe to execute if it comes accompanied by a formal proof of compliance with a predetermined safety policy. This puts the burden of proving safety on the code producer and enables the code receiver to enforce safety with a simple and fast proof- checking infrastructure.

With Proof-Carrying Code, Professor Necula has made a fundamental contribution that spans several areas of Computer Science including operating systems, programming languages, logics, theorem provers and most importantly security. Professor Necula is recognized both for inventing the concept and for addressing the theoretical and technical issues involved in making Proof-Carrying Code practical.