Some of the projects associated with the OSQ project currently under
Active Projects & Papers
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).
:: 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.
||Hybrid Concolic Testing [paper(ps)]
Rupak Majumdar and Koushik Sen,
29th International Conference on Software Engineering (ICSE'07), IEEE, 2007.
||CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools[paper(ps)]
Koushik Sen and Gul Agha, 18th International Conference on Computer
Aided Verification (CAV'06), Lecture Notes in Computer Science,
Springer, 2006. (Tool Paper).
||"Automated Systematic Testing of Open Distributed Programs"
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.
||A Race-Detection and Flipping Algorithm for Automated Testing of Multi-Threaded Programs
Koushik Sen and Gul Agha,
Haifa verification conference 2006 (HVC'06), Lecture Notes in Computer Science, Springer, 2006.
||CUTE: A Concolic
Unit Testing Engine for C
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
Automated Random Testing
Patrice Godefroid, Nils Klarlund, and Koushik Sen (PLDI 2005)
|Deputy is a C compiler that is capable of preventing
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
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
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
with Deputy can be linked directly with code compiled by other C
compilers, so you can choose exactly when and where to use Deputy
your C project.
||SafeDrive: Safe and
Recoverable Extensions Using Language-Based Techniques
Feng Zhou, Jeremy Condit, Zachary Anderson, Ilya Bagrak, Rob Ennals,
Matthew Harren, George Necula, and Eric Brewer, OSDI 2006.
Types for Low-Level Programming
Condit, Matthew Harren, Zachary Anderson, David Gay, and George
Necula. ESOP 2007
|Fast and precise points-to analysis
algorithms, with potential applications in development environments,
just-in-time compilers, and verification tools.
Context-Sensitive Points-To Analysis for Java
Manu Sridharan and Rastislav Bodik.
Proceedings of ACM
SIGPLAN 2006 Conference on Programming Language Design and
2006). Ottawa, Canada, June 10-16, 2006. Technical
report with full data. Talk
Points-To Analysis for Java [pdf]
Manu Sridharan, Denis Gopan, Lexin Shan, and Rastislav Bodik.
Published in Proceedings
Conference on Object-Oriented Programs, Systems,
Languages, and Applications (OOPSLA 2005). San Diego, CA,
16-20, 2005. Talk
|A sketching system allows the user to specify the
the code in a clean and readable form and independently
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
that the completed sketch is faithful to the original functionality
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
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
without getting bogged down in their details.
Armando Solar-Lezama, Gilad Arnold, Liviu
Tancau, Rastislav Bodik, Vijay Saraswat, Sanjit
for Finite Programs
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay
Saraswat, Sanjit A. Seshia,.
In ACM Conference on Architectural Support for
Languages and Operating Systems (ASPLOS '06), San Jose CA, October 2006
for Bitstreaming Programs
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
system properties through model-checking
|This project is working on timed systems, and aims to
use model-checking to obtain quantitative properties of systems.
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,
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.
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
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
Incrementalization speeds up function execution by using previous
execution results and only performing anew the portions of computation
that correspond to new input.
Shankar, Rastislav Bodik, et.al (PLDI 2007)
||Runtime Specialization With
Optimistic Heap Analysis [pdf]
Ajeet Shankar, S. Subramanya Sastry, Rastislav Bodik, James Smith
OOPSLA, San Diego CA, 2005.
|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.