Current Projects
- Portable Library Models: I have been working on portable models of source code libraries, called synopses, for side-effect analysis. The idea is that since static analysis tools need to analyze libraries as well as the program source, we should make the libraries easy to analyze by modeling them as source code. Since the models are just source code, they will work with any static analysis tool. The open issues here are how to automatically construct the models (we want them to be very small) from existing library implementations and what type of information needs to be modeled.
- Visualization and Navigation of Data Repositories: Peter Bergstrom (graduate student) is working on finding new ways to visualize and navigate large data repositories such as the digital libraries of ACM and IEEE. Peter started this work as his undergraduate thesis by looking at the papers in a single conference, and hopes to extend its scope. We want to look at handling larger amounts of data and also different types of data, such as source code and images.
- Refactoring Detection: Todd King (graduate student) has done some really nice work on automatically detecting refactorings in C# source code. We analyzed several open source C# programs and found that his tool could correctly detect refactorings about 90% of the time.
Past Projects
- Market Microstructure Software: Sanjiv Das (finance department) is working on creating a real-time trading lab in the business school. Some computer engineering students worked on developing a prototype of the software, and Clayton Hoefer and Joe Mastroieni (former undergraduate students) built an enhanced version of the system as part of their senior capstone project.
- Process Model Verification: Dan Weeks (former graduate student) and I worked with John Noll to write a verification tool for PML, a process modeling language he designed. PML is lightweight and very easy to use, having the look and feel of a high-level scripting language. The downside of this design is that no error checking is done until run-time. Dan's tool tries to verify that a model is correct before enactment by looking for common mistakes.
- Slicing with Dynamic Points-To Data: Markus Mock (University of Pittsburgh, now at Google) and I worked on using dynamic points-to data in a program slicing tool. The key idea is that since the dynamic points-to data is optimistic rather than conservative like static points-to data, program slices should be smaller and therefore for useful. What we found however is that the slices weren't that much smaller, which we attribute to the fact if a program slice is large, then it's just inherently large because of the way slices are defined. As a result of this work, we both were invited to a Dagstuhl seminar on understanding program dynamics.