|
|
Date (
Fall 2008
) |
Speaker and Abstract |
| 2008/09/19 |
Speaker:
Baochun
Li
Affiliation: University of Toronto
Title: Live Peer-to-Peer Streaming Systems with Network Coding
Abstract: Recent years have witnessed real-world success of peer-to-peer (P2P) live streaming systems. In this talk, we discuss some of our recent work and understanding on the use of network coding in P2P live streaming protocol design. we seek to analyze and understand a new family of streaming protocols, simultaneously considering important performance metrics, such as playback quality, initial buffering delay, server bandwidth costs, and resilience to peer dynamics. We believe that network coding eliminates some of the analytical difficulties associated with previous theoretical models, and leads to simple and practical streaming protocols. This simplification makes it possible to take into account all of the important performance metrics, even under a more realistic system model.
We identify several design principles for streaming systems with network coding and show that any protocol following our design principles is sufficient to achieve provably good overall performance in realistic settings. In particular, we have provided sufficient conditions on the required server bandwidth costs to ensure smooth playback under peer dynamics, and with short initial buffering delays. A closer look at these conditions further suggests that our design principles are able to achieve near-optimal bandwidth utilization during flash crowds and to handle severe peer dynamics with ease.
Our design principles can be readily implemented in practice with low overhead. Through an example of a practical protocol design, combined with our theoretical framework of fundamental properties, we have provided a striking demonstration of an effective streaming protocol design with network coding. We believe our theoretical framework will bring considerable light into the journey towards the best possible protocols in P2P streaming systems.
Biography of Speaker:
-
Baochun Li received his B.Engr. degree in 1995 from Department of Computer Science and Technology, Tsinghua University, China, and his M.S. and Ph.D. degrees in 1997 and 2000 from the Department of Computer Science, University of Illinois at Urbana-Champaign. Since 2000, he has been with the Department of Electrical and Computer Engineering at the University of Toronto, where he is currently a Full Professor. He holds the Bell University Laboratories Endowed Chair in Computer Engineering since August 2005. In 2000, he was the recipient of the IEEE Communications Society Leonard G. Abraham Award in the Field of Communications Systems. His research interests include large-scale multimedia systems, peer-to-peer networks, applications of network coding, and wireless networks. He is a senior member of IEEE, and a member of ACM.
|
| 2008/10/03 |
Speaker:
Insup
Lee
Affiliation: University of Pennsylvania
Area:
Systems and Networking
Title: Compositional Real-Time Schedulability Analysis Techniques: Challenges, Techniques, and Open Problem
Abstract: Real-Time Embedded Systems (RTES) consist of a collection of components that interact with each other and with their environment through sensors and actuators. Embedded systems are built into physical computing systems such as aircraft, automobiles, medical devices, robots, and consumer electronics. As embedded systems become more complex, component-based technologies are becoming an essential alternative to traditional monolithic design approaches. The main advantage of a component-based technology is that complexity can be effectively managed by encapsulating large system modules within a component. Each component exposes an interface that abstracts and hides component details and complexities. Component interface allows a component to be composed with other components. While designing of individual components is well understood, the integration and interoperability of components present challenges in adopting the framework. One essential challenge is to support compositionality, which means that the properties of a system can be determined from the properties of its components. We have been developing a hierarchical, resource-based framework for RTES using components. One salient aspect is compositional schedulability analysis techniques for RTES, based on the assume-guarantee reasoning of formal methods. I will describe various resource demand models, resource supply models, and compositional analysis methods, and applications.
If time permits, I will also talk about Cyber Physical Systems (CPS). CPS are to meet the needs of the new generation of engineered systems that are highly dependable, efficiently produced and certified, and capable of advanced performance in computation, communication, and control. The Internet transformed how we interact and communicate with one another and also revolutionized how and where we access information. We believe that CPS will transform how we interact with and control the physical world around us. I will describe the opportunities and challenges of CPS.
Biography of Speaker:
-
Insup Lee received the B.S. degree in mathematics from the University of North Carolina, Chapel Hill, in 1977, and the Ph.D. degree in computer science from the University of Wisconsin, Madison, in 1983. He is the Cecilia Fitler Moore Professor in the Department of Computer and Information Science at the University of Pennsylvania, where he has been since 1983. He was CSE Undergraduate Curriculum Chair from September 1994 to August 1997.
His research interests include embedded systems, real-time computing, formal methods, wireless network, and software engineering. He has been developing programming concepts, language constructs, and operating systems for real-time systems. In recent years, he has developed specification, analysis, and testing techniques based on real-time process algebra (ACSR). In addition, he has devoloped a hierarchical specification language for hybrid systems (CHARON). Based on CHARON, he has been developing techniques for automatic code generation and test generation. He also has benn developing the run-time monitoring and checking framework (MaC) that can be used to assure the correctness of a running system through monitoring and checking of safety, QoS, and security properties. The prototype MaC system has been implemented in Java and C. In addition to doing research, he has been transitioning research results to practice by applying them to safety-critical real-time systems and high-confidence medical devices. He has published widely and received the best paper award in RTSS 2003 on compositional schedulability analysis.
He was Chair of IEEE Computer Society Technical Committee on Real-Time Systems (2003-2004) and an IEEE CS Distinguished Visitor Speaker (2004-2006). He has served on many program committees and chaired several international conferences and workshops, including IEEE RTSS, IEEE RTCSA, IEEE ISORC, CONCUR, ACM EMSOFT, and HCMDSS/MD PnP. He has also served on various steering and advisory committees of technical societies, including Steering Committee on ACM SIGBED and Co-Chair of IEEE CS Technical Steering Committee on Embedded Systems. He has served on the editorial boards on the several scientific journals, including IEEE Transactions on Computers, Formal Methods in System Design, and Real-Time Systems Journal. He is a co-Editor-in-Chief of KIISE Journal of Computing Science and Engineering since Sept 2007. He is IEEE Fellow and a member of Technical Advisory Group (TAG) of President's Council of Advisors on Science and Technology (PCAST) Networking and Information Technology (NIT).
|
| 2008/10/10 |
Speaker:
Aleks
Nanevski
Affiliation: Microsoft Research
Title: Program verification with Hoare Type Theory
Abstract: Two main properties make type systems an effective and scalable formal
method. First, important classes of programming errors are eliminated
by statically enforcing the correct use of values. Second, types
facilitate modular software development by serving as specifications
of program components, while hiding the component's actual
implementation. Implementations with the same type can be
interchanged, thus facilitating software reuse and evolution.
Mainstream type systems focus on specifying relatively simple
properties that admit type inference and checking with little or no
input from the programmer. Unfortunately, this leaves a number of
properties, including data structure invariants and API protocols
outside of their reach, and also restricts the practical programming
features that can be safely supported. For example, most simply-typed
languages cannot safely allow low-level operations such as pointer
arithmetic or explicit memory management.
In this talk, I will describe Hoare Type Theory (HTT) which combines
dependent types of a system like Coq with features for specification
and verification of low-level stateful operations in the style of
Hoare Logic. The specification is performed via types -- which we call
Hoare types -- thus also guaranteeing that the system is modular in
nature.
Such a combination is desirable for several reasons. On the
type-theoretic side, it makes it possible to integrate stateful
behavior into dependent type theories that have so far been purely
functional. On the Hoare Logic side, it makes is possible to use the
higher-order data abstraction and information hiding mechanisms of
type theory, which are essential for scaling any kind of verification
effort. For example, by combining type-theoretic abstractions with
Hoare types, it is possible to ascribe common specifications to
stateful data types (e.g. hash tables and splay trees), which
functionally implement the same data structure (finite map), but have
very different stateful behavior.
From the technical standpoint, it is interesting that the design of
HTT relates in an essential way some of the most venerable ideas from
programming language theory such as Dijkstra's predicate transformers,
Curry-Howard isomorphism and monads.
I will discuss the implementation of HTT (called Y-not) which is
currently under way, as well as the possibilities for scaling HTT to
support further programming features.
This is joint work with Greg Morriset, Lars Birkedal, Amal Ahmed,
Rasmus Petersen, Avi Shinnar and Paul Govereau.
Biography of Speaker:
-
|
| 2008/10/17 |
Speaker:
Victor
Zordan
Affiliation: CSE Department, UC Riverside
Area:
Graphics
Title: Animating characters using motion capture and simulation
Abstract: Automatically creating humanlike animation for characters is
difficult, especially in applications such as video games and online
environments where the characters must move realistically, respond to
unpredicted events, and remain controllable at a high level by the
users of such virtual worlds. In this talk, I describe several
techniques for generating realistic character motion using examples
recorded from humans and physically based models, focusing primarily
on controllable, responsive characters that combine dynamic simulation
and recorded data. My research relies on human examples to dictate
movement style and on simulation to create physically plausible motion
including interactions with the environment and other simulated
characters. Emphasis will be placed on generating believable
unpredicted responses within a motion capture dependent animation
system as well as on using both motion capture and simulation alone as
mechanisms for generating high fidelity movement for humans. The talk
will close with a brief discussion about the role of physics in
generating games and online motion that is beyond the scope of
applications seen today.
Biography of Speaker:
-
Dr. Victor Zordan is an Assistant Professor of Computer Science and Engineering at UC Riverside, Dr. Victor Zordan received his Ph.D. in computer science from Georgia Institute of Technology in 2002. Professor Zordan's research interests fall in several areas of computer animation including human motion, physically based modeling, interactive virtual environments, behavior control, and character design. He has published numerous papers on the control of human and humanlike characters as well as on several other topics including anatomical modeling, procedural approaches, and video-based animation.
|
| 2008/10/24 |
Speaker:
Andreas
Zeller
Affiliation: Saarland University
Area:
Software Engineering
Title: Seeding Bugs to Find Bugs: Mutation Testing Revisited
Abstract: How do you know your test suite is "good enough"? One of the best ways to tell is mutation testing. Mutation testing seeds artificial defects (mutations) into a program and checks whether your test suite finds them. If it does not, this means your test suite is not adequate yet.
Despite its effectiveness, mutation testing has two issues. First, it requires large computing resources to re-run the test suite again and again. Second, and this is worse, a mutation to the program can keep the program's semantics unchanged - and thus cannot be detected by any test. Such equivalent mutants act as false positives; they have to be assessed and isolated manually, which is an extremely tedious task.
In this talk, I present the JAVALANCHE framework for mutation testing of Java programs, which addresses both the problems of efficiency and equivalent mutants. First, JAVALANCHE is built for efficiency from the ground up, manipulating byte code directly and allowing mutation testing of programs that are several orders of magnitude larger than earlier research subjects. Second, JAVALANCHE addresses the problem of equivalent mutants by assessing the impact of mutations on dynamic invariants: The more invariants impacted by a mutation, the more likely it is to be useful for improving test suites.
We have evaluated JAVALANCHE on seven industrial-size programs, confirming its effectiveness. With less than 3% of equivalent mutants, our approach provides a precise and fully automatic measure of the adequacy of a test suite - making mutation testing, finally, applicable in practice.
Joint work with David Schuler and Valentin Dallmeier.
Biography of Speaker:
-
Andreas Zeller is computer science professor at Saarland University; he researches large programs and their history, and has developed a number of methods to determine the causes of program failures - on open-source programs as well as in industrial contexts at IBM, Microsoft, SAP and others. His book "Why Programs Fail" has received the Software Development Magazine productivity award in 2006.
|
| 2008/10/31 |
Speaker:
Klara
Nahrstedt
Affiliation: University of Illinois at Urbana-Champaign
Title: View-casting:View-based Stream Dissemination and Control for Multi-Party 3D Tele-immersive Environme
Abstract: Tele-immersive 3D multi-camera, multi-display room environments are emerging and with them new challenging research questions. One important question is how to organize the large amount of visual data, being captured, processed, transmitted and displayed, and their corresponding resources over current COTS computing and networking infrastructures so that “everybody” would be able to install and use tele-immersive environments for interactive physical activities. In this talk, I introduce the concept of a view to deal with and translate between the large amount of data, these immersive and interactive environments produce, and the bandwidth/delay barriers of current COTS networks and operating systems for these environments. I will discuss our cross-layer control, adaptive streaming framework with view dissemination, called TEEVE (Tele-immersive Environments for EVErybody). TEEVE aims for (1) effective and adaptive coordination, synchronization and soft QoS-enabled delivery of tele-immersive visual streams to remote rooms, and (2) effective view-casting model for different view dissemination in the multi-party 3D tele-immersive environments.
This is a joint work with Zhenyu Yang, Wanmin Wu, and Ruzena Bajcsy.
Biography of Speaker:
-
Klara Nahrstedt is a professor at the University of Illinois at Urbana-Champaign, Computer Science Department. Her research interests are directed towards multimedia middleware systems, QoS-aware resource management in distributed multimedia systems. She is the recipient of the Early NSF Career Award, the Junior Xerox Award, the IEEE Communication Society Leonard Abraham Award for Research Achievements, the Ralph and Catherine Fisher Professorship Chair, and IEEE Fellow. She is the general chair Percom 2009, and the elected chair of ACM Special Interest Group in Multimedia (2007-2009).
Klara Nahrstedt received her BA in mathematics from Humboldt University, Berlin, in 1984, and M.Sc. degree in numerical analysis from the same university in 1985. In 1995 she received her PhD from the University of Pennsylvania in the Department of Computer and Information Science.
|
| 2008/11/07 |
Speaker:
Bernard
Chazelle
Affiliation: Princeton University
Area:
Theory
Title: Natural Algorithms
Abstract: What do migrating geese, flocking cranes, bait balls of fish, prey-predator systems, and synchronously flashing fireflies have in common? All of them are instances of "natural algorithms," that is, algorithms which have been designed
by nature through evolution over millions of years.
Unlike the human-manufactured variety, natural algorithms are engineered for survival and reproduction rather than speed and efficiency, though all these considerations often overlap. I will discuss why the study of natural algorithms offer exciting challenges for computer scientists and I will present new results on bird flocking.
Biography of Speaker:
-
Bernard Chazelle is the Eugene Higgins Professor of Computer Science at
Princeton University. His research area is in Algorithms, a field believed by some to hold the promise of a scientific revolution.
|
| 2008/11/14 |
Speaker:
Michael
Geist
Affiliation: University of Ottawa
Title: Why Copyright? The Fight for Canada's Digital Future"
Abstract: In June 2008, the Canadian government introduced Bill C-61, new
copyright legislation that closely followed the U.S. Digital
Millennium Copyright Act. The public response to the bill was both
immediate and angry - tens of thousands of Canadians wrote to the
Minister and their local Members of Parliament, leading to town hall
meetings, negative press coverage, and the growing realization that
copyright was fast becoming a mainstream political and policy issue.
The "Canadian copy-fight", which includes many new advocacy groups and
the Fair Copyright for Canada Facebook group that has over 90,000
members, has attracted considerable attention from the mainstream
media, with many wondering how copyright had emerged as a contentious
policy issue. This talk will assess both the legislative proposals and
the Canadian copyfight experience in an effort to answer the oft-asked
question – "why copyright?".
Biography of Speaker:
-
Please see details at:
http://www.michaelgeist.ca/content/view/62/128/
|
| 2008/11/21 |
Speaker:
Bianca
Schroeder
Affiliation: University of Toronto
Title: Failures in the real world
Abstract: This talk highlights a new line of research, which is motivated by the fact that, with
the ever growing component count in large-scale IT systems, component failures are
quickly becoming the norm rather than the exception. Yet, virtually no data on failures
in real systems is publicly available, forcing researchers to base their work on anecdotes
and back of the envelope calculations rather than empirical data. The goal of this work is
to collect and analyze failure data from real, large-scale production systems and to exploit
the results for better system design and management.
Biography of Speaker:
-
Bianca is currently an assistant professor in the Computer Science Department
at the University of Toronto. Before joining UofT, she spent 2 years as a post-doc
at Carnegie Mellon University working with Garth Gibson. She received her
doctorate from the Computer Science Department at Carnegie Mellon University
under the direction of Mor Harchol-Balter in 2005. She is a two-time winner of
the IBM PhD fellowship and her work has won three best paper awards. Her recent
work on system reliability has been featured in articles at a number of news sites,
including Computerworld, Slashdot, PCWorld, StorageMojo and eWEEK.
|
| 2008/11/28 |
Speaker:
Jackie
Vogel
Affiliation: Department of Biology, McGill University
Title: Analysis of cytoskeletal dynamics in living cells: genome, proteome, molecules
Abstract: The fundamental unit of all living systems is the cell. Cell number and diversity depends on the process of cell division, where the genetic material (chromosomes), and the cytoplasm and organelles of a single cell is are partitioned into two daughter cells. I will describe two critical steps required for cell division; the assembly of a bipolar mitotic spindle, and its positioning relative to the geometric center of the cell and how spindle position relates to the plane through which the cell will ultimately cleave. Elegant mechanisms coordinate these two processes in space and time. We use genomic approaches to discover contextual relationships between protein structure and function, proteomic assays that reveal the dynamical behavior of protein complexes involved in cytoskeletal organization, and the analysis of spindle dynamics in living yeast cells at high temporal and spatial resolution. In this talk, I will describe our efforts to probe these spatiotemporal relationships in cells and what we have learned as a consequence of these studies.
Biography of Speaker:
-
Jackie Vogel is an Associate Professor and CIHR New Investigator in the Department of Biology at McGill University, and the Scientific Director of the Cell Imaging and Analysis Network (CIAN) at McGill. She received her PhD in Cell Biology and Biochemistry at the University of Kansas, and did her post-doctoral training at Yale University in the lab of Michael Snyder. A general theme of her research is the control of cytoskeletal dynamics during the cell cycle, using budding yeast as a model system. A particular focus is the relationship between protein structure and function, and understanding function in the context of signaling inputs; for example, how changes in a protein's phosphorylation state may act a means of spatiotemporal control of its function. Classical yeast genetics and cell biology are combined with genomic and computational biology methods, as well as high resolution imaging of living cells, to study evolutionarily conserved proteins that act in three essential cellular processes: 1) assembly and 2) positioning of the bipolar mitotic spindle, and 3) the control system that promotes high fidelity segregation of the chromosomes into daughter cells during mitosis.
|
|