Contact:

George Necula, Associate Professor – Electrical Engineering and Computer Science
Email: necula AT cs DOT berkeley DOT edu
Address: 783 Soda Hall, Berkeley, CA 94720 Phone: 510 643 1481; Fax: 510 642 3962

I am currently on industrial leave at Rinera Networks.

Publications, Curriculum Vitae

Current research projects

• Deputy a compiler for C that uses programmer annotations to prevent most memory safety errors.
• Open Source Quality Project. This umbrella project investigates techniques and tools for assuring software quality: finding and removing defects in software systems, as well as improving current methodology for designing high-quality software systems at the outset.
• Extensible Shape Analysis (XISA) This project explores novel ways in which we can involve programmers to contribute specifications for the purpose of checking complex data structure manipulations.

Past research projects

• CCured: Type-safe variant of C, along with tools for porting legacy applications. You can try CCured online
• Random Interpretation is a program analysis technique that relies on executing a program fragment on a number of random inputs. The obvious problem with a naïve implementation of such random testing is that it lacks soundness. We have shown that for certain program properties the interpretation can be suitably modified such that we can make the probability of unsound results very small.
• Touchstone is a certifying compiler for Java, used in conjunction with PCC. You can try Touchstone online.  
• Translation Validation for Optimizing Compilers. Techniques for checking that the optimizers do not change the semantics of the code they process.
• CIL (C Intermediate Language) is a high-level representation along with a set of tools that permit easy analysis and source-to-source transformation of C programs.
• Elkhound is a parser generator, similar to Bison, but uses the Generalized LR parsing algorithm. We used it to produce a C++ front-end.
• Finding and Preventing Run-Time Error Handling Mistakes. Language-level exceptions make it easy to signal that an error has happened, but do not make it easy to handle the error. We showed that this leads to a large number of bugs in Java code, and we proposed a language mechanism for addressing this problem.
• The Open Verifier is a framework that allows even untrusted parties to develop safety verifiers for untrusted code. For example, instead of using the built-in and trusted Java Bytecode verifier, an untrusted party may supply a replacement verifier, which perhaps functions even on optimized bytecode. The challenge is to provide a framework that ensures the soundness of such verifiers, without posing an undue burden on the verifier developer.
• Proof-Carrying Code (PCC) is a technique for safe execution of untrusted code. The basic idea is to require the code producer to generate a formal proof that the code meets the safety requirements set by the code receiver. You can try PCC online (as used with the Touchstone certifying compiler for Java).
• Specifying and Verifying Data Structure Invariants.
• Certifying Theorem Prover is a state-of-the-art theorem prover that outputs formal proofs for the theorems that it proves. Still going on, but without a web page.

Graduate students

Current

• Benjamin Hindman
• Raluca Sauciuc
• Evan Bor-Yuh Chang

Graduated

• Robert Schneck (PhD 2004, at Google and Acorn Community)
• Sumit Gulwani (PhD 2005, at Microsoft Research)
• Scott McPeak (PhD 2005, at Coverity)
• Westley Weimer (PhD 2005, at University of Virginia)
• Adam Chlipala (PhD 2007, now at Jane Street)
• Jeremy Condit (PhD 2007, now at Microsoft Research)
• Matthew Harren (PhD 2007, now at Google Inc.)

My Family

My daughter Deanna is working on a web site about animals.

Where I am from

I am originally from Baia Mare, Romania situated in the Maramures county of northern Transylvania.