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.
LENORE BLUM
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.
MANUEL BLUM
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.
STEPHEN BROOKES
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.
RANDAL E. BRYANT
President's Professor,
Computer Science and Electrical and Computer Engineering(C)
Department Head, Computer Science
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.
JONATHAN CAGAN
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.
JAIME CARBONELL
Allen Newell Professor,
Computer Science and 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.
MIKE CHRISTEL
Senior Systems Scientist,
Computer Science and 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.
EDMUND M. CLARKE
FORE Systems Professor,
Computer Science and 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 fifteen 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.
STEVEN DOUGLAS COCHRAN
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.
ALBERT
CORBETT
Research Scientist, Human Computer Interaction
My interests are in the
application of artificial intelligence to education, in particular, the use of
cognitive models in computer-based tutoring environments. Our approach is to
build tutoring programs around rule-based models of how people perform skills,
such as programming. Such a model allows the tutoring program to solve practice
exercises along with the student, providing help as needed. My research has
focused recently on estimating students' mastery of the knowledge represented
in the cognitive model. By integrating learning and performance assumptions
with the cognitive rules, we attempt to predict students' test performance,
shape practice appropriately and improve the model. I am also interested in
related issues in the design of computer-based practice environments, for
example the content and timing of help messages and their impact on students'
performance.
KARL CRARY
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.
ROGER DANNENBERG
Senior Research Scientist, Computer Science
Senior Research Artist, Art(c)
Fellow, Studio for Creative Inquiry, College of Fine Arts(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.
DANNIE DURAND
Associate Professor, Biological Sciences and 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
Associate Professor, Computer Science and 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.
SCOTT FAHLMAN
Principal Research Scientist, 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 problem solving, image processing, machine learning, knowledge
representation, massively parallel approaches to search and inference, and the
development of improved learning algorithms for artificial neural networks.
I have also worked on developing 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.
At present my primary research goal is to develop an efficient
and flexible system for representing large amounts of real-world, common-sense
knowledge. In my Ph.D. thesis, I
described how a massively parallel machine could be used to achieve this
end. Today, machines are much faster
and memories are much larger. We should
now be able to build a respectable knowledge base on a standard high-end
workstation. In addition to its value
for AI, I believe that such a knowledge-base system would find many uses in
industry.
CHRISTOS
FALOUTSOS
Professor, Computer Science
The research focus is on
Databases and specifically, on fast searching methods for multimedia and
medical-image databases, on data mining and on performance issues for large
datasets.
The first project examines
fast methods for approximate matching in multimedia databases. Typical queries
are as follows: "in a collection of product photographs, find products
that look like tennis shoes"; "in a collection of medical X-rays,
find ones that look like the X-ray of the current patient, and list the
corresponding diagnoses". The main idea behind our approach is to extract n features from the objects of interest
(typically, with the help of a domain expert), thus mapping each object into a
point in n-dimensional feature space.
Subsequently, we can use state-of-the-art database techniques (like the
'R-trees') to store and retrieve these n-dimensional
points. The philosophy of our approach is to provide a the vast majority of
irrelevant objects. Allowing some 'false alarms' is accept- able, because they
can be easily discarded by a elaborate test, or even by the user. We have
already successful sets of features for 2-d color images, 2-d shapes, and 1-d
time series (such as stock-price movements). Depending on the domain, we are
experimenting with modern signal processing techniques, such as the discrete
wavelet transform for sound and images, hidden Markov chains for digitized
voice, the discrete cosine transform for stock-price time series.
The second project focuses
on data mining. The goal is to discover correlations ('rules') in a collection
of records. For example, in a set of patient records with demographic
characteristics, symp- toms and diagnoses, we would like to find all the
'interesting' rules (eg., 'patients 50 years old with cholesterol 300 have 10%
probability of heart attack'). We are studying traditional clustering methods
as well as statistical methods like the 'Singular Value Decomposition' (SVD),
to do cluster analysis and rule discovery.
The last project examines
algorithms and architectures for fast execution of expensive database
operations. We are working on Active Disks for data mining, on striping and
placement algorithms for video servers, and on buffering algorithms for
database operations.
BABAK FALSAFI
Assistant Professor,
Electrical and Computer Engineering and 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.
GREG GANGER
Associate Professor,
Electrical and Computer Engineering and Computer Science(c)
I have broad research interests in computer systems, including
operating systems, security,
storage/file systems, networking, and 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 device-embedded functionality, storage/file
system design, and computer infrastructure security.
Device-Embedded Security. We are exploring a new
approach to computer security in which each individual device erects its own
security perimeter and defends its own critical resources. Together with
conventional border defenses (e.g., firewalls and OS kernels), such self-securing
devices could provide a flexible infrastructure for dynamic prevention,
detection, diagnosis, isolation, and repair of successful breaches in borders
and device security perimeters.
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.
DAVID GARLAN
Associate Professor, Computer Science
My field of interest is software engineering, and specifically
the areas of software architecture, pervasive 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. Towards this goal 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), Aesop (a design
environment for software architecture, supporting rapid customization to
architectural styles), and Acme (a language for interchange of architectural
designs).
Pervasive Computing. The most precious resource in a computer
system is no longer its processor, memory, disk or network. Rather, it is a
resource not subject to Moore's law: user attention. Today's systems distract a
user in many explicit and implicit ways, thereby reducing his effectiveness.
Project Aura, on which I am a Principal Investigator, is fundamentally
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. Meeting this goal will require effort at every
level: from the hardware and network layers, through the operating system and
middleware, to the user interface and applications. Within this project, my principal
interest is developing support for managing a users task load. Specifically, I
am developing 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.
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. Among
the important research issues are those of methodology (How should we use
formal notations in practice to arrive at system abstractions?), language (What
notations, type systems, parameterization mechanisms, etc. are best suited to
this use of formal methods?), and reusability (What properties of a formal
model best support reusability, evolution, and adaptation?).
GARTH GIBSON
Associate Professor, Computer Science
and Electrical and Computer Engineering(c)
(On leave of absence 2000-2003)
My research is centered on parallelism in secondary storage
system technologies, especially parallel and distributed file systems, disk
arrays, and network-attached storage devices.
I work with multiple projects in the Parallel
Data Lab, a community of a few dozen storage researchers including faculty,
PhD students, masters students and professional programmers. The Lab is supported by government and
industrial sponsors with guidance from an industrial consortium including HP,
Sun, Intel, Veritas, Seagate, Quantum, 3Com, LSI Logic and EMC.
SETH
COPEN GOLDSTEIN
Assistant Professor, Computer Science
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.
MOR
HARCHOL-BALTER
Assistant Professor,
Computer Science
I am interested in the
performance analysis and design of computer systems, particularly distributed
systems. I work on finding analytical models which capture the important
characteristics of a computer system and allow me to redesign the system to
improve its performance.
I believe that many
fundamental conventional wisdoms on which we base system designs are not well
understood and sometimes false, leading to inferior designs. My research
challenges these age-old beliefs. Here are just a few examples:
·
Thousands of "load balancing" heuristics do
exactly that -- they aim to balance the load among the existing hosts. But who
said that's neccessarily a good thing?
·
Migration policies for networks of workstations and
distributed servers direct jobs to the host with least load. That seems good
from the job's perspective, but is it best for the system overall?
·
Given a choice between a single machine with power p ,
or n identical machines each with power p/n, which would you choose?
·
Migrating active jobs is generally considered too
expensive. Killing jobs midway through execution and restarting them from
scratch later is even worse! Says who?
·
Ever notice that the "proven best" scheduling
policies like SRPT (shortest-remaining-processing-time-first) are never used in
practice? There's a fear that the big jobs will starve. Is this true?
Application areas I currently work
in include: Web servers, distributed Web servers, distributed supercomputing
servers, networks of workstations, and communication networks.
ROBERT HARPER
Professor, Computer Science
My principal research interest is in the application of type
theory to building and reasoning about programs. The focus of my work
is the ConCert Project, which is led by Karl Crary, Peter Lee, Frank
Pfenning, and me. The ConCert Project
is concerned with developing the theoretical and practical foundations of
trust-free grid computing. The overall goal is to minimize trust
relationships that must hold between host owners and application developers
in grid computing. Our primary methodology is to investigate the use
of techniques from logic and type theory to support policy-based certification
techniques that allow mutually suspicious parties to verify mechanically the
integrity of application code and computed results. Frank Pfenning and
I lead a research project on refinement types, which seek to extend
the power of programming language type systems to capture a richer class of
invariants without sacrificing the ease of use afforded by current type systems.
I also participate in the Twelf Project on the theory and practice of logical
frameworks, and in the Aladdin project on the applications of theory to
practical computing.
All of my research centers on the application of type
theory to practical programming problems. Type theory provides a
unifying conceptual framework for programming language design, specification,
and implementation. As a design tool
type theory provides a clean framework for organizing programming language
constructs. A type consists of a collection of values together with a
collection of primitive operations on those values. Familiar notions such as trees or lists may be viewed as values
of recursive type; the operations
permit traversal of these structures. Procedures may be viewed as values
of function type, with operations to create procedures and to apply them to
arguments. Abstract data structures such as dictionaries may be seen as
values of existential type, with operations to create a data structure and to use
a data structure without revealing its implementation details. In fact a
programming language may be defined by giving an interpretation of its
constructs in type theory. For example, modularity mechanisms might be
rendered as uses of existential type, together with a notion of subtyping to
admit code reuse and generic operations. A significant advantage of the
type-theoretic viewpoint is that it has direct implications for compiler
writers. My work on the TILT compiler demonstrates the importance of typed
intermediate languages for building compilers that generate efficient
machine code. The stages of the TILT compiler are defined as type-directed
translations that transform both a program and its type. This allows the compiler to take advantage
of type information at compile-, link-, and run-time. The TILT compiler
generates code that is three times faster and uses half the space of other
competing compilers.
Types are also a useful tool for prototyping programming
languages and proving properties of programs. My work with Frank Pfenning
on the LF logical framework is concerned with the development of a "logic
workbench" that allows one to implement formal systems such as type
systems for programming languages or logics for reasoning about programs.
The LF language is a simple, yet expressive, type theory in which one may
describe the abstract syntax and deductive apparatus of a formal logical
system. The Twelf programming language may be used to build proof
checkers and theorem provers for a logic specified in LF. In a recent
case study Twelf was used to define a small assembly language for network
packet filters and to define a logic for stating and proving memory invariants
of programs written in this language. The program, together with the LF
representation of its proof, form a "self-certified" binary that may
be safely installed in an operating system kernel without fear of violating the
kernel's memory. Twelf has also been used to prototype experimental
languages, and to study the properties of logical systems such as linear logic.
Home Page: http://www.cs.cmu.edu/~rwh
ConCert Project: http://www.cs.cmu.edu/~concert
Twelf Project: http://www.cs.cmu.edu/~twelf
Aladdin Project: http://www.cs.cmu.edu/~aladdin
Fox Project (completed): http://www.cs.cmu.edu/~fox
ALEXANDER
HAUPTMANN
Senior Systems Scientist,
Computer Science
My research interests
revolve around the integration of text, image video and audio analysis. In the
Informedia Project we have built the News-on-Demand application, which is an
instantiation of the Informedia Digital Video Library idea, based completely on
automatic methods for processing television and radio news. Through the
combination of the strengths of speech recognition, natural language
processing, information retrieval and interface design, the system is able to
overcome some of the shortfalls inherent in each of the component technologies.
My goal is to utilize
large corpora of "found data", that is data that is already available
through the Internet or other readily accessible open sources, to improve
speech and natural language processing by exploiting advantages across
different modalities. It has become clear in recent years that large volumes of
text, image, video and audio can be easily stored and made available for
research and applications. However, most of these text, image, video and audio
sources were not produced with computer processing in mind. My intention is to
design and build intelligent, understanding programs that help process data
from these sources and make the data useful for other applications. This data
can be used to improve speech recognition, image understanding, natural
language processing, machine learning as well as information retrieval. The
challenge is to find the right data, process it into suitable form for training,
learning or re-use and build mechanisms that can successfully utilize this
data.
Speech and multimedia
technology is about to make a major impact on our daily interaction with
computers. What is needed at this point are clear demonstrations of the advantages
of integrated speech and multimedia interfaces.
JESSICA HODGINS
Associate Professor, Computer Science and Robotics
Dr. Hodgins's research focuses on the coordination and control
of dynamic physical systems, both natural and human-made and explores techniques
that may someday allow robots and animated creatures to plan and control their
actions in complex and unpredictable environments. Her current research focuses on generating motion for computer
animation by using control algorithms in combination with physically realistic
simulation. Hodgins and her students
have used these techniques to animate dynamic human behaviors such as running,
bicycling, diving, and vaulting. In
recent work they have combined simulation with motion capture to create human
simulations with more stylized movements.
Hodgins and her students have also explored passive simulations for
animating phenomena such as clothing, water, breaking objects, and explosions.
JAMES C. HOE
Assistant Professor,
Electrical and Computer Engineering and Computer Science(C)
My research interests cover many aspects of computer
architecture and digital hardware design. My current focus is on developing
high-level hardware description and synthesis technologies to simplify hardware
development. I am also working on innovative processor microarchitectures for
soft-error tolerance and security.
Operation-Centric Hardware Description and Synthesis: This
research develops a high-level hardware design framework that supports a new
hardware design abstraction. In an operation-centric description, the behavior
of a system is decomposed and described as a collection of atomic operations
(instead of the currently prevailing paradigm of decomposing into multiple
concurrent threads of execution). A high-level operation-centric representation
permits an unambiguous sequential interpretation by the designer and, at the
same time, allows a hardware compiler to automatically exploit available
parallelism by scheduling multiple operations for concurrent execution in the
resulting hardware implementation.
A Mathematical Approach to DSP Hardware Synthesis: This project develops a high-level synthesis
system for digital signal processing (DSP) hardware. The proposed framework
employs a natural symbolic mathematical representation for specifying DSP
transforms and their algorithms. Using knowledge in mathematics and algebra,
this framework manipulates a mathematical transform description to discover
what amounts to be different ways of "architecting" the desired DSP
circuit from basic hardware primitives. High-level optimizations, beyond the
means of normal logic optimizations, are accomplished by automatically
searching and evaluating this space of architecturally distinct
implementations.
SCOTT E. HUDSON
Associate Professor, Human Computer Interaction
My research interests lie
in the area of user interface software and technology. I am interested in
creating tools and software infrastructure which make it possible to produce high
quality user interfaces quickly and economically. This work includes the
creation of innovative new interaction techniques for 2D and 3D interaction,
development of advanced user interface toolkits, work in the use of constraint
systems for us
FACULTY
RESEARCH GUIDE