|
2001 – George Necula
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."
Press Release
Full Citation
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.
|
