CS169, Software Engineering
George Necula, Professor – Electrical Engineering and Computer Science
: necula AT cs DOT berkeley DOT edu
783 Soda Hall, Berkeley, CA 94720 Fax
: 510 642 3962
Current research projects
- 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:
- 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:
- Hinted Garbage Collection. See the ISMM'13 paper.
- Testing with Spies.
- SwiftHand: an
automated testing tool for Android GUI applications.
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
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.
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
- 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.
Philip Wontae Choi