Contact:

George Necula, (Retired) Professor – Electrical Engineering and Computer Science
Currently, working at Google Switzerland.
Email: necula AT cs DOT berkeley DOT edu

Publications, Curriculum Vitae

Technical Blog (last updated 2015)

Past 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.
• 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.

Hinted Garbage Collection. See the ISMM'13 paper.

SwiftHand: an automated testing tool for Android GUI applications and Javascript/HTML5. OOPSLA'13 paper

Testing with Spies. This research is looking into ways to write behavioral tests that are very easy to maintain. One idea is to add to the code spy statements that capture key state variables, much like logging statements. The collected logs are used to compare executions and look for behavior changes. Of course, the comparison has to be done smartly to detect values that are expected to change from run to run.

Specification and Verification of Parallel Programs. We developed NDSEQ (NonDeterministic SEQuential Specifications), a novel lightweight specification method to specify the correctness of parallelism in a program. In particular, NDSEQ specification of a program specifies the correctness of a program's parallelism using a sequential version of the program with controlled nondeterminism. Such a nondeterministic sequential specification allows (1) the correctness of parallel interference to be verified independently of the program's functional correctness, and (2) the functional correctness of a program to be understood and verified on a sequential version of the program, one with controlled nondeterminism but no interleaving of parallel threads. See our papers at: PLDI'2011, PPoPP'2012, ASPLOS'11, HotPar'10,

Concurrit: Domain-specific language for testing Concurrent Programs. It is very hard to write tests that seek or reproduce parallel bugs. Concurrit is a domain-specific language that allows the test writer to control the actors and their interleaving scenarios, in order to reproduce certain concurrency scenarios. See our papers at: PLDI'13, HotPar'12 .

Graduate students

Graduated

• Patrick Li
• Philip Wontae Choi (PhD 2017, at Google)
• 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 MIT)
• Jeremy Condit (PhD 2007, now at Google Inc.)
• Matthew Harren (PhD 2007, now at Google Inc.)
• Evan Bor-Yuh Chang (PhD 2008, now at University of Colorado, Boulder)
• Benjamin Hindman
• Raluca Sauciuc (MS 2012, now at Google)
• Derrick Coetzee
• Philip Reames (MS 2013, now at Azul Systems)

Personal

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