Program Analysis Group
· Computer Science and Artificial Intelligence Laboratory ·
· Massachusetts Institute of Technology ·

#  Program Analysis Group
T#  Publications
T#  People
T#  Projects
|T#  Potential projects (for students)
|T#  Javari: reference immutability
|T#  JSR 308: annotations on Java types
|T#  Eclat: test generation
|T#  Daikon: invariant detection
|T#  Generics-related refactoring
|T#  Continuous testing
|T#  Fjalar: C/C++ framework
T#  Past Projects
|T#  Fault Invariant Classifier
|T#  IO Automata
|T#  Jiggetai
|T#  Upgrade safety
|T#  PittSFIeld: fault isolation
#  PAG Internal
This is a partial list of projects. Also see our list of potential projects ( only) and our publications.

Upgrade Safety: Predicting Incompatible Software Upgrades

How can one tell whether upgrading to a new version of a library will cause another part of a complex system to malfunction? By inferring operational properties from a component's execution, we can predict when an upgrade might cause disruptive changes.

Continuous Testing

Continuous testing provides rapid feedback to developers about failures in their test suite as source code is edited. This feedback can help speed software development. Test prioritization and factoring can further improve the speed and quality of feedback.

Eclat: Automatic Generation and Classification of Test Inputs

Suppose you have written a piece of software and tested it on a few inputs, which you have made into a small test suite. The goal of Eclat is to automatically generate new inputs to the program with two qualities:
  • They make the software behave differently from the existing inputs.
  • They can reveal faults in the software.

Compile-time-checked immutability constraints for Java

Javari is an extension of the Java language that permits the specification and compile-time verification of immutability constraints. Such immutability ("read-only") constraints provide valuable documentation, aid program understanding, reveal errors at compile time, and can assist optimization.

JSR 308: Annotations on Java types

JSR 308 “Annotations on Java Types”, enriches the Java annotation system. For example, it permits annotations to appear in more places than Java 6 permits; one example is generic type arguments (List<@NonNull Object>). These enhancements to the annotation system require minor, backward-compatible changes to the Java language and classfile format. These changes will be part of the Java 7 language.

Verifiable Alignment-based Binary Sandboxing

Sandboxing, also known as software-based fault isolation (SFI), modifies code at the instruction level to enforce control flow and memory access safety. PittSFIeld implements a new technique that makes efficient and robust sandboxing possible with variable-length instructions. Separate verification and a machine-checked formal proof increase confidence in the system's security.

Daikon: Dynamic Invariant Detection

Daikon aims to dynamically detect invariants about a program's data structures -- the sort that might be written in an assert statement or a formal specification. These properties are useful for a wide variety of software construction, understanding, reuse, and modification tasks, but they are usually absent from code.

Generics-related refactorings for Java

You have an application written in pre-1.5 Java and want to upgrade it to take advantage of the increased type safety and expressiveness provided by generics. Our analysis and tool that we wrote will let you do that efficiently as a source-to-source refactoring.

Fjalar: A Dynamic Analysis Framework for C and C++ Programs

It is often difficult to implement robust and scalable dynamic analysis tools for C and C++ programs due to lack of memory and type safety and complex constructs in these languages. For instance, the run time system does not keep track of array sizes or whether values have been initialized. Fjalar is a framework that addresses these difficulties and facilitates the construction of dynamic analysis tools for C and C++ programs.

Past projects

Theorem Proving Distributed Algorithms via Dynamic Analysis

Theorem provers are notoriously hard to use, but they are the only tools that can verify infinite state distributed systems. We present a method to make theorem proving safety properties of distributed algorithms modeled as I/O automata more productive, using lemmas generated by dynamic invariant detection and tactics specific to the model.

Software Fault Identification via Dynamic Analysis and Machine Learning

The Fault Invariant Classifier is a technique to automatically recognize faults in programs based on models of other faults. An implementation of the FIC uses dynamic invariant detection and support vector machine and decision tree software to model and classify program invariants as fault-revealing and non-fault-revealing.

Jiggetai: Inference of Generic Types for Java

Jiggetai is a tool that reads Java source code and infers generic types for classes that are used polymorphically. It then emits the source code translated to use the more expressive types; these types not only help to prevent several kinds of error, but also serve as a more precise specification.

Creating and Training Adaptive Software via Program Steering

Software systems often contain several distinct modes of operation with predetermined behavior and hard-coded decisions for switching between modes. Program steering utilizes dynamic program analysis to determine the optimal modality for a system in any environment, even when the software was not written with that situation in mind.