Computer Science: Past, Present, and Future

September 22, 2009

Abstract:
The National Science Foundation created the Computing Community Consortium to stimulate the computing research community to envision and pursue longer-range, more audacious research challenges.

I'd like to take this opportunity to engage you in this process. The next ten years of advances in computer science should be far more significant, and far more interesting, than the past ten. I'll review the progress that our field has made, and I'll present a number of "grand challenge" problems that we should be prepared to tackle in the coming decade.

Bio:
Lazowska focuses on the design, implementation, and analysis of high performance computing and communication systems. He is a member of the Microsoft Research Technical Advisory Board, and serves as a board member for a number of high-tech and venture companies. He co-chaired the President’s Information Technology Advisory Committee from 2003-05, and chairs the Computing Community Consortium, an effort created to engage the computing research community in envisioning more audacious research challenges. He is a Member of the National Academy of Engineering and a Fellow of the American Academy of Arts & Sciences, ACM, IEEE, and AAAS.

Discrete Stochastic Simulation of Spatially Inhomogeneous Biochemical Systems

October 20, 2009

Abstract:
In microscopic systems formed by living cells, the small numbers of some reactant molecules can result in dynamical behavior that is discrete and stochastic rather than continuous and deterministic. An analysis tool that respects these dynamical characteristics is the stochastic simulation algorithm (SSA), which applies to well-stirred chemically reacting systems. However, cells are hardly homogeneous!

Spatio-temporal gradients and patterns play an important role in many biochemical processes. In this lecture we report on recent progress in the development of methods for spatial stochastic and multiscale simulation, and outline some of the many interesting complications that arise in the modeling and simulation of spatially inhomogeneous biochemical systems.

Bio:
Petzold focuses on the development of computational methods for multiscale discrete stochastic simulation of biochemical kinetics, as well as the formulation and analysis of mathematical models for biochemical systems including circadian rhythm, unfolded protein response, diabetes type 2, polarization in yeast mating and coagulopathy. She is the recipient of numerous awards including the Wilkinson Prize for Numerical Software, the Dahlquist Prize, and the Sonia Kovalevski Prize. She is a Fellow of SIAM, ASME and AAAS, and is a member of the U.S. National Academy of Engineering.

My 28-year Quest to Overcome the State Explosion Problem

November 10, 2009

Abstract:
Model Checking is an automatic verification technique for state-transition systems that are finite-state or that have finite-state abstractions. In the early 1980’s in a series of joint papers with my graduate students E.A. Emerson and A.P. Sistla, we proposed that Model Checking could be used for verifying concurrent systems and gave algorithms for this purpose. At roughly the same time, Joseph Sifakis and his student J.P. Queille at the University of Grenoble independently developed a similar technique. Model Checking has been used successfully to reason about computer hardware and communication protocols and is beginning to be used for verifying computer software. Specifications are written in temporal logic, which is particularly valuable for expressing concurrency properties. An intelligent, exhaustive search is used to determine if the specification is true or not. If the specification is not true, the Model Checker will produce a counterexample execution trace that shows why the specification does not hold. This feature is extremely useful for finding obscure errors in complex systems. The main disadvantage of Model Checking is the state-explosion problem, which can occur if the system under verification has many processes or complex data structures. Although the state-explosion problem is inevitable in worst case, over the past 27 years considerable progress has been made on the problem for certain classes of state-transition systems that occur often in practice. In this talk, I will describe what Model Checking is, how it works, and the main techniques that have been developed for combating the state explosion problem.

Bio:
Clarke’s interests include software and hardware verification and automatic theorem proving. His research group pioneered the use of Model Checking for hardware verification, developed Symbolic Model Checking using BDDs, and developed the first parallel resolution theorem prover (Parthenon) and the first theorem prover to be based on a symbolic computation system (Analytica). Among other awards, Clarke was a recipient of the 2007 ACM Turing Award (with Allen Emerson and Joseph Sifakis) for his role in developing Model Checking into a highly effective verification technology, widely adopted in the hardware and software industries.

High Performance Computers and Compilers: A Personal Perspective

December 1, 2009

Abstract:
The talk will describe a related sequence of projects including some early, very bold projects that profoundly influenced high performance computing even as some of them failed. The talk includes a personal perspective of what worked and what didn’t, the historical threads of some ideas and the lessons learned. The talk concludes by identifying some current compiler challenges and the need for a new focus on new compilers.

Bio:
Allen’s work focuses on compilers and languages that together enable both application performance and user productivity on high performance computers. The resulting advances have led to numerous awards for Allen including ACM’s 2006 Turing Award “For pioneering contributions to the theory and practice of optimizing compiler techniques that laid the foundation for modern optimizing compilers and automatic parallel execution.” She is a member of the American Philosophical Society, the National Academy of Engineering, a Fellow of the American Academy of Arts and Sciences, ACM, IEEE, and the Computer History Museum, and the recipient of six honorary doctorates.

Interactive Media Research at The Walt Disney Company

February 9, 2010

Abstract:
The research challenges in interactive media faced by the different business units of The Walt Disney Company fall in four broad categories: motion pictures, park attractions, games & sports, and media networks. Enumerating these challenges provides a key industry perspective on promising directions for future research in digital arts, experiential media systems, creative environments, and emerging media technologies.

Bio:
Marks’ areas of interest include computer graphics, human-computer interaction, and artificial intelligence. He has worked previously at Bolt Beranek and Newman and at Digital’s Cambridge Research Laboratory. Prior to joining The Walt Disney Company he was the Research Director at Mitsubishi Electric Research Labs in Cambridge, MA, from 2000-2006. In addition to numerous other service activities, he has served as Chair of ACM SIGART, SIGGRAPH 2007 Conference Chair, and he is currently a member of the DARPA ISAT Study Group.