|
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.
|
|