Active Projects & Papers

Some of the projects associated with the OSQ project currently under development.
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.
[MS07] Hybrid Concolic Testing [paper(ps)] [paper(pdf)]
Rupak Majumdar and Koushik Sen, 29th International Conference on Software Engineering (ICSE'07), IEEE, 2007.
[SA06] CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools[paper(ps)] [paper(pdf)]
Koushik Sen and Gul Agha, 18th International Conference on Computer Aided Verification (CAV'06), Lecture Notes in Computer Science, Springer, 2006. (Tool Paper).
[2SA07] "Automated Systematic Testing of Open Distributed Programs"
[paper(ps)] [paper(pdf)] [extended paper(ps)] [extended paper(pdf)] [tool]
Koushik Sen and Gul Agha, International Conference on Fundamental Approaches to Software Engineering (FASE'06) (ETAPS'06 conference), Lecture Notes in Computer Science, Springer, 2006.
[3SA07] A Race-Detection and Flipping Algorithm for Automated Testing of Multi-Threaded Programs
[abstract] [bibtex] [paper(ps)] [paper(pdf)]
Koushik Sen and Gul Agha, Haifa verification conference 2006 (HVC'06), Lecture Notes in Computer Science, Springer, 2006.
[SMA05] CUTE: A Concolic Unit Testing Engine for C [paper(ps)] [paper(pdf)]
Koushik Sen, Darko Marinov, and Gul Agha.
ACM SIGSOFT Distinguished Paper Award Winner. Extended version invited for publication in ACM Transactions on Software Engineering and Methodology (TOSEM)

[GKS05] DART: Directed Automated Random Testing [paper(ps)] [paper(pdf)]
Patrice Godefroid, Nils Klarlund, and Koushik Sen (PLDI 2005)

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.
[ZCABEHNB06] SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques [pdf]
Feng Zhou, Jeremy Condit, Zachary Anderson, Ilya Bagrak, Rob Ennals, Matthew Harren, George Necula, and Eric Brewer, OSDI 2006.

[CHAGN06] Dependent Types for Low-Level Programming [pdf]
Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George Necula. ESOP 2007

Points-To Analysis
Fast and precise points-to analysis algorithms, with potential applications in development environments, just-in-time compilers, and verification tools.
[SR06] Refinement-Based Context-Sensitive Points-To Analysis for Java [ pdf]
Manu Sridharan and Rastislav Bodik.
Proceedings of ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (PLDI 2006). Ottawa, Canada, June 10-16, 2006. Technical report with full data. Talk slides 
[SGSB05] Demand-Driven Points-To Analysis for Java [pdf]
 Manu Sridharan, Denis Gopan, Lexin Shan, and Rastislav Bodik. Published in Proceedings of Twentieth Conference on Object-Oriented Programs, Systems, Languages, and Applications (OOPSLA 2005). San Diego, CA, October 16-20, 2005. Talk slides

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.
[SATBSS07] Sketching Stencils
Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodik,  Vijay Saraswat, Sanjit Seshia (PLDI2007)
[STBSS06] Combinatorial Sketching for Finite Programs [ pdf ]
 Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, Sanjit A. Seshia,. In ACM Conference on  Architectural Support for Programming Languages and Operating Systems (ASPLOS '06), San Jose CA, October 2006
[SRBE05] Programming by Sketching for Bitstreaming Programs [ pdf ]
Armando Solar-Lezama, Rodric Rabbah, Rastislav Bodik, Kemal Ebcioglu. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '05), Chicago IL, June 2005

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.
[HP06] Timed Alternating-Time Temporal Logic [ pdf]
Thomas A. Henzinger and Vinayak Prabhu, in Proceedings of the Fourth International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science, Springer, 2006. 
[HMP05] Quantifying Similarities between Timed Systems [pdf]
Thomas A. Henzinger, Rupak Majumdar, and Vinayak Prabhu, in Proceedings of the Third International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science 3829, Springer, 2005, pp. 226-241.

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.
[SB07] ditto
Ajeet Shankar, Rastislav Bodik, et.al (PLDI 2007)
[SSBS05] Runtime Specialization With Optimistic Heap Analysis [pdf]
Ajeet Shankar, S. Subramanya Sastry, Rastislav Bodik, James Smith
OOPSLA, San Diego CA, 2005. 

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.
[SFB07] Thin Slicing [pdf ]
Manu Sridharan, Stephen J. Fink and Rastislav Bodik. Technical Report No. UCB/EECS-2006-184. Revised version to appear in ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI 2007).


Page maintained by Joel Galenson.