| |
Active Projects & Papers |
| Quantifying
system properties |
Beaver SMT Solver | |
| Runtime optimization using dynamic heap analysis | ||
| CUTE | Points-To Analysis | Thin Slicing |
| Deputy | Programming by Sketching |
You may also want to see the list of past projects.
| Beaver SMT solver |
| Beaver is an SMT solver (decision procedure) for the theory of quantifier-free finite-precision bit-vector arithmetic (QF_BV). It supports all operators defined under QF_BV, including signed and unsigned non-linear arithmetic operators. Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich in conjunction of linear constraints such as path feasibility queries), security (rich in nonlinear arithmetic) and equivalence checking (rich Boolean structure). |
| CUTE :: A Concolic Unit Testing Engine for C and Java | ||||||||||||
| CUTE (a Concolic Unit Testing Engine for C and Java) is a tool to systematically and automatically test sequential C programs (including pointers) and concurrent Java programs. CUTE combines concrete and symbolic execution in a way that avoids redundant test cases as well as false warnings. | ||||||||||||
|
| Deputy | ||||
| Deputy is a C compiler that is capable of preventing
common C
programming errors, including out-of-bounds memory accesses as well as
many other common type-safety errors. It is designed to work on
real-world code, up to and including the Linux kernel itself. Deputy allows C programmers to provide simple type annotations that describe pointer bounds and other important program invariants. Deputy verifies that your program adheres to these invariants through a combination of compile-time and run-time checking. Unlike other tools for checking C code, Deputy provides a flexible annotation language that allows you to describe many common programming idioms without changing your data structures. As a result, using Deputy requires less programmer effort than other tools. In fact, code compiled with Deputy can be linked directly with code compiled by other C compilers, so you can choose exactly when and where to use Deputy within your C project. |
||||
|
| Points-To Analysis | ||||
| Fast and precise points-to analysis algorithms, with potential applications in development environments, just-in-time compilers, and verification tools. | ||||
|
| Programming by Sketching | ||||||||
| A sketching system allows the user to specify the
functionality of
the code in a clean and readable form and independently
specify an
implementation strategy by simply sketching its outlines.
The sketch itself is a partial description of the implementation,
a program with holes in place of low-level details that are easy to get
wrong. The compiler automatically fills in the missing details by
ensuring
that the completed sketch is faithful to the original functionality
specification. The approach has some important productivity benefits; for example, once the functionality description (the spec) has been written and debugged, one can produce implementations targeted to different architectures without the risk of introducing bugs; this simply by producing a different sketch for each desired implementation. Conversely, the same sketch can be used with many different specs, as long as they can all be implemented using the same high-level strategy. This has the added benefit of making the sketch resilient to small changes in the spec, since small changes that don't affect the high level implementation strategy will not require any corresponding changes in the sketch. But most importantly, the sketch provides a very natural way for programmers to express implementation ideas without getting bogged down in their details. |
||||||||
|
| Quantifying system properties through model-checking | ||||
| This project is working on timed systems, and aims to use model-checking to obtain quantitative properties of systems. | ||||
|
| Runtime optimization using dynamic heap analysis | ||||
| Modern languages have constricted many classes of
programming errors, such as memory and type errors. As a result,
algorithmic and semantic errors
now present a proportionally greater challenge during the development
cycle. Many static tools exist to track down such errors, but data
structure bugs, an important class of semantic bugs, resist these tools
because scalable heap analysis is very challenging. Naive dynamic
solutions
do not fare much better, as user-written or automatically generated
data structure invariant checks are often prohibitively slow, commonly
incurring at least a ten-fold slowdown. Ditto is an automatic incrementalizer for read-only data structure invariant checks in modern imperative languages like Java and C#; such checks include verifying the properties of a red-black tree or that the elements in each bucket of a hash table have the right hash code. Incrementalization speeds up function execution by using previous execution results and only performing anew the portions of computation that correspond to new input. |
||||
|
| Thin Slicing | ||
| Thin slicing is an alternative to program slicing that aims to better focus on statements most relevant to debugging and program understanding tasks. | ||
|
Page maintained by Joel Galenson.