 |
|
||||||||||||||
 |
 |
 |
 |
 |
 |
 |
 |
|
|||||||
|
|
||||||||||||||
|
|
||||||||||||||
|
|
||||||||||||||
Fall 2001 to Spring 2002
Title: Taming the Infinite:
Verification of Parameterized Systems In this talk, we will survey approaches which combine ideas from the two methods to achieve higher degrees of automation in the verification of infinite-state systems. After exploring the various sources for infinity within systems, which could be due to complex control or architectural structure or due to extensive data, we will identify the main techniques proposed to deal with this "state explosion", and can be used to reduce an infinite-state system into a finite one. These include the techniques of abstraction, (de)composition, reduction due to symmetry, and generic instantiation. Typical successful applications of these techniques are the uniform verification of parameterized systems, where we consider a family of networks whose size (e.g. number of processes) is a parameter, and the method is able to establish its correctness for any value of the parameter. |
Title: How to find lots
of bugs with system-specific static analysis The first part of this talk shows how to automatically check such rules using system-specific static analysis. In our approach, system builders write simple compiler extensions that automatically check their code for rule violations. The approach has found thousands of errors in real systems such as Linux, OpenBSD, the Xok exokernel, and the FLASH machine's embedded software. Most extensions were less than a hundred lines of code and written by implementers who had a limited understanding of the systems checked. The second part of the talk describes how to automatically infer rules from the source code itself rather than having to know them a priori. The cornerstone of our approach is inferring "beliefs" from code that we then cross-check for contradictions. Beliefs are facts implied by code: a dereference of a pointer, "p", implies a belief that "p" is non-null, a call to "unlock(l)" implies that "l" was locked, etc. For beliefs we know the programmer must hold, such as the pointer dereference above, we immediately flag contradictions as errors. For beliefs that the programmer may hold, we can assume these beliefs hold and use a statistical analysis to rank the resulting errors from most to least likely. For example, if a call to "spin_lock" is paired with a call to "spin_unlock" 1000 times and not paired 1 time, this is a good indication that the code believes these calls must be paired, and that the single deviation is an error. The key feature of this approach is that it requires no a priori knowledge of truth: if two beliefs contradict, we know that one is an error without knowing what the correct belief is. Belief analysis allows us to infer 10-100 times things to check than if we relied on manual specification and to check properties we found impractical to manually specify. Bio: Dawson Engler is an Assistant Professor and
Terman Fellow at Stanford. He received his PhD from M.I.T. and his
undergraduate degree from University of Arizona, the latter in large
part funded by being a bouncer. His past work has ranged from extensible
operating systems to dynamic code generation. His current research
focuses on developing techniques to find as many interesting software
errors as possible. |
Title: Environment Management
for Augmented Reality This talk provides an overview of the work being done by Columbia's Computer Graphics and User Interfaces Laboratory to explore user interface design for collaborative mobile augmented reality systems. One issue that I will discuss is environment management, by which I mean the task of managing the presentation of a large number of virtual objects on many displays for many users. The use of see-through displays has a profound effect on the user interface, precisely because virtual objects appear in the same surrounding space as other users and physical objects. Thus, as a user's head moves, or anything visible through their see-through display moves, the user's combined view of the virtual and physical world also changes. For example, a static virtual object intended to be viewed next to a physical object may suddenly obscure or be obscured by it or other objects. To address these problems, we have developed a prototype environment management component that interactively manages the geometry of virtual objects to maintain desired viewplane relationships between them and other physical and virtual objects. Bio: Steven Feiner is a Professor of Computer
Science at Columbia University, where he directs the Computer Graphics
and User Interfaces Laboratory. He received a Ph.D. in Computer
Science from Brown University in 1987. His research interests include
virtual environments and augmented reality, knowledge-based design
of graphics and multimedia, information visualization, wearable
computing, and hypermedia. Prof. Feiner is coauthor of Computer
Graphics: Principles and Practice (Addison-Wesley, 1990) and of
Introduction to Computer Graphics (Addison-Wesley, 1993). He is
an associate editor of ACM Transactions on Graphics, has served
on the executive boards of the IEEE Computer Society Technical Committee
on Visualization and Graphics, and the IEEE Computer Society Task
Force on Human-Centered Information Systems, and is a member of
the steering committees for the IEEE Symposium on Information Visualization,
the IEEE and ACM International Symposium on Augmented Reality, and
the IEEE Symposium on Wearable Computers. Over the past year, he
has been general chair of IEEE Information Visualization 2001, symposium
co-chair of the IEEE and ACM International Symposium on Augmented
Reality 2001, and program co-chair of the International Symposium
on Mixed Reality 2001. In 1991 he received an Office of Naval Research
Young Investigator Award. |
Title: Optimizing Component
Interaction Optimizing component interaction is a fundamental problem in constructing efficient component-oriented programs. Our work lays out a foundation for reformulating the implementation of the interaction between components, with the goal of optimizing the assembled system. Our approach amounts to automatically choosing among a number of candidate implementation alternatives for each of the data structures and communication mechanisms that the components use during their interactions. This choice is done by an interesting combination of dynamic and static analysis. The system becomes aware of alternatives one component can offer to another and what kinds of uses another requires and so we can get the two interacting better via the system than seems permissible with good software engineering practice. Some of our initial work in this area has shown how to transform one example of component interaction optimization into a graph problem, and has proposed analysis of dynamics and fast graph reduction heuristics as an efficient technique for solving the problem. Our hope is that this work will inspire debate that ultimately will lead to a new area of investigation, within the field of compiler-performed optimization, with the potential to achieve orders of magnitude improvements in the performance of component-oriented programs. Bio: Mark Wegman received his undergraduate degree from NYU and his Ph.D. from Berkeley. He has been at IBM Research working on program analysis and related topics for more than 20 years. He is known for his work in data compression, and program optimization and static single assignment analysis for programming languages. More recently he has worked with some groups at IBM building technologies for visualizing the behavior of object oriented programs and automatically animating them. In addition to programmer productivity, his professional interests include, compiler technologies and programming languages, algorithm design, and information theory. Mark is a fellow of the ACM and has recently been elected to the
technical committee of the IBM Academy of Science and Engineering
(modelled on the National Academy). He is also a senior manager
at IBM Research responsible for the area of Object and Enterprise
Programming. |
Title: Computational Geometry
for Sculpture For examples of Hart's work, see http://www.georgehart.com |
| Title: Artificial Intelligence
and the Imminent Revolution in Brain Science |
Distinguished Lecture Series
