Chandrasekhar Boyapati's Research Interests

The motivation behind most of my research is the need for reliable software. Software is rapidly becoming the foundation for our entire civil infrastructure. All activities including transportation, telecommunications, energy, medicine, and banking rely on the correct working of software systems. As software becomes more pervasive in our infrastructure, failures of software can cause more and more damage. Hence the increasing need for reliable software. Software reliability also has a significant impact on our economy. Studies estimate that bugs in software cost businesses worldwide about $175 billion annually. Making software reliable is one of the most important problems facing computer science today. Making software reliable is also one of the most challenging problems, primarily because of the inherent complexity of large software systems.

My primary research interest is software reliability, which spans the spectrum from programming languages, through program analysis, to software engineering. I am interested in all approaches for helping programmers write and maintain reliable software. I am particularly interested in developing programming languages with strong type systems to improve software reliability.

The following are some research projects I have worked on. A list of my publications appears on another page.

[SafeJava] Next Generation Safe Programming Languages

Programming languages with strong type systems have significant software engineering benefits. Types can enforce a wide variety of program invariants at compile time and catch programming errors early in the software development cycle. Types also serve as documentation that lives with the code and is checked throughout the evolution of code.

For my Ph.D. thesis, I developed a new type system for a next generation safe programming language. Our type system improves software reliability by preventing several classes of common but potentially serious programming errors. If a program type checks, the system guarantees at compile time that the program does not contain any of those errors. We designed our type system in the context of a Java-like object-oriented language; we call the resulting language SafeJava.

The SafeJava type system offers significant software engineering benefits. Specifically, SafeJava provides a statically enforceable way of specifying object encapsulation and enables local reasoning about program correctness; it combines effects clauses with encapsulation to enable modular checking of methods in the presence of subtyping; it statically prevents data races and deadlocks in multithreaded programs, which are some of the most difficult programming errors to detect, reproduce, and eliminate; it enables software upgrades in persistent object stores to be defined modularly and implemented efficiently; it statically ensures memory safety in programs that manage their own memory using regions; and it also statically ensures that real-time threads in real-time programs are not interrupted for unbounded amounts of time because of garbage collection pauses. Moreover, SafeJava provides all these benefits in a unified type system framework, indicating that seemingly different issues such as encapsulation, multithreading, software upgrades, and memory management have much in common.

We have implemented several Java programs in SafeJava. Our preliminary experience suggests that SafeJava is sufficiently expressive to support common programming patterns, its type checking is fast and scalable, and it requires little programming overhead. The SafeJava type system thus offers a promising approach for improving software reliability.

[Korat] Software Model Checking

Manual software testing, in general, and test data generation, in particular, are labor-intensive processes. Automated testing can significantly help programmers write and maintain correct programs.

We have developed Korat, a novel framework for automated testing of Java programs. Given an executable specification for a method, Korat uses the method precondition to automatically generate all nonisomorphic test cases up to a given small size. Korat then executes the method on each test case, and uses the method postcondition as a test oracle to check the correctness of each output.

Most previous work on software model checking focused on checking event sequences and not linked data structures. Korat, on the other hand, can check correctness of programs that manipulate linked data structures.

We tested several data structures using Korat, including some from the Java Collections Framework. Experimental results show that it is feasible to generate test cases from executable specifications, even when the search space for inputs is very large. Korat achieves complete code coverage, even for intricate programs that manipulated complex data structures. We also compared Korat with Alloy, a testing framework based on declarative specifications. Contrary to our initial expectation, experiments show that Korat generates test cases much faster than Alloy.

This work was done as part of the Mulsaw project.

[Upgrades] Software Upgrades

Long-lived software systems need upgrades to improve implementations, to correct errors, or even to change interfaces in the face of changing application requirements. Providing a satisfactory solution for upgrades in persistent object stores has been a long-standing challenge.

We have developed a novel mechanism for upgrading objects in a persistent object store. Our mechanism is expressive, supporting a rich set of upgrades; it is efficient and does not stop application access to persistent objects while running an upgrade; it avoids storing multiple copies of the objects; yet it provides good semantics. Our system uses a variant of ownership types to ensure that the code for upgrading objects only observes interfaces and invariants that existed at the time it was written. This enables modular reasoning about the correctness of upgrades.

We have implemented our approach in the Thor object-oriented database. Our performance results show that the overhead of our upgrade infrastructure is low.

More information on the software upgrades project can be found here.

[Thor] Persistent Object Stores

Persistent object stores provide a simple yet powerful programming model that allows applications to store objects reliably so that they can be used again later and shared with other applications. For my Master's thesis, I designed, implemented, and evaluated the performance of a distributed Java Persistent Store called JPS. JPS is built on top of the Thor object-oriented database.

JPS provides several advantages over other persistent Java systems. Unlike most of other persistent Java systems, JPS is distributed and it allows multiple clients to simultaneously access the object store. JPS is built to be used over a wide area network and scales well with large databases. JPS provides a very reliable and highly available storage. JPS also offers significantly better performance for many important types of workloads.

More information on the Thor project can be found here.

[AspectJ] Aspect-Oriented Programming

Aspect-oriented programming (AOP) is a new programming methodology that enables the modularization of crosscutting concerns. AspectJ is an extension to Java that supports AOP.

I was a summer intern at Xerox PARC in 1999, where I worked with Gregor Kiczales on AspectJ. Specifically, I was involved in the design of language constructs that make it possible to write reusable aspects as part of aspect libraries. I also built a rudimentary editor and debugger for AspectJ.

More information on AspectJ can be found here.

[Marmot] Optimizing Compilers

I was a summer intern at Microsoft Research in 2000, where I worked with Erik Ruf on the Marmot optimizing compiler. Specifically, I worked on profile-guided inlining of Java code.

More information on the Marmot project can be found here.

[Data Structures] Worst Case Efficient Data Structures

An efficient amortized data structure is one that ensures that the average time per operation spent on processing any sequence of operations is small. Amortized data structures typically have non-uniform response times, which makes them unsuitable in many important contexts, such as real time systems, parallel programs, persistent data structures, and interactive software. On the other hand, an efficient worst case data structure guarantees that every operation will be performed quickly.

The construction of worst case efficient data structures from amortized ones is a fundamental problem which is also of pragmatic interest. For my Bachelor's thesis, I solved two different open problems in data structures: the implementation of priority queues and the implementation of concatenable double ended queues with heap order. I eliminated amortization from existing data structures and proposed new worst case efficient data structures for these problems.

Chandrasekhar Boyapati