Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Plaid: Research Experiences for Undergraduates
Research Experiences for Undergraduates
Plaid Research Group: Programming Languages and Software Engineering
The Plaid research group does research applying programming language
techniques to software engineering problems. We work on all kinds
of languages, but many projects focus in particular on object-oriented
systems. Projects range from foundational development of new
object models and core calculi, to pragmatic language extensions or
analyses that can verify properties of programs written in industrial
languages like Java. The group name comes from Plaid, a new
object-oriented language currently in planning based on technologies
developed within the group and elsewhere.
Logistics
We have 1-2 positions open for Fall 2006. Positions are open
until filled. Please contact jonathan.aldrich@cs.cmu.edu
to apply.
Summer REUs: At least 2 REUs were available for Summer 2006; we expect
one or more to be available in Summer 2007. Students are
provided with a stipend, but are responsible for their own room, board,
and travel expenses.
The NSF REU program emphasizes broadening participation in computing,
and accordingly members of underrepresented groups are especially
encouraged to apply.
Current Projects
We have multiple REUs available in the general area of programming
language and software engineering research. Descriptions of some
potential projects are below, but I'm happy to discuss alternative
possibilities as well; just contact me if you're interested.
1. A System for Developing Domain-Specific Languages
Current students: Key Shin, Lutz Wrage. Positions still open for other aspects of
the project.
Domain-Specific Languages (DSLs) capture the key concepts for
developing programs in a particular domain, supporting far more
effective programming in that domain by providing natural abstractions,
succinct syntax, and automated checking of important domain
properties. Developing new DSLs, however, is hard, often
requiring intimate knowledge of compiler design and taking a long time
to perfect. We propose to build a system for more efficiently
creating DSLs based on well-known, principled techniques for giving
program syntax and semantics, including structured operational
semantics, type systems (both taught in 15-312) and rewriting
rules. The idea is that developers of a DSL would write down a
specification for the language, and an implementation and typechecker
would be automatically generated. The tool would build on ideas
from logical frameworks like CMU's Twelf, but would be more
specialized to DSLs, would focus more on efficient implementation of
languages, and would be more user-friendly to enable use by non-experts.
2. Ownership Type Inference
Former students: Will Cooper, Owen Yamauchi. Positions open for continuing work.
Ownership types promise to provide a practical mechanism for enforcing
stronger encapsulation by controlling aliasing in object-oriented
languages. Ownership is a central feature of the ArchJava language, developed in
the Plaid research group, which ensures that an object-oriented
implementation is consistent with its software architecture. This paper
provides an introduction to ownership types, and a compiler for Java
with ownership is available at the ArchJava
web site.
A major barrier to the adoption of ownership-and thus to achieving the
benefits of systems built using ownership-is that it is difficult and
time-consuming to annotate existing code with ownership types.
While previous work (including previous CMU REUs) has developed basic
algorithms for inferring ownership types, these algorithms are not yet
precise enough or scalable enough to be practical.
This project will extend a new approach to the problem: incremental,
programmer-guided ownership inference. Because ownership requires
knowledge of the programmer's design intent, our system gathers simple
design intent from the programmer and uses this together with analysis
technology to annotate the program semi-automatically. Because
ownership, as a form of context-sensitive aliasing information, is
intractable to compute for large programs, our approach will provide
tool support for incrementally annotating a few classes of the program
at a time.
The student working on this project will first evaluate existing
ownership algorithms on more realistic examples, to examine their
precision and scaling behavior. Based on this evaluation, the
student will refine the algorithms to improve their performance.
In order to make ownership inference practical, the student will build
a simple integrated development environment that allows users to
interactively specify their encapsulation intent and guide the
algorithm's inference. Finally, the student will evaluate the
final tool on code examples at scale, and write up a report describing
the algorithm, tool, and experience.
3. Data Flow Analysis Infrastructure
Former students: Tim Kirchner. Positions
open for continuing work.
The goal of this project would be to refine a data flow analysis
framework to support richer forms of analysis (e.g. interprocedural
analysis, flow sensitivity). The target data flow analysis
framework is Crystal, an Eclipse-based project currently used to teach
CMU courses on software analysis.
4. Checking Architectural Protocols in ArchJava
Current and former students: Kevin Bierhoff, Sangjin Han, Matthew Kehrt.
Many architecture description languages (ADLs) allow architects to
define protocols of interaction between components-that is, the
permitted ordering of events in the component interfaces. While
existing systems can verify compatibility between the protocols of
components, little work has been done to ensure that the implementation
of a component conforms to the specified protocol. We propose to
leverage the guarantees of ArchJava--a system which verifies that
components communicate only in ways declared explicitly in an
architecture--in order to verify component protocols. ArchJava
makes this problem easier by allowing compositional analysis: since all
inter-component communication is explicit, the problem can be decomposed
The student working on this project would participate in defining a
specification system for protocols in ArchJava, extending and
generalizing a previously developed proposal. The student will
take the lead in defining and implementing an interprocedural analysis
which tracks the protocol of a component's interface through the
component code and verifies correctness. If time permits, the student
will also use a model checker to verify the correct composition of
components, in order to verify that the whole composed system is
sound. At the end of the summer, the student will write a
technical report describing the work, which will be part of an eventual
paper submission on the topic.
5. Model Checking for Objects
This project would involve investigating ways to model check
object-oriented software systems. Very sophisticated predicate
abstraction refinement techniques have been developed in projects like
MAGIC, SLAM, and Blast for system programs written in C-like
languages. However, much less has been done for object-oriented
software. Two major challenges are handling the recursive
functions that are common in OO systems, as well as dealing with the
structure of the heap. This research project is currently less
well defined than those above, but could be refined for a very
interesting REU.
6. Protocol Specification for Objects in JML
This project would apply our previous
research specifying protocols of interaction between objects, to a
practical setting. The Java Modeling Language
(JML) is a standard specification language for Java; the goal of this
project would be to take a draft specification of an extension to JML
that defines protocols and implement it, by translation to existing JML
constructs.
Past Undergraduate Research Projects
We've had a lot of great REUs in the past. Here are some of the
undergraduates that have done research in the Plaid group, along with a
brief description of their project and a paper, if applicable.
Andi Bejlieri
Ego: a new core language with linear objects and methods, which
supports type-safe method addition, removal, and update.
Andi Bejleri, Jonathan Aldrich, and Kevin Bierhoff. Ego:
Controlling the Power of Simplicity.
In Proceedings of the POPL '06 Workshop on the Foundations of
Object-Oriented
Languages, January 2006.
Matthew Kehrt
Refined the Ego core language to simplify the design and add
support for a region-based borrowing technique.
Paper in preparation.
Will Cooper
Worked on ownership type inference, a predecessor to the
related project described above.
Paper in preparation.
Lee Salzman
PMD: a new object model unifying prototypes with multiple
dispatch
Implementation and empirical evaluation work on selective open
recursion, a technique that provides a more modular version of
inheritance (and solves the fragile base class problem) by specifying
where callbacks to subclasses are expected.