Sponsored by |
|
Listing of Talks Abstracts Return to Colloquium Homepage

Edmund M. Clarke
Logical errors in sequential circuit designs and communication protocols are an important problem for system designers. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. My research group has developed a verification method called temporal logic model checking for this class of systems. In this approach specifications are expressed in a propositional temporal logic, while circuits and protocols are modeled as state--transition systems. An efficient search procedure is used to determine automatically if a specification is satisfied by some transition system. The technique has been used in the past to find subtle errors in a number of non-trivial examples. During the last few years, the size of the state-transition systems that can be verified by model checking techniques has increased dramatically. By representing transition relations implicitly using Binary Decision Diagrams (BDDs), we have been able to check some examples that would have required 1020 states with the original algorithm. Various refinements of the BDD-based techniques have pushed the state count up to 10100. By combining model checking with various abstraction techniques, we have been able to handle even larger systems. For example, we have used this technique to verify the cache coherence protocol in the IEEE Futurebus+ Standard. We found several errors that had been previously undetected. Apparently, this is the first time that formal methods have been used to find nontrivial errors in an IEEE standard. Prof. Clarke will also give an informal talk to people in the department that are interested in the areas of formal specification, automated verification and reliable systems.
BACK Jihoon Yang
The recent proliferation of computers and communication networks has made it possible for individuals around the world to access a wide variety of information sources through the Internet. However, effective use of these information sources requires fairly sophisticated tools or information assistants for locating, classifying, selectively retrieving and extracting knowledge from data. Intelligent agents, mobile agents, and multi-agent systems provide an attractive approach to the design of such information assistants. Intelligent behavior in any domain requires knowledge of the domain. Machine learning is arguably the most practical and cost-effective approach to automated knowledge acquisition. This describes the design and implementation, and integration into a mobile agent platform, of software agents for selective information retrieval and data-driven knowledge discovery. Information retrieval agents acquire knowledge of the user's interests through machine learning. Knowledge discovery agents apply machine learning algorithms to extract knowledge from data. Artificial neural networks provide an attractive approach to machine learning because of their potential for massive parallelism and fault tolerance. We present DistAl, a novel algorithm for automated construction of pattern classifiers from data. DistAl is significantly faster than conventional neural network algorithms and has been demonstrated to perform well on a broad variety of benchmark data-driven knowledge discovery problems. The performance of DistAl can be further improved by using it in conjunction with a genetic algorithm for automated selection of attributes used to encode the data. DistAl can also be used for data-driven refinement of incomplete or inaccurate domain knowledge. The talk will discuss the design and implementation of DistAl and its use in a number of data-driven knowledge discovery applications (including the design of customizable information assistants). We conclude with a brief discussion of some directions for ongoing and future research in machine learning and multi-agent systems.
BACK Andrew William
Much research has been done on intelligent agent knowledge sharing through the use of common, pre-defined ontologies. However, several domains, including the World Wide Web, often precipitate intelligent agents selfishly inventing ontologies based on their utility for the task at hand. If such agents are able and willing to teach each other semantic concepts based on their individual ontologies, then the entire group of agents can accomplish their group and individual tasks more efficiently and with more creativity. We outline the hypotheses we are investigating, review the design of our prototype system, and describe our proposed method for multiagent learning with diverse ontologies using the World Wide Web domain.
BACK Kelvin Nilson
Java was created by Sun Microsystems as part of a research project to "develop advanced software for a wide variety of networked devices and embedded systems." In this talk, Dr. Nilsen provides an introductory overview of the state of the art in embedded and real-time development and discusses Java's strengths and weaknesses in this application domain. Dr. Nilsen also describes a number of extensions for the standard Java platform that make Java more appropriate for real-time programming.
BACKYan Bin-Jia
The first part of the talk describes two geometric algorithms for computing the pose (position and orientation) of a polygonal part, from a continuum and a finite number of possible poses, respectively. Both algorithms can generalize to other shapes in two and three dimensions. The first algorithm uses simple geometric constraints (i.e., two inscribing cones) to immobilize the polygonal part. Although the number of ambiguous poses in the worst case are linear in the number of polygon vertices, extensive simulations demonstrate that no ambiguity would arise in most cases. The second algorithm distinguishes the real pose from a finite number of apparent poses by point probing. Minimizing the number of probes is shown to be NP-complete. And a greedy approximation algorithm is subsequently designed with logarithmic ratio, which is then proven to be hard to improve on. Applying nonlinear control theory, the second part of the talk establishes that the states of objects are often locally observable through contact in typical manipulation tasks. I present an approach, termed pose and motion from contact , for estimating the pose and motion of a manipulated object from a small amount of tactile data. In particular, I have investigated the task of a finger pushing an object in the plane and developed two nonlinear observers as sensing strategies: the first one is asymptotic while the second one requires minimum sensor data. In addition to simulations, I have implemented a contact sensor using strain gauges. Generalizing the above results to three dimensions, I conclude my talk with a study on the local observability of a rolling object on a translating horizontal palm, through cotangent space decomposition.
BACKSuzanne & Ralph Tomlinson
R.C. Sekar
Our increasing reliance on networked information systems to support
critical infrastructures (e.g, telecommunication, commerce and banking,
power distribution, and transportation) has prompted interest in making
the information systems survivable, so that they continue to perform
their primary functions even in the face of coordinated attacks and
spontaneous failures. Of particular importance are techniques that can
enhance the survivability of today's systems, as opposed to requiring
them to be completely redesigned and/or reimplemented.
Most attacks on current networked information systems exploit
vulnerabilities that can ultimately be traced to software flaws.
Consequently, recent research has focussed on analysis techniques to
determine whether such errors lead to exploitable vulnerabilities (
vulnerability analysis), and detection techniques to identify actual
exploitation of these vulnerabilities (intrusion detection). Whereas
previous efforts could only detect attacks after the fact, our approach
can prevent large classes of attacks before they cause damage. Our
approach can also launch automatic responses aimed at isolating and
containing damage. The key observation behind our approach is that
regardless of how an intrusion takes place, damage must ultimately be
effected via system calls provided by the operating system or network
packets delivered to the system. We therefore develop a high-level
language in which normal system behaviors can be specified in terms of
interactions of processes with the operating system kernel, and network
packets received or transmitted by the system. We then develop algorithms
for compiling these specifications into efficient extended finite-state
automata that can recognize deviations from specified behaviors,
indicating potential intrusions. We discuss our implementation of these
techniques into a high-performance intrusion detection system, and the
results of its participation in a recent competition of intrusion
detection systems organized by MIT Lincoln Laboratories and DARPA.
Chou Hui-Hsein
In this decade we saw a major breakthrough in life science research, i.e. the use of automatic sequencing machines to churn out data of living cells at an enormous speed compared to methods a decade ago. Combined that with other advance techniques, biological data is accumulating far faster than before. This creates a new challenge to scientists: how can we effectively make use of this large volume of new data? In the past the problem has always been "how to get the data out of a cell ?". Now suddenly it changes to "How to analyze the huge amount of data in our life time?" A new field, called bioinformatic, has emerged to address this problem. It focuses on biological data acquisition, storage, analysis and dissipation. In addition to that field, many biological research can now be carried out partially on computers and new discoveries can be made without the need to go to the "wet lab", thus a new field has also emerged, the computational biology. Although these two new fields cannot replace the traditional "wet lab" experiments, they can dramatically cut down on their numbers. With the help of bioinformatic and computational biology techniques, biologists can better utilize their limited wet lab resource on solving critical problems, rather than wasting them on the sea of all possibilities. Recently, life science research has become a "big science" just like the Apollo project in the 60s or the high energy accelerator projects in the 70s/80s. It has to involve not just biologists but physicists, mathematicians and especially computer scientists. The well-known Human Genome Project, is just one example of that. In this talk I will briefly introduce various topics in bioinformatic and computational biology that require nontrivial computer techniques. This will show what we as computer scientists can do to help advance life science research. Next, I will present a specific example I was involved last year. It tells us that some computer works in these fields are better suited for computer scientists rather than biologists.
BACKBwolen Yang
Symbolic model checking is an automatic verification paradigm for checking temporal properties (e.g., safety, liveness, fairness) of finite state systems. It has been successfully applied to a variety of applications, ranging from hardware designs to software protocols. The technology enabling these successes is the use of Binary Decision Diagrams (BDDs) to perform symbolic computation. BDD computations are both time and space intensive and their computational characteristics are not well understood. In this talk, I will address this issue at two levels. At the low level, I will present an evaluation methodology for systematically studying BDD computation. Application of this methodology to model checking computations led to better understanding of the computation and significant performance improvements. At the high level, I will describe a new algorithm to reduce the state space for a special class of constraint-rich models. Together, these optimizations resulted in a powerful model checker, which enabled verification of fault diagnosis models in the NASA Deep Space One spacecraft. Tuesday, March 9, at 3:30 pm in 1652 Gillman Refreshments will be served afterwards in 213 Atanasoff.
BACKHongwei Hi
Security concerns with mobile code have raised many challenging questions in compiler optimization. A significant example is that array bound checks must be performed at run-time to enforce the memory safety of mobile code. This practice can become prohibitively expensive in cases such as numerical computation. In particular, it can be readily observed that Java applets often incur a vast number of run-time array bound checks when performing tasks related to graphics. In this talk, we present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types. With such a type system, the memory safety property of mobile code can be captured with types and thus verified through type-checking before execution. This enables us to eliminate array bound checks in mobile code statically, leading to both safer and faster execution. We intend to use this assembly language as a target language for compiling high-level source languages with dependent type annotations. Thursday, Mar. 11, 1999, at 3:30pm in B29 Atanasoff Refreshments will be served afterwards in 213 Atanasoff.
BACKOm P. Damani
Leslie Lamport once described a distributed system as one in which the failure of a computer you did not even know existed can render your own computer unusable. Clearly, fault-tolerance issues need to be addressed before the power of distributed computing can be fully exploited. My research work has primarily focused on the use of message logging for recovering from process crashes in distributed systems. Optimistic protocols, an important class of message logging protocols, minimize fault-tolerance overhead based on the fact that failures are rare. We have designed an efficient optimistic protocol, which tolerates multiple concurrent failures with low overhead. Natural extensions of optimistic protocols to multi-threaded environments offer a trade-off between false causality and failure-free overhead. We eliminate this trade-off by simultaneously treating a thread as the unit of recovery and a process as the unit of failure. Despite lower overhead of optimistic logging, many industrial applications have chosen 'pessimistic' (synchronous) logging for fast and localized recovery. We have designed an adaptive protocol to fine-tune the 'degree of optimism', thus, bridging the gap between pessimistic and optimistic logging. I will present the main ideas behind these protocols and the results of our experiments.
BACKWallapak Tavanapong
Recent advances in multimedia processing technologies, internetworking technologies, and the World Wide Web phenomenon have resulted in a vast creation and use of digital videos in all kinds of applications ranging from entertainment, business solutions, to education. Designing efficient techniques for searching and retrieving videos becomes increasingly more important as more digital videos are being archived daily. To address this issue, many techniques have been proposed by two distinct research communities. Database researchers have been focusing on techniques for searching video data. Independently, computer communications researchers have been investigating video delivery techniques. Little work, if any, has been done to relate these two topics although searching for video data is typically an interactive process which involves the transmission of video data. VideoCenter presents one such unified approach. It can offer video browsing and search operations with little delays and with minimum storage requirements. The visual quality of the browsing and the search operations are excellent. VideoCenter can handle its own search operations without involving the server making it more scalable.
BACKSandeep Kulkarni
My talk will be divided into two parts. In the first part, I will present two components, {\em detectors} and {\em correctors}, that form a basis of fault-tolerant systems. This part shows that for a rich class of fault-tolerant systems --including those designed by existing methods-- these components are both necessary and sufficient. The necessity is shown by identifying the components used in a given fault-tolerant system. The sufficiency is shown by designing components that will transform the given fault-intolerant system into a fault-tolerant one. In the second part of my talk, I will illustrate our method to design fault-tolerant systems using detectors and correctors. Towards this end, I will show how our fault-tolerant distributed reset protocol is designed using these components. Our protocol is multitolerant in the sense that it tolerates multiple types of faults and provides different levels of fault-tolerance to each type. This example shows how the use of these components helped us in the design of this {\em first} multitolerant distributed reset protocol. Tuesday, March 30, at 3:30 pm in 1652 Gillman Refreshments will be served afterwards in 213 Atanasoff.
BACKPhyllis Crandall
With the demise of the majority of supercomputer vendors in the last few years, high performance computing platforms have taken a new direction. "Clustering" has now become the architecture of choice. In this structural paradigm, collections of components that can themselves be treated as stand-alone computers are combined to produce a high-end parallel computational environment. Cluster designs vary from the common (networks of workstations) to the exotic (clusters of Cray/SGI Origin 2000s). Additionally, these clusters usually include a combination of both shared and distributed memory systems. While these platforms have incredibly high theoretical peak speeds, programming in this environment is still so new that no theories have been developed regarding the programming methods that will yield the best performance. In this talk I will describe the issues that arise in the high-performance distributed shared memory environment, ways to address these issues, experimental data that show the consequences of some of the solutions, and the beginnings of an analytical theory to determine the best programming paradigms in this complex environment. Thursday, April 8, at 3:30 p.m. in B29 Atanasoff
BACKBill Fulkerson
Bill will discuss the role of information technology in the transition from the industrial economy to the informational economy for discrete manufacturing. In particular, he will discuss classes of business solutions needed to support mass customization.
BACKMaria Carla Calzarossa
The performance of High Performance Fortran (HPF) applications depends on their inherent parallelism and on the strategies adopted by compilation systems to distribute work and data among the processors. The evaluation of the performance of HPF applications has to consider all the aspects which in different ways determine such performance. This talk presents an experimental approach towards performance analysis of HPF applications. This approach addresses all the performance issues typical of these applications. Medea, a software tool developed at the University of Pavia, is in integral part of this approach. Medea provides various types of statistical and visualization facilities for the analysis of measurements collected while the applications are being executed on a parallel system. In such a way, performance analysis of HPF applications can be carried out at various levels of detail.
BACKSamir Ranjan Das
A mobile ad hoc network is an autonomous system of mobile hosts connected purely by wireless links. Such networks are useful in military and other tactical applications, e.g., emergency rescue or exploration missions, where cellular infrastructure is unavailable or unusable. Because of constantly changing topology, ad hoc networks must adopt efficient dynamic routing techniques. Routing overhead is a major concern, as the wireless link bandwidth is typically small. Recently, a new class of protocols called "on-demand" protocols has received attention because of their very low routing overhead. On-demand protocols discover routes on an "as-needed" basis, rather than in a more proactive fashion, as in the traditional link state or distance vector protocols. We will present a comparative simulation study of on-demand protocols with the more traditional proactive protocols. We will demonstrate that over-reliance on query flooding can actually cause on-demand protocols lose their overhead advantages at high loads. We will describe a new query control approach that reduces the routing overhead by a significant extent. We will also explore new multipathing techniques that can reduce overheads further. Towards the end of the talk, we will present our past work on fast and efficient network simulation via parallel discrete event simulation (PDES). We will conclude by pointing out how preformance study of ad hoc networks can benefit from using PDES techniques. Thursday, April 22 at 3:30 pm in B29 Atanasoff Refreshments will be served afterwards in 213 Atanasoff
BACKChi-Hsiang Yeh
Colloquium Abstract: Meshes, tori, k-ary n-cubes, and hypercubes are the most popular networks for the interconnection of parallel processors. This talk will introduce some efficient algorithms for communications in these networks with or without faults. In a dynamic communication problem, the packets to be routed/broadcast are generated at each node of a network or parallel computer according to a certain random process. We introduce the priority broadcast scheme for dynamic broadcasting in meshes, tori, and hypercubes. Based on this scheme, we show that the time required for dynamic broadcast in an n-dimensional hypercube or k-ary n-cube is O(n + 1/(1-rho}), which is asymptotically optimal and improves the best previous results by a factor of n, where rho is the throughput factor and k=O(1). We then show that by using a unified scheme for routing and broadcasting, the throughput for communications in general meshes and tori can be considerably improved. The priority broadcast scheme can also be applied to the multicasting problem in communication networks. We further explore the communications problem in meshes and tori with faulty nodes and links. We introduce the robust-algorithm approach, incorporating fault tolerance into the design of algorithms. No hardware redundancy or bypass capability is required and no assumption is made about the availability of a complete submesh or subtorus. Based on this approach, a wide variety of algorithms, such as unicast, broadcast, permutation routing, total exchange, multinode broadcast, sorting, reduction, prefix computation, and fast Fourier transform (FFT), can all be executed on faulty meshes, tori, and k-ary n-cubes with a factor of 1+o(1) slowdown relative to a fault-free array of the same type.
BACK
(Top)
Thank you for visiting this page.Please send your suggestions and comments to one of us in the Computer Science colloquium commitee.
(Top)