FACULTY
RESEARCH GUIDE
2004-05
Computer Science Department
Carnegie Mellon University
©2003
Carnegie Mellon University
This file presents the current research interests of the faculty
members of the Carnegie Mellon University Doctoral Program in Computer Science,
along with those of associated faculty of other departments. Each person listed has written his or her own
section of the Guide. There has been no
attempt to eliminate redundancy by combining descriptions of related work. In addition to the research descriptions,
indices at the end of the document list the faculty by interest keywords and by
project names.
The primary purpose of the Guide is to acquaint new and prospective
members of our community, especially doctoral students, with the on-going
research and with the faculty involved.
We also use the Guide to inform outside colleagues and visitors, and to
direct those looking for persons knowledgeable about any particular topics.
Assistant Professor, Computer Science
My research spans
several areas of database management systems (DBMSs). The goal is to discover
innovative ways to improve database system performance, inspired by the
behavior characteristics of popular database applications on modern machines.
The long-term research plan is to explore the interaction between database
systems and other related areas towards improving performance (compilers,
networks) and expanding functionality (artificial intelligence, user
interfaces).
One
of the topics I am currently working on the impact of the hardware and
operating system on the behavior of database workloads. Hardware has become
extremely sophisticated, and it employs many levels of non-blocking memory and
highly parallel instruction execution techniques. The operating system and
compilers successfully exploit the underlying hardware to deliver the high
performance to the application level. This is great, because modern database
applications (i.e., geographical/map applications) are computationally
intensive, therefore they should fully exploit the new capabilities.
But do they?
Recent studies show
that database workloads do not exploit the capabilities of modern machines. For
most database applications, an increase in processor speed does not result in a
commensurate improvement in application performance performance. Although
commercial database systems such as DB2, Oracle, or SQL Server are easy to
install and operate on just about any machine/operating system, in reality
database system technology has evolved independently from operating systems and
computer architecture; however, its performance still depends much on resource
management and the underlying hardware. Therefore, the database system must
learn to utilize better the functionality offered by the OS and the hardware.
There are two related projects:
Cache-Resident Data Bases (CRDB). It has been proven that database
workloads suffer from memory-related delays caused by cache misses. CRDB studies
software techniques to provide the performance illusion that the database is
entirely in the cache, i.e., avoid or hide the latencies of cache misses. Such
techniques include dynamic cache block coloring of instruction, data, and
metadata, and prefetching of cache blocks likely to be used next by database
algorithms.
Query-Pipeline (Q-Pipe). This large long-term project introduces a
revolutionary staged design for high-performance, evolvable DBMS that are easy
to tune and maintain. We break the database system into modules and to
encapsulate them into self-contained stages connected to each other through
queues. The staged, data-centric design remedies the weaknesses of modern DBMS
by providing solutions at both a hardware and a software engineering level.
There are multiple problems associated with this new database system
architecture, ranging from job queueing and scheduling with multiple
constraints to multi-query processing and optimization.
A related research
area is storage management for database systems of the new millennium. Modern
database systems do not need (or want) to care about the storage devices used
to store the data, but they want optimal performance. There are several
research directions in this area: First, we are looking into transparently
exporting the device characteristics upwards to the database storage manager
and achieving optimal use of the device. We are designing Fates, a smart
storage subsystem that aims at dynamically allocates memory to store data of
interest, optimizes I/O accesses, and performs transparent data placement onto
devices such as disks, RAID, or MEMS.
Finally, a newer topic of interest is supporting
scientific (astronomy or biology) applications by automatically administering
the database system that stores and manipulates the scientific data. We work
with the astronomers in the Sloan Digital Sky Survey (sdss.org) group and their
data using commercial database systems. While working with a real astronomy
dataset, we made the important observation that query execution performance
depends not only on the indexes and views, but also on the definition of the
tables in the database schema. Using the automated index-discovery algorithms
on a poorly designed initial schema will result in a proposed set of thick indices
with several replicated fields, each of which destined to improve performance
of a single query. To help design an efficient schema we introduced AutoPart, a
new tool for automated physical design that modifies the original database
schema into a vertically partitioned one according to a set of representative
queries. AutoPart incorporates the well-known advantages of data table
partitioning into a family of novel automatic schema modification algorithms.
The system uses the optimizer's advice to determine "bottleneck"
tables in the original schema, and performs lossless decomposition on the
tables while balancing cost to potential performance improvements. Experimental
results using the Sloan Digital Sky Survey dataset reveal that the workloads
run twelve times faster on the striped database than on the original database.
More importantly, the automatic index generation runs an order of magnitude
faster and produces drastically fewer and slimmer indices on the striped
database. We will continue this research by expanding AutoPart to accommodate
dynamic schema and index reorganization when changes in the workload occur, and
to propose schema and indexes even when the actual queries are not available.
Personal web site:
http://www.cs.cmu.edu/~natassa
CMU Database Group
web site: http://www.db.cs.cmu.edu
JONATHAN ALDRICH
Assistant Professor,
Institute for Software Research, International and Computer Science
My research applies language and program analysis technology to the challenges of designing, building, and evolving software systems. I address these challenges using formal techniques in the context of mainstream programming systems such as Java. To evaluate my work, I perform exploratory case studies on real applications. These studies assess both the usability of the techniques I develop and the engineering tradeoffs that they entail.
Software Architecture represents the high-level
structure of a software system, and can be used to build, analyze, and evolve
software more effectively. My work on
the ArchJava project was the first to provide a rigorous, compile-time
guarantee that an object-oriented software system conforms to a specification
of architectural structure. Initial case
studies on real programs suggest that ArchJava is practical and provides
engineering benefits during software evolution.
I am currently extending ArchJava to specify and enforce richer
architectural properties, such as the temporal sequence of architectural
events. With David Garlan, I am also
exploring more effective ways to formally model and analyze software
architecture in the presence of dynamism and multiple architectural views.
Lightweight Formal Methods show great promise for helping software engineers write secure software, avoid defects, and achieve performance and other non-functional goals. I am interested in how language and type system design can be used to more effectively check a range of critical software properties. For example, an ownership type system we are developing will provide the first lightweight, flexible, and general way to modularly reason about programs with state. We would like to build on this type system to support modular model checking of object-oriented programs. Language design can also aid in checking object protocols, such as the required ordering of calls to a socket-based communication library. Finally, I am interested in lightweight verification tools for embedded and real-time systems, which are notoriously hard to build and maintain.
Objects and Aspects are emerging programming language
paradigms that support cleaner program designs and easier software
evolution. My current work focuses on
ways to make these languages more expressive while also providing better human
and automated reasoning capabilities.
For example, I am developing the first module system for aspect-oriented
programming languages that will allow a library provider to verify properties
of their implementation that will continue to hold even if clients write
aspects that affect the library. Other
projects include better language and tool support for error handling, and a
novel object model that supports both dynamic inheritance and multiple
dispatch.
Interest keywords (for the faculty interests index):
formal methods, language design, object-oriented programming, aspect-oriented
programming, programming languages, program analysis, semantics of programming
languages, software architectures, software engineering, specification, type
theory, model checking
Professor, Computer Science
My main research interest is in the interaction between algorithms and
languages, mostly in the context of parallel computing, and has consisted of
both theoretical and experimental work. As programming languages become higher
level, implementations become more complex, and parallelism becomes pervasive,
users are naturally becoming more removed from the hardware and its costs.
Rather than trying to bring programmers down to the level of the machine to
understand and get good performance, however, I believe that we should be
trying to bring languages and cost models up to the level of the programmer. My
research therefore centers around questions of how to model costs (e.g. time
and space) for very-high level programming constructs (e.g. dynamic
parallelism, futures, garbage collection), of how to design systems so these
costs have meaning, and of how to make use of these features in effective
algorithms design.
My recent work includes
work on the PSCICO project with Gary Miller, Bob Harper and Peter Lee. Here we
are looking at how to use very-high level programming constructs in geometric
and scientific algorithms. We hope this project will give guidance to future
language design, and will identify new ways of thinking about algorithm
implementation. I also work on applied algorithms, parallel garbage collection,
parallel scheduling, efficient parallel algorithms, and continue to work, to
some extent, on the NESL programming language, a parallel language that my
students and I developed in the early 90s.
Professor, Computer Science
My main research interests are in computational learning
theory, on-line algorithms, and approximation algorithms, as well as in a variety
of topics that combine several of these areas.
Computational Learning Theory. The goals of computational learning theory are to provide a mathematical understanding of the issues involved in getting machines to learn from experience, as well as to provide new analyzable algorithms. One problem I am particularly interested in is: how quickly can one learn an arbitrary boolean function over n variables, given only the guarantee that it depends on just a small number r << n of them? Can we do this substantially faster than n^r? This seems to be at the heart of classic difficult problems such as the problem of learning general DNF formulas, and also has cryptographic implications. Another, more general, question is: what are good methods for learning from both labeled and unlabeled data, and how can the algorithmic and sample-complexity issues be best formalized in a PAC-style theoretical model? There also seem to be interesting connections between this question and problems of constructing good graph separators. Finally, we have recently begun exploring relations between active learning and the problem of preference-elicitation in combinatorial auctions.
On-line algorithms. On-line algorithms involve repeatedly making
decisions knowing only the past history and without knowledge of future
events. The goal is to come up with an
algorithm such that, no matter what events end up happening, you do not greatly
regret the decisions you made. (I.e.,
your perormance is within a small factor of the best you could have done in
hindsight; this factor is called the "competitive ratio" of the
algorithm). For example, you can think
of portfolio allocation problems, or matching buyers with sellers in an
electronic auction; or, in a more CS context, adaptive data structures that can
adjust their internal state based on the series of accesses made so far. One direction I have been particularly
interested in is using online learning techniques as tools for attacking some
of the fundamental open questions in this area.
In many cases these tools provide a way to combine multiple online
algorithms so that in the end you perform nearly as well as the best of them in
hindsight. I have been working on
applying this in the design of adaptive data structures and in algorithms for
online auctions. I have also recently
been working on online scheduling problems and ways of combining multiple
objective functions.
Approximation
algorithms. Many important problems
turn out to be NP-hard, implying that it is unlikely there will be algorithms
for them that are both efficient and optimal in the worst case. One approach,
then, is to find algorithms that produce approximately-optimal solutions. I am
interested in a variety of problems of this sort including traveling
salesman-like problems, graph coloring-like problems, and problems in DNA
sequencing. For example, an interesting problem from this perspective is the
"trick-or-treater's problem": given a weighted graph (a map
of a neighborhood), a starting location (your house), and an integer k (a candy
bag of a certain size), find the shortest route that visits at least k vertices
(enough different houses to fill the candy bag) and returns back to the
start. This problem turns out to have
good constant-factor approximations; that is, you can give an efficient
algorithm that always finds a tour not too much longer than optimal. But, if you fix the length of the tour and
ask to approximate the number of vertices, then no good approximations are
known. Broadly, the key challenges are
to understand the approximability of fundamental problems, as well as to better
understand the set of fundamental techniques for achieving good approximation
guarantees. Recently we have been
working on approximation algorithms for an interesting graph clustering problem
motivated from machine learning.
Distinguished Career Professor, Computer Science
Complexity and Real Computation. In
1989, Steve Smale, Mike Shub and I introduced a theory of computation and
complexity over an arbitrary ring or field R. In 1997, along with Felipe
Cucker, we published a book, Complexity and Real Computation (Springer-Verlag).
From our Introduction: "The classical theory of computation had its origin
in the work of logicians -- of Godel, Turing, ... , among others -- in the
1930's. The model of computation developed in the following decades, the Turing
machine, has been extraordinarily successful in giving the foundations and
framework for theoretical computer science.
"The
point of view of this book is that the Turing model (we call it
"classical") with it's dependence on 0's and 1's, is fundamentally
inadequate for giving such a foundation for modern scientific computation,
where most of the algorithms - with origins in Newton, Euler, Gauss, et al. -
are real number algorithms."
Our approach
applies to the analysis of algorithms over continuous domains as well as the
discrete. The classical theory is recovered if we allow the ring R to be Z_2
(the integers mod 2). But now R can also be the real or complex numbers, or any
other field. The familiar complexity classes P, NP and fundamental question
"does P= NP?" make sense over R and moreover, relate explicitly to
fundamental problems in mathematics such as Hilbert's Nullstellensatz. Thus, we
are particularly interested in research concerning the complexity of algorithms
that solve systems of polynomial equations.
Transfer Principles for Complexity
Theory. A powerful tool of the
classical theory is that of reduction: If problem A can be shown to be reducible
to problem B, then techniques for solving B can be used to solve A.
Classically, A and B are both discrete, i.e. defined over the same domain Z_2.
But now we have an additional powerful tool, namely that of transfer: When
there was essentially only one model of computation (i.e. over Z_2), it didn't
make sense to transfer complexity results from one domain to another. But now,
transfer becomes a real possibility. We can ask: Suppose we can show P=NP over
the complex numbers (using all the mathematics that is natural here). Then can
we conclude that P=NP over another field such as the algebraic numbers or even
over Z_2? (Answer: Yes and essentially yes.)
I am
particularly interested in such transfer results and problems that appear in
the interface between the discrete and the continuous.
Bruce J. Nelson Professor, Computer Science
My research interests include recursion theory, automata
theory, complexity theory, algorithms, random number generation, cryptography,
and program result checking.
My current two projects are:
1. The
HumanOID (Human Oriented ID) project.
This is a cryptographic project to develop a challenge-response
authentication protocol that a human can do entirely in his head: The human must be able to authenticate himself
to a computer while a powerful adversary (one with a CRAY) -- who knows the
protocol, listens on the line, and records every challenge and response --
should be incapable of learning to impersonate the human.
Preston Tollinger has set up the 4th
floor lounge coke machine to give free cokes to anyone who authenticates
himself using the current prototype system.
This is to test the viability of the protocol for human use. Nick Hopper is working on proving the security of the system. Adam Kalai is working to break it.
2. The
Stable Circuit Problem. This is an algorithms problem that arose
(independently) in several contexts, including games, circuits, and logic
programming. Two graduate students,
Rachel Rue and Ke Yang, are working with me to solve it. A polynomial time algorithm would extend
linear programming to an interesting nontrivial substantially larger class of
problems.
Associate Professor, Computer Science
My main interests concern
the mathematical semantics of programming languages. I believe that proper
attention to semantic foundations can yield significant benefits in developing
techniques for proving properties of programs, in program design, in language
design and implementation.
I am particularly
interested in developing intensional semantic models, in which one is able to
reason both about the correctness and efficiency of programs. This is in
contrast to most traditional semantic models, which are extensional and focus
on the input-output behavior of programs while abstracting away from
computation strategy. I am working mainly on the semantic foundations of
parallelism. This work includes the development of axiomatic proof techniques
for establishing behavioral properties of parallel systems, design rules for
parallel networks that guarantee desirable behavior such as deadlock-freedom,
and the design and implementation of programming languages that employ
parallelism uniformly and cleanly.
A semantics for a
programming language is an assignment of meanings to program terms. For a
semantics to be useful it should accurately capture the computational behavior
of program terms, at an appropriate level of abstraction.
I believe that major
improvements in the formal treatment of program properties can be achieved by
paying careful attention to semantics. If we want to reason about a particular
behavioral notion (such as partial correctness) we should first define a
mathematical model for programs which precisely captures this behavior without
being overly complicated. Ideally, we would like a fully abstract semantics:
terms should be given the same meaning precisely when the terms would induce
identical behavior in all program contexts. The construction of fully abstract
models is by no means an easy task, and depends in any case on the underlying
notion of behavior.
For modelling and
reasoning about certain types of program behavior, such as partial or total
correctness, an extensional semantics is satisfactory: the meaning of a program
can be chosen to be a (partial) function from initial states to final states,
and all details of how the program goes about its computation can be suppressed
since all we really need to keep track of is the state transformation that the
program induces. However, such a semantics is no use if we want to make
comparisons between programs for the same function. In an extensional semantics
all sorting programs have the same meaning, whereas we might well want to
design a semantics with which we can compare sorting programs with different
computation strategies. This motivation leads to a desire for a theory of
intensional semantics. In an intensional semantics the meaning of a program is
taken to be an algorithm rather than simply a function. An algorithm can be
viewed as a function together with a (mathematical representation of a)
computation strategy. I have recently developed a category-theoretic approach
to the modelling of algorithms, and applied these ideas to the semantics of the
lambda calculus. In the resulting semantic model, there is a complete partial
order on algorithms and standard operations such as composition, application,
and currying are continuous; thus, one may define algorithms recursively and
use the standard techniques of denotational semantics (least fixed points) to
reason about recursive programs, even at this intensional level. This approach
using categories is rather general, and I am exploring several other possible
applications.
Semantic principles and
insights should be used in the design of new programming languages, to avoid
the development of cumbersome languages in which the programmer may have to
labor to overcome the syntactic quirks and idiosyncrasies of the programming
language in order to express his algorithm as a program. I am particularly
interested in designing a language that embodies parallelism uniformly: it
ought to be as easy to specify parallel expression evaluation as it is to
specify parallel execution of statements, and it ought to be easy to put
together the results of parallel activities. The choice of an appropriate set
of primitives for such a language should be guided by proper attention to
semantic foundations, and I am carrying out research on this topic.
University Professor and Dean
My primary research
interest is in formally verifying hardware designs. This interest grew out of
earlier work in logic simulation and symbolic circuit analysis. Over the past
few years, we have made great progress in formal verification, to the point
where industrial hardware designers are making use of our ideas and tools.
These tools promise to eliminate the uncertainty that lingers even after
extensive evaluation by techniques such as simulation. The recent fiasco with
the defective floating point divider in the Intel Pentium has placed formal
verification at the forefront in digital hardware research. Industry is showing
great interest in our work. Much more research is required in formalizing and
generalizing our methodology, as well as in tool development.
During the course of
developing hardware verification tools, I have become quite interested in
symbolic representations and manipulation of discrete functions. Most tasks
performed by a symbolic manipulator require solving NP-hard problems, and hence
there are no known algorithms with good guaranteed performance. Instead, this
work seeks heuristic methods that give satisfactory performance in practice.
Our approach involves representing functions by directed acyclic graphs and
applying graph algorithms to perform operations on functions. The results of
our work in this area have spread beyond the original application. Our methods
are now being applied to such areas as, temporal logic model checking, logic
circuit optimization, automated theorem proving, and truth maintenance systems.
In
recent years, we have developed techniques that generalize from Boolean
functions, representing each bit of data as a separate function, to word-level
functions, representing an entire data word as a function. This has lead to a
hierarchical methodology for verifying arithmetic circuits such as multipliers
and dividers. In fact, Intel has already started using these methods on their
floating point units. I also maintain a longstanding interest in parallel
computing, particularly in efficient mappings of application programs onto
parallel machines. I am particularly interested in applications involve the
manipulation of sparse and dynamically changing data structures. Such
applications have historically performed poorly on parallel machines, but I
believe that the right combination of architecture, programming model, and
algorithms could lead to efficient solution techniques.
I am particularly
interested in developing techniques to formally verify pipelined
microprocessors. Each generation of microprocessor uses increasingly complex
mechanisms to maximize performance, but these mechanisms should not affect
program behavior. The challenge is to verify that the hardware implements the
sequential semantics of the instruction set definition despite the fact that
many instructions are executed in parallel. Since the complexity of a
microprocessor is in its control logic, we can model the data operations as
unintepreted functions operating on symbolic data. We have recently devised techniques
that can verify simple, superscalar processors. However, major research
breakthroughs are required to handle the complexity of advanced
microprocessors.
Professor, Mechanical Engineering,
Computer Science(c), and Biomedical Engineering(c)
Professor Cagan's research focuses on the early design
process. His interests span from computational tools and theories to product
development practice. His computational work on design conceptualization and
product layout emphasizes computational representation, generation, and
optimizing search of the design space. His premise is that computational tools
must support a design process modeled by lateral exploration, followed by a
focused investigation of one or more good designs. Based on this premise, much
of his work has concentrated on stochastic optimization algorithms as search
techniques, and various grammatical representations to model, generate, and
move within the design space. The result is a merging between artificial
intelligence and operations research, giving a unique approach to addressing
the conceptual design problem.
Professor Cagan's other area of focus is in user-centered design and new product development practice. He works closely with colleagues in industrial design, psychology, and business in creating new methods for product development that focus on the Fuzzy Front End of the product development process. In collaboration with Prof. Craig Vogel, of the School of Design, Dr. Cagan has been consultant to and conducted research with small and large companies and has conducted professional development seminars in Integrated New Product Development. They annually co-teach a state-of-the-art course in Integrated New Product Development at CMU, which has resulted in patented products. Through their consulting, research, and teaching they have identified a number of factors that contribute to successful products that redefine their markets and often transcend their original program goals to create new markets. Profs. Cagan and Vogel’s book, Creating Breakthrough Products, summarizes their findings in a form that will aid practitioners and managers in the product development process.
Allen Newell Professor,
Computer Science, Language Technologies
Director, Language Technologies Institute
My interests span several areas of Artificial Intelligence, Language Technologies and Machine Learning. In particular, my current research is focused on areas such as text mining (extraction, categorization, novelty detection) and in new theoretical frameworks such as a unified utility-based theory bridging information retrieval, summarization, free-text question-answering and related tasks. I also work on Machine Translation, both high-accuracy knowledge-based MT and machine learning for corpus-based MT (such as generalized example-based MT). My research style combines theory, experimentation and system building, as often such synergy proves superior to more uni-dimensional approaches, at least in my research areas. The following are my current projects; all represent collaborative efforts with graduate students, research staff, and/or faculty colleagues:
The TDT Project (Topic
Detection and Tracking) [with Brown, Jin, Yang]. Automated topic-tracking
and novel-event detection for textual, and audio news media, including
developing new classifiers trainable with very few positive instances of events
or topics to track. Novelty detection in news-streams is the primary
emphasis.
The INFOSPHERE
Project (Information Utility and Summarization) [With Goldstein, Lafferty,
Likhodedov]. Infosphere includes retrieval and query- and task-relevant text
summarization based on Maximal Marginal Relevance (MMR) extended to
multi-document, topical-cluster summaries. New directions involve generalizing
MMR into a maximum-expected-utility theory of information access.
The
JAVELIN Project (Free-Text Question Answering) [With Callan, Czuba,
Hiyakumoto, Nyberg, Veloso and others]. The objective is to answer questions
ranging from simple factual ones "What is the population of Ghana?"
to multi-cycle ones "Who is in competition with JDS-Uniphase?" (where
planning is required to first establish what the company produces, then
determine who else produces comparable products, etc.), to questions without
pin-point answers "What are the root causes of Middle East
instability?" Textual and web corpora are the sources of
information, and multiple methods need to be combined to address this
challenge, including: question analysis, information retrieval, extraction,
partial parsing, synthetic summarization, and more, all combined via a
utility-based planning architecture.
The NICE and AVENUE projects (Machine Translation for
Indigenous Languages) [With Brown, Lafferty, Lavie, Levin, Petersen,
Probst]. The objective is to produce viable MT for new minority languages (such
as Quechua, Inupiac, Mapudungun, Haitian Creole) where there may be little or
no previously-developed linguistics, and only small amounts of parallel or
comparable text. Methods include Generalized example-based MT, new
Max-Entropy Statistical MT, and symbolic transfer-rule acquisition via Seeded
Version Space learning.
The MUCHMORE Project (Translingual Information Retrieval
[with Brown, Frederking, Rogati, Yang]. MUCHMORE focuses on developing multiple
methods for bridging the language barrier between queries and document
collections in IR, including example-based thesauri, translingual pseudo-relevance
feedback, generalized vector spaces, latent semantic indexing, and shared
interlingual ontologies (such as MeSH and UMLS in the biomedical domain). This
project partners with Stanford University, DFKI-Saarbrueken, Eurospider, Xerox
Grenoble and the University of Frankfurt.
The KANT Project (High-accuracy knowledge-based MT)
[with Mitamura, Nyberg]. Unlike other my other text-based projects that are
primarily corpus-based and domain independent, KANT is a knowledge-intensive
project to optimize translation accuracy conditioned on large but semantically
delineated domains of direct interest to industry. The primary method explored
is full parsing and semantic disambiguation into an extensive interlingua,
followed by generation into multiple target languages.
Senior Systems Scientist,
Computer Science, Human Computer
Interaction
My interests are in multimedia
interface development and evaluation, digital
video libraries, and computer support for
situated learning. My current work as part of the Informedia Digital Video
Library leverages from other CMU CS research in image processing, natural
language processing, and speech recognition to enable full content search and
retrieval from digital video, audio and text libraries.
Given thousands of hours of
video and the need to find a relevant ten minute clip, a user should be able to
locate the relevant clip without investing hours of viewing time. I contribute
to the development of segmentation and abstraction strategies to meet this goal
of more efficient information retrieval from multimedia libraries. I also
conduct empirical studies evaluating the effects of multimedia abstractions
such as thumbnail images, storyboards, and video skims.
A user might also find relevant material scattered across portions of
many video clips in the library rather than concentrated in any single
clip. I am interested in improving browsing and navigation within digital
video libraries by supplementing the current query interface with information
visualization techniques, and extending the user pool for the Informedia
library by fielding Web-based interfaces compliant with the latest World Wide
Web Consortium recommendations. Through visualization interfaces, users will
be able to explore meaningful, manipulable overviews of large video document
sets, issue true multimodal queries, and be aided by automatic, adaptive
summarizations of vast amounts of video.
FORE Systems Professor,
Computer Science, Electrical and Computer Engineering(c)
My interests span three areas: Programming Systems, Hardware, and Theory. I use the techniques and insights of theoretical computer science to solve problems in programming systems and hardware design that are of practical interest. I have a number of active research projects in these areas that I would be happy to discuss with students. Below are short descriptions of two research projects that I think are particularly exciting.
Hardware and Software Verification. Logical errors in finite state concurrent systems like sequential circuits and communication protocols are an important problem for computer scientists. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. The most widely used verification method is based on extensive simulation and can easily miss significant errors when the number possible states of the system is very large. Although there has been considerable research on the use of theorem provers, term rewriting systems and proof checkers for verification, these techniques are time consuming and often require a great deal of manual intervention. My group has developed an alternative approach called temporal logic model checking in which specifications are expressed in a propositional temporal logic and an efficient search procedure is used to determine whether or not the specifications are satisfied.
In the twenty-three years that have passed since the original algorithm was published, the size of the systems that can be verified by this means has increased dramatically. By developing special programming languages for describing transition systems, it became possible to check examples with several thousand states. This was sufficient to find subtle errors in a number of nontrivial, although relatively small, circuit and protocols designs. Use of boolean decision diagrams (BDDs) led to a major increase in the size of the examples we could handle by this technique. Representing transition relations implicitly using BDDs made it possible to verify examples that would have required 1020 states with the original version algorithm. Refinements of the BDD-based techniques have pushed the state count up over 10100 states. By combining model checking with abstraction, we have been able to check even larger examples. In one case, we were able to verify a pipelined ALU design with 64 registers, each 64 bits wide, and more than 101300 reachable states.
Analytica --- A Theorem Prover for Mathematica. Analytica is an automatic theorem prover for theorems in elementary analysis. The prover runs in the Mathematica environment and is written in Mathematica language. The goal of the project is to use a powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic theorem provers. The theorem prover is also able to guarantee the correctness of certain steps that are made by the symbolic computation system and therefore prevent common errors like division by a expression that could be zero.
Since we wanted to generate proofs that were as similar as possible to proofs constructed by humans, we use a variant of natural deduction to generate proofs. We have demonstrated the power of our theorem prover on several non-trivial examples including the basic properties of the stereographic projection and a series of three lemmas that lead to a proof of Weierstrass's example of a continuous nowhere differentiable function. Each of the lemmas in the latter example is proved completely automatically. In a related project that uses similar techniques, we have managed to prove all of the theorems and examples in Chapter 2 of Ramanujan's Collected Works completely automatically. We believe these examples provide convincing justification for combining powerful symbolic computation techniques with theorem provers.
Senior Systems Scientist, Computer Science
I am interested in image understanding and computer vision systems, especially in the area of binocular stereo from passively-acquired imagery. I am currently working with Dave McKeown, Chris McGlone and Jefferey Shufelt at the Digital Mapping Laboratory in the investigation of the automated analysis of aerial imagery to support research in computer vision for digital mapping and the creation of databases for virtual world simulation.
Binocular Stereo. Humans are able to surmise depth in 2-D "monocular" images and to perceive it through the stereoscopic fusion of a pair of images. The process used by the human visual system to achieve this, however, is not well understood. How, then can we produce autonomous systems which are able to extract depth information about, and interact with, their environments? One way is to attempt to emulate some of those processes, which seem to be present in the human visual system, and learn what does and does not work. This approach allows us to attempt automatic visual recognition of objects, and, perhaps in some cases, to gain insight about the operation of the human visual system. The perception of depth from a stereo pair provides both a qualitative and a quantitative measure in depth determination that is not available from a monocular view and produces the ability to detect objects which are difficult to distinguish from the background due to similar image intensities or textures. For my theses work at USC, I developed a Stereo Vision System (SVS) in which I showed methods to integrate primitives derived from area-based and feature-based stereo matching algorithms. I have continued this work at CMU particularly with respect to improvements in stereo matching accuracy and refinement.
Data Fusion. Stereo data alone is not sufficient to solve the cartographic feature extraction problem. To achieve that goal, we will need to gather together various partial scene abstractions formed by differing methods: stereo, monocular, multi-spectral and others. Relating image derived measurements and features into a consistent and rigorous object-space representation is an important first step in automated fusion. As an example, four aerial images that cover a common area allow twelve different sets of pairwise stereo data to be produced, along with four sets of monocular estimates of building hypotheses. The key issue is finding common robust structure from this noisy and diverse set of information.
Evaluation. It is not enough to simply point at a set of results and saying Look! I am doing a great job. It is necessary to determine quantitatively, as well as qualitatively, how well an approach is working in order to justify claims of an improvement to that approach. At the same time it is difficult and/or expensive to obtain or generate a complete ground-truth model of a test scene. Therefore I have been working on ways to generate quantitative results with respect to a set of goals. For instance, if the goal is to extract all of the buildings in the scene, then only the buildings need to be explicitly modeled in the ground reference data.
Assistant Professor, Computer Science
My research interests are in the design and implementation of advanced programming languages and in applying programming language technology to improve the development, maintenance, and performance of software systems. I am particularly interested in the application of types to the structure and implementation of programming languages.
A current focus of my research is on typed compilation. Compilation using types offers some compelling benefits over conventional, untyped compilation. For example, preserving types through compilation provides additional information that may be used to optimize programs. Type-based optimizations are particularly useful for compiling advanced programming languages, such as ML. Advanced programming languages provide many features such as first-class functions, automatic memory management, polymorphism and abstraction, that are valuable to programmers but are also hard to implement efficiently. Modern implementation strategies, including type-based optimization, allow advanced languages to be implemented roughly as efficiently as less advanced ones. For instance, the TIL (Typed Intermediate Languages) compiler for ML, one project I work on, uses type-based optimizations to obtain a 3-fold speedup over other ML compilers.
An even more important benefit of typed compilation lies in its application to mobile code security. With the increasing importance of the widely distributed computing (particularly with the World Wide Web), it has become impractical for agents to limit their computing interactions to other agents whom they trust. This leads directly to a need for mechanisms whereby an agent can safely execute untrusted and potentially malicious programs. However, it is important that such mechanisms not substantially sacrifice performance, as is the case with run-time checking mechanisms. Typed compilation gives us a tool for producing certified executables, which can be statically determined to be safe before execution. This certification strategy works by attaching types to mobile code; that code is then type-checked and is run only if type-checking succeeds. If it does succeed, the formal semantics of the type system guarantees that code is safe.
For this to work requires a type system suitable for low-level code, in particular for machine binaries. However, most research into type systems has focused on high-level languages, in part because low-level languages can be uncooperative to type-theoretic analysis. Recently, I and others have been studying typed assembly languages, machine-level programming languages with sound type systems. In a typed assembly language, one can program with direct access to machine resources without sacrificing the safety guarantees provided by typed high-level languages. In practice, however, typed assembly code is typically produces by a typed compiler from high-level source code. My ongoing research into typed assembly languages focuses on enhancing their type systems both to make them more flexible and to strengthen the safety properties they can guarantee.
Associate Research Professor, Computer Science and Art (c)
My work is focused on various aspects of computer music, a field which poses many challenges for computer science. I also direct the Just-In-Time Lecture Consortium, which offers a new technology for low-cost, computer-based training and education.
A central problem in computer music is expressive control, that is, the detailed control of timing, gesture, nuance, and tone quality that is essential to music. This problem has many facets, resulting in a variety of research directions. The Computer Music Project has developed new languages, development tools for real-time systems, synthesis techniques, and music understanding systems. This research is more than intrinsically interesting. It can shed light on related problems in real-time systems, multimedia, human-computer interaction, and artificial intelligence. Moreover, new possibilities of control and interaction in music are changing the very nature of music composition, performance, and aesthetics.
One research example is the development of new languages for expressing temporal behavior. One of these is Nyquist, a language that provides a single abstraction mechanism for the seemingly different notions of "note," "instrument," and "musical score." Nyquist gives composers an elegant, uniform notation that spans the range from low-level digital signal processing to high-level music composition. Nyquist is not intended for interactive real-time sound generation, but concepts from Nyquist are incorporated in other systems, including one of our own named Aura.
Expressive control of musical tones is another topic of research. A violin is expressive because there are many parameters under continuous control by the player, including bow pressure, finger and bow positions, and bow velocity. These give rise to variations in the resulting sound. My colleagues and I have developed a new synthesis technique, spectral interpolation, which allows us to synthesize tones with interesting variations in spectra. Spectral interpolation has been used to accurately synthesize a variety of instruments. In the future, we will use this technique to give composers and performers greater intuitive control over synthesized sound.
Real-time performance systems present interesting problems. I have developed several systems for real-time music understanding that "listen" to a live performance and derive some abstract information regarding rhythm, tempo, harmony, etc. The degree of understanding is usually demonstrated by having the system participate in the performance. One example is Computer Accompaniment, in which the computer follows a performance in a score and plays an accompaniment in synchronization with the performer. My computer accompaniment technology appeared in a commercial product in 1994. Other examples include a system that listens to an improviser playing 12-bar blues and plays the part of a rhythm section, and a system for classifying improvisational styles. This is only the beginning of what is possible. Current work includes more sophisticated systems for listening to improvisations, ensembles, and vocalists.
Education is another interest. Our country spends more for education than for health care, and as with health care, education costs are growing faster than the inflation rate. Computer-based tutoring systems have much to offer, but development costs and lack of expertise have made it difficult to produce good tutoring systems. Work on automating instructional design principles to lower the cost of intelligent tutoring systems led to an even simpler approach, "Just-In-Time Lectures," in which presentations are captured using digital video, synchronized slides, a table-of-contents, and links to the Web. Just-In-Time Lectures have been used to deliver entire courses and by large corporations for training.
Associate Professor, Biological Sciences, Computer Science(c)
Computational analysis of molecular sequence data is a key component in solving three critical biological problems of the 21st century: how genes interact to produce living cells, how gene malfunction causes disease and how complex, multicellular organisms evolved from simple, unicellular organisms. The late 20th century revolution in DNA sequencing technology has produced an exponentially growing wealth of data that can be used to answer these and similar questions. The World Wide Web has made it possible to integrate data from diverse, distant sources and make it universally available. The field of computational molecular biology was born at the confluence of these two revolutions.
In my research in computational molecular biology, I study the role of gene duplication in the acquisition of new gene function and the evolution of vertebrate genomes. (A genome is the complete set of genes in an organism.) New genes arise through gene duplications, errors during cell division that result in extra copies of genes. These extra copies subsequently mutate to take on new functional roles in the cell. The duplication of large regions, ranging from chromosomal segments to the entire genome, is believed to have played a crucial role in early vertebrate evolution. According to the hypothesis, the new genes that resulted from these massive duplications are responsible for the evolution of innovations, such as skeletal structure, limbs, and a complex central nervous system, that distinguish vertebrates from other life forms. If we can understand how these genes acquired new function following duplication, we will have a better understanding of how we evolved and the role those genes play in vertebrates living today.
This project contains a number of interesting open problems in both information retrieval and algorithms. In order to understand the evolution of new function in duplicated genes, sequence data must be combined with other types of biological data leading to problems in web-based data management and retrieval, including data mining, analysis and visualization of large biological datasets that are diverse, distributed and noisy. Algorithmic and combinatorial problems arise in reconstructing the history of genomic duplications and rearrangements that led to the modern genome. For example, while individual duplicate genes can be found using algorithms based on approximate string matching, the problems of identifying entire sets of genes that were duplicated simultaneously and estimating the age of these large-scale duplications remain open.
I welcome discussions with computer science students and computer scientists who are interested in either the algorithmic or the information retrieval aspects of computational molecular biology.
MICHAEL ERDMANN
Professor, Computer Science, Robotics
I am interested in Robotics and in Computational Molecular Biology, with shape sensing as a unifying theme. My research draws on tools from geometry, mechanics, and stochastic processes.
On the robotics side, I wish to make robots act purposefully and successfully despite the inevitability of noisy sensors, imprecise actions, and mistaken world models. I have worked on grasping strategies, friction representations, and automatic planning to overcome uncertainty. Recently, I created a two-palm robot. The robot consisted of two manipulator arms cooperating to manipulate objects without the need for full kinematic constraint. The arms "programmed themselves", that is, they invoked an automatic planner to find sequences of motions for reorienting objects in their palms. The planner built a geometric graph based on a critical event analysis of the underlying mechanics.
At present, my students and I are developing sensing strategies to acquire the shape of unknown objects concurrently during manipulation. Amazingly, it is possible for a robot to determine the shape of an unknown object from tactile information without requiring that the object be held firmly; the object may slip and slide in the hands. Such strategies are useful for robots manipulating novel objects in unstructured environments. One application we are considering is desktop robotics.
On the molecular side, I am interested in protein shape and motion. Currently I am collaborating with researchers in the Department of Biological Sciences to determine protein homology from sparse NMR data. Our approach draws heavily on techniques from Computational Geometry.
Research Professor, Computer Science
I am interested in artificial intelligence and its application to real-world problems.. Over the years, I have worked in many areas of AI, including knowledge representation, problem solving, image processing, machine learning, massively parallel approaches to search and inference, and the development of improved learning algorithms for artificial neural networks.
I am currently one of the leaders of CMU;s Radar Project, a DARPA-funded effort to build a software "cognitive assistant" for busy managers. Radar uses advanced AI and machine-learning techniques to help its human master organize mail, produce reports, schedule meetings, and allocate scarce resources. My particular focus within the project is the Scone knowledge base, which is used by all parts of the Radar system.
I have also worked on programming
languages and software development
environments that support an incremental, evolutionary style of software development. This work has been done in Common Lisp,
Dylan, and Java..
Professor, Computer Science
The
major focus is on data bases and data mining. There are three major research
areas: Multimedia, sensor, and graph data mining.
The first area
focuses on the discovery of correlations across several media, like video, with
frames, motion, text annotations. The goal is to summarize video clips, to
attach text annotations to video or still images, to do segmentation.
The second area
focuses on the discovery of patterns, given a large collection of sensor
measurements, like temperature, humitidy, and illumination readings. The goal
is to find outliers, periodicities, lag-correlations, without human
intervention, on semi-infinite streams of data. Typical problems are
forecasting, interpolation, segmentation, as well as “which two sensors are
strongly correlated, possibly with a lag”.
The last area is on
finding patterns and outliers in large graphs, like social networks, computer
networks, metabolic networks in biology. For example, “who is the most
influential person” in a social network; “which routers have suspicious
connectivity patterns”; “how quickly will a virus propagate in a given computer
network”.
We use power laws,
Singular Value Decomposition, to help us detect patterns and outliers, as well
as concepts from fractals and self-similarity.
BABAK FALSAFI
Assistant Professor,
Electrical and Computer Engineering, Computer Science(c)
My research focuses on design, evaluation, and implementation of computer systems with emphasis on processor and memory architecture/microarchitecture.
Prediction/speculation in high-performance memory system. Technological advancements in semiconductor fabrication together with architectural innovation are resulting in phenomenal increases in processor performance. While memory capacity has commensurately increased, memory speeds have primarily lagged behind processor speeds. We propose Proactive Memory, memory systems that "proactively" move and place data among the hierarchy levels in both uniprocessors and multiprocessors in anticipation of a processor memory access, to hide the long memory latency. The key mechanisms enabling proactive memory are memory predictors that monitor program execution, capture processor memory access patterns, and accurately predict subsequent processor memory accesses.
Power-aware computer systems. The unabated growth in the number of transistors is resulting in a proportional increase in the chip's power dissipation. Higher power dissipation increases cost and reduces the reliability of computer products in all market segments, and significantly reduces the usability of portable systems by diminishing the battery life. We propose and investigate power-aware architectures in which software/hardware minimize power dissipation while maintaining high performance. The key observation behind our designs is that the demand for hardware resources widely varies both within and across applications. Our systems use mechanisms both at software/architecture and circuit level to dynamically identify and enable an application's required processor/memory resources, thereby eliminating power dissipation in unused resources.
Single-chip multiprocessor/multithreaded architecture. The diminishing degrees of instruction-level parallelism (ILP) and the hardware complexity of extracting ILP in large-window wide-issue superscalar processors are leading architects to innovate threaded architectures. Current proposals for threaded architectures, however, either rely entirely on programmer/compiler to generate threads, or extract "speculative" threads in hardware, requiring sophisticated and high-overhead mechanisms to track dependences among threads. Our research investigates novel threaded architectures that use an integrated software/hardware approach to reducing speculation overhead. Our architectures can be mapped to both centralized (SMT-like) and distributed (CMP-like) chip organizations.
Eugene Fink
Systems Scientist
Computer Science, Language Technologies Institute
My research interests are in various aspects of artificial intelligence,
including machine learning, planning, problem solving, automated problem
reformulation, e-commerce applications, medical applications, and theoretical
foundations of artificial intelligence. My interests also include computational
geometry and algorithm theory.
I am currently working on an intelligent system for automated allocation
of offices and related resources, in both crisis and routine situations. This
work is part of the Radar project, aimed at creating an automated
general-purpose assistant for office managers.
I am also working on techniques for identification of both known and
surprising patterns in large-scale databases, and applying these techniques to
homeland security. This work is part of the Argus project, which is joint
research involving
Associate Professor,
Electrical and Computer Engineering, Computer Science(c)
I have broad research interests in computer systems, including operating systems, storage/file systems, security, networking, distributed systems. I am particularly interested in developing new ways of structuring computer systems to address technology changes and enable new applications. My group has many ongoing projects in such areas as self-* (managing, tuning, ...) systems, device-embedded functionality, and computer infrastructure security.
Parallel Data Lab (PDL).
As Director of the Parallel Data Lab (http://www.pdl.cs.cmu.edu/),
I lead a number of storage-related projects in areas such as storage system
architecture, storage security, file systems, disk characterization, and server
implementation. As one example, we are exploring how new storage
technologies like MEMS-based storage could best be incorporated into computer
systems. As another, we are exploring the use of detailed disk knowledge
in the design of file systems and databases.
Jiang Gao
Systems Scientist, Computer Science
My research interests lie primarily in the area of computer vision and
robotics, with special focus on understanding an environment of human,
including activities, faces and written symbols. The progress in this area will
impact our daily lives in a profound way. Some research directions and projects
include:
HumanID and Caremedia projects. We are developing a system
for activity analysis from video cameras in a nursing home, based on robust
motion features and a hidden Markov model. The focus is on event understanding
and knowledge mining from video.
Interpretation of written symbols. Developed a fully
automatic, real time system for detection, recognition, and translation of text
/signs from a natural environment. I am also interested in natural language
processing (NLP) and machine translation through this work. Some part of this
work was performed in Interactive Systems Labs, Human Computer Interaction
Institute.
Face expression analysis. My work is focused on
generic 3D face modeling from video and rigid head motion stabilization for
face expression analysis.
These works play a central role in a variety of applications, including
human-computer interaction, intelligent systems / interfaces, and medical
applications. Besides, I am also interested in statistics, estimation,
operational research, and control engineering, through my previous research
experience.
Professor,
Institute for Software Research, International, Computer Science
My field of interest is software engineering, and specifically the areas of software architecture, self-healing systems, pervasive and cognitive computing, and applied formal methods. The common thread that links these areas is the problem of controlling the complexity of large software systems by providing a scientific basis for software design.
Software Architecture. Successful design of software architecture has always been a major factor in determining the success of a software system. But until recently architectural design has been largely based on ad hoc choice, informal experience, and local expertise. The goal of this research component is make this knowledge precise, codified, and available to engineers as a matter of routine engineering. My research group has developed a number of languages and tools to support architectural design, including Wright (a formal language for software architectures that focuses on specification and analysis of component interactions) and Acme (a language and design environment for software architecture, supporting rapid customization to architectural styles).
Self-healing Systems. Increasingly systems must continue to operate continuously, interacting with diverse external services not under the control of the system designer. A new paradigm is emerging to handle such systems: each system takes responsibility for observing its own behavior, and for improving that behavior over time based on models of what behavior is desirable. My research group is using architectural models to do this. Thus architectural designs become run-time artifacts that permit system self-reflection and repair.
Pervasive and Cognitive Computing. The most precious resource in a computer system is no longer its processor, memory, disk or network, but rather user attention. Today's systems distract a user in many explicit and implicit ways, reducing effectiveness. Projects Aura and Radar, with which I am working, are rethinking system design to address this problem. Aura's goal is to provide each user with an invisible halo of computing and information services that persists regardless of location. Project Radar is developing a basis for creating cognitive assistants that actively assist users in meeting their needs, such as scheduling a meeting, allocating space resources, or generating annual reports. Within these two projects, my principal interest is developing support for managing a users task load. Specifically, I am creating infrastructure that permits a user to move from one physical environment to another, and continue working on the same tasks, even though the underlying resources may change radically. I am also working on coordinating tasks for a single user or across multiple users.
Applied Formal Methods. The traditional use of formal (or mathematically-based) methods has been to solve the problem of refinement: given a formal specification of a system, how does one construct an implementation that is correct with respect to that specification. In contrast, my interest in formal methods is in dealing with the inverse problem of abstraction: given a family of existing systems, how does one construct a formal model that characterizes the important commonalities in these systems. When used in this way, formal methods become a tool for extracting reusable software architectures, for clarifying system design, for simplifying the way we think about a class of system, and for building a framework for reuse.
The ABLE Project: www.cs.cmu.edu/~able
Project Aura: www.cs.cmu.edu/~aura
The Radar Project: www.cs.cmu.edu/~radar
The Software Verification Center: www.cs.cmu.edu/~svc
Associate Professor,
Computer Science, Electrical and Computer Engineering (c)
My research goal is to develop novel architectures and compilers which will reduce the cost of processors while increasing their performance (operations per second-watt-liter). We are examining how to effectively harness deep-submicron VLSI and electronic nanotechnology to construct architectures which are inexpensive and easy to manufacture and can scale to devices with billions of transistors.
Electronic Nanotechnology. Although we have come to expect, and plan for, the exponential increase in processing power in our everyday lives, today Moore's Law faces imminent challenges both from the physics of deep-submicron CMOS devices and from the enormous costs of next-generation fabrication plants and mask sets. A promising alternative to CMOS-based computing is electronic nanotechnology, which constructs electronic circuits out of nanometer-scale devices that take advantage of quantum-mechanical effects. Our fundamental strategy is to substitute compilation time (which is inexpensive) for manufacturing precision (which is expensive).
Using electronic nanotechnology to build computer systems will require new ways of thinking about computer architecture and compilation. Unlike conventional CMOS, it cannot be used to fabricate construct heterogeneous structures. Instead, one fabricates dense regular (but potentially defective) structures that can be programmed after fabrication to implement complex circuits. We are investigating new circuit families and architectures based on the anticipated manufacturing primitives available for nanoscale devices. We expect the manufacturing process to create devices with defects and are developing diagnostic and compilation methods that can target defective chips with little or no loss in performance. For more information consult NanoFabrics: Spatial Computing Using Molecular Electronics.
Reconfigurable Computing. Reconfigurable computing is a general term that applies to any device which can be configured, at run-time, to implement a function as a hardware circuit. A reconfigurable device has sufficient logic and routing resources that it can be configured, or programmed, to compute a large set of functions in space. Later, it can be re-programmed to perform a different set of functions. It shares attributes of microprocessors, in that it can be programmed post-fabrication, and of custom hardware, in that it can implement a circuit directly. Our investigations are focused on compiler technology and architectures for reconfigurable computing. The architectures are all highly regular and thus can tolerate defects making deep-submicron and electronic nanotechnology manufacture more efficient. Our first architecture, PipeRench, overcomes most of the problems of commercial reconfigurable devices. Our backend compiler is more than two orders of magnitude faster than commercial CAD tools, allowing it to scale to larger devices. Our short-term goal is to bring reconfigurable computing into the mainstream by developing the architectures and compilers necessary to integrate a reconfigurable fabric with a processor core for both high-powered, general-purpose processors and embedded systems.
Assistant Professor,
Center for Automated
Learning and Discovery
C