 |
SSS Abstracts |
 |
|
SSS Abstracts |
|
This talk is in partial fulfillment of the speaking requirement.
This talk is in partial fulfillment of the Speaking Skills Requirement.
This talk is in partial fulfillment of the speaking requirement.
In this talk I will describe the application of predicate abstraction for verification of hardware designs given in Verilog. The two main challenges when applying predicate abstraction are: 1) discovery of suitable predicates. 2) computation of predicate abstraction in presence of large number of predicates. I will describe the techniques for addressing these problems and present encouraging experimental results.
This is joint work with Daniel Kroening, Natasha Sharygina, Edmund Clarke.
Extreme value theory attempts to make meaningful statements about the probability of as-yet-unprecedented events. A surprising result is that, under fairly mild statistical assumptions, the probability is actually well-defined. Specifically, under certain regularity conditions, the maximum of n independent and identically distributed random variables must asymptotically follow one of three "generalized extreme value" (GEV) distributions. Estimating the parameters of the GEV distribution allows one to draw inferences about its upper tail, including portions of the tail for which there is no observed data.
In the first half of this talk I will give a self-contained introduction to extreme value theory, including a sketch of the proof of its main theorem. I will then present the "max k-armed bandit problem", a previously-studied problem that is motivated by extreme value theory and has applications to combinatorial optimization. The problem asks: given k "payoff" distributions, each a GEV distribution with unknown parameters, how can we sample the distributions so as to maximize the expected maximum payoff obtained after n samples? I will outline an asymptotically optimal algorithm for the problem. Specifically, I will describe a strategy that obtains expected maximum payoff within o(1) of that obtained by a strategy that plays optimally knowing the true parameters of each distribution.
Joint work with Steve Smith. This talk is in partial fulfillment of the speaking requirement.
Finding Equilibria in Large Sequential Games of Imperfect Information
Friday, September 23rd, 2005 from 12-1 pm in NSH 3305.
Presented by Andrew G. Gilpin, CSD
Computing an equilibrium of an extensive form game of imperfect information is a fundamental problem in computational game theory, but current techniques do not scale to large games. To address this, we introduce the ordered game isomorphism and the related ordered game isomorphic abstraction transformation. For an n-player sequential game of imperfect information with observable actions and an ordered signal space, we prove that any Nash equilibrium in an abstracted smaller game, obtained by one or more applications of the transformation, can be easily converted into a Nash equilibrium in the original game. We present an efficient algorithm, GameShrink, which automatically and exhaustively abstracts the game. Using GameShrink, we find an equilibrium to a poker game that is over four orders of magnitude larger than the largest poker game solved previously. To address even larger games, we introduce approximation methods that do not preserve equilibrium, but nevertheless yield (ex post) provably close-to-optimal strategies.
This is joint work with Tuomas Sandholm.
This talk is in partial fulfillment of the speaking requirement.
Managing Scale and Dynamism in Claytronics
Friday, September 30th, 2005 from 12-1 pm in NSH 1507.
Presented by Ben Rister, CSD
The Claytronics project aims to use extremely large numbers of extremely small robots to dynamically form and animate actual 3D physical objects, forming an environment we call "synthetic reality." The challenging task of efficiently coordinating the actions of millions of these robots is critical to the effective functioning of the system, and is further complicated by the constant changes both in the internal state of the system and influences from the environment.
We propose the use of a self-organizing hierarchical runtime framework that provides automatic handling of these issues for the logical system processes, such as balance, motion planning, and sensor aggregation. In this talk, I will provide an overview of the structure and function of the Claytronics hierarchy system. No previous knowledge of Claytronics, networking, or related sensor network systems is presumed.
This is joint work with Phillip B. Gibbons, Srinivasan Seshan, Padmanabhan Pillai, Todd C. Mowry, and Seth Copen Goldstein.
This talk is in partial fulfillment of the speaking requirement.
What Is Modal Logic and What Is It Good for?
Friday, October 7th, 2005 from 12-1 pm in NSH 1507.
Presented by Tom Murphy, CSD
Modal logic is the name for a family of logics that share a common feature: rather than reasoning about a single notion of "truth," they allow for simultaneous reasoning about truth from multiple perspectives. Modal logics are therefore useful for reasoning about systems in which there is more than one participant (e.g., security systems), more than one moment in time, or more than one place of interest (e.g., distributed systems). Moreover, since logics can be naturally transformed into programming languages via the Curry-Howard isomorphism, modal logic forms a rich source of languages that directly express concepts like spatial distribution.
This talk is intended as an introduction to modal logic for a general computer science audience. The speaker's own work on a modal distributed programming language will be used as a motivating example.
This talk is in partial fulfillment of the speaking requirement.
ViVo: Visual Vocabulary Construction for Mining Biomedical Images
Friday, October 14th, 2005 from 12-1 pm in NSH 1507.
Presented by Jia Yu (Tim) Pan, CSD
Given a large collection of medical images of several conditions and treatments, how can we succinctly describe the characteristics of each setting? For example, given a large collection of retinal images from several different experimental conditions (normal, detached, reattached, etc.), how can data mining help biologists focus on the important regions in the images or on the differences between different experimental conditions?
If the images were text documents, we could find the main terms and concepts for each condition by existing IR methods (e.g., tf/idf and LSI). We propose something analogous, but for the much more challenging case of an image collection: We propose to automatically develop a visual vocabulary by breaking images into n*n tiles and deriving key tiles ("ViVos") for each image and condition. We experiment with numerous domain-independent ways of extracting features from tiles (color histograms, textures, etc.), and several ways of choosing characteristic tiles (PCA, ICA).
We perform experiments on two disparate biomedical datasets. The quantitative measure of success is classification accuracy: Our "ViVos" achieve excellent classification accuracy (up to 83% for a nine-class problem for the cat retinal images). More importantly, qualitatively, our "ViVos" do an excellent job as "visual vocabulary terms": they have biological meaning, as corroborated by domain experts; they help spot characteristic regions of images, exactly like text vocabulary terms do for documents; and they highlight the differences between pairs of images.
This is joint work with Arnab Bhattacharya, Vebjorn Ljosa, Mark R. Verardo, Hyungjeong Yang, Christos Faloutsos and Ambuj K. Singh.
This talk is in partial fulfillment of the speaking requirement.
A Monadic Analysis of Information Flow Security with Mutable State
Friday, October 21st, 2005 from 12-1 pm in NSH 1507.
Presented by Aleksey Kliger, CSD
Information flow through a program is secure if users' high-security inputs do not affect low-security behavior of a program, that is, if an attacker cannot learn any secrets by observing public outputs. Type systems have been used to guarantee secure information flow: a language is designed so that only secure programs are well-typed. We illustrate the principle with one such language based on monads --- types that are usually used to indicate the presence of side-effects such as input/output, mutation of a memory store, exceptions, etc. We show that monads can also be used to reason about secure information flow. Prior secure languages tag all values with security levels. In contrast, in our language only mutable store locations are tagged, and monads classify computations according to the security levels of the locations they access. Starting from a purely functional language, ours is a lighter-weight extension that simplifies the task of reasoning about programs.
In this talk, I will present a mini-review, suitable for a general computer science audience, of how monads are used for including effects such as I/O and mutation in purely functional languages. I will then show how we can further refine monadic types into a form suitable for reasoning about security.
This is joint work with Karl Crary and Frank Pfenning.
This talk is in partial fulfillment of the speaking requirement.
Reconstructing Evolutionary Trees Optimally
Friday, October 28th, 2005 from 12-1 pm in NSH 1507.
Presented by Srinath Sridhar, CSD
Evolutionary trees are fundamental to our understanding of the mechanisms of nature. They have been used to solve many important problems, such as tracing the evolution of diverse species and tracking historical human migration patterns. Over the last decade, there has been a tremendous amount of research in the area bringing together theoreticians and biologists. In this talk, I will focus on reconstructing evolutionary trees optimally by finding the smallest (most parsimonious) tree for an input set of DNA sequences. We will consider an important special case of the problem that is equivalent to finding the minimum Steiner tree in Hamming space. In this talk, I will formulate the problem, prove a simple lower bound on the size of the smallest tree and outline an algorithm to reconstruct it. Finally, I will show experimental results using DNA from humans (multiple ethnic groups) and other primates.
Scalable Shape Sculpting via Hole Motion: Motion Planning for Claytronics
Friday, November 4th, 2005 from 12-1 pm in NSH 1507.
Presented by Mike De Rosa, CSD
The Claytronics project aims to use massive numbers of extremely small modular robots as display, telepresence, and manipulation devices. One of the major challenges associated with this project is motion planning for such ensembles. Planning the coordinated motion of thousands to millions of catoms is impossible with current motion planning techniques. This talk will present an initial design and evaluation of an algorithm capable of solving at least part of this problem. The presented algorithm is capable of performing approximate, 2D motion planning for arbitrarily large ensembles of catoms, without the use of broadcast channels or gradient fields. No prior knowledge of the Claytronics project, robotics, or motion planning is presumed.
New Streaming Algorithms for Fast Detection of Superspreaders
Friday, November 11th, 2005 from 12-1 pm in NSH 1507.
Presented by Shobha Venkataraman, CSD
High-speed monitoring of Internet traffic is an important and challenging problem, with applications to real-time attack detection and mitigation, traffic engineering, etc. However, packet-level monitoring requires fast streaming algorithms that use very little memory and little communication among collaborating network monitoring points. In this paper, we consider the problem of detecting superspreaders, which are sources that connect to a large number of distinct destinations. We propose new streaming algorithms for detecting superspreaders and prove guarantees on their accuracy and memory requirements. We also show experimental results on real network traces. Our algorithms are substantially more efficient (both theoretically and experimentally) than previous approaches. We also extend our algorithms to identify superspreaders in a distributed setting, with sliding windows, and when deletions are allowed in the stream. More generally, our algorithms are applicable to any problem that can be formulated as follows: given a stream of $(x,y)$ pairs, find all the $x$''s that are paired with a large number of distinct $y$''s. This paper discusses the applications of this general problem and, for concreteness, focuses on the superspreader problem. Joint work with Dawn Song, Phillip Gibbons and Avrim Blum.
Predicate Abstraction and Refinement for Verifying Hardware Designs
Friday, November 18th, 2005 from 12-1 pm in WeH 4625.
Presented by Himanshu Jain, CSD
Verification techniques such as model-checking when applied to large industrial circuits suffer from the state-space explosion problem. A major technique to address this problem is abstraction. Abstraction involves the generation of simpler models by focusing on the characteristics of a system that are essential for checking the property of interest. Predicate abstraction has been used successfully for verifying the control related properties of large software programs.
This talk is in partial fulfillment of the speaking requirement.
Extreme Value Theory and the Max k-Armed Bandit Problem
Friday, December 9th, 2005 from 12-1 pm in NSH 1507.
Presented by Matt Streeter, CSD
The National Climatic Data Center has recorded the monthly precipitation in Pittsburgh since 1895. Given this data, what can we say about the probability that the precipitation this January will exceed some high threshold, say 10 inches? (The current record of 8.2 inches was set in 1937.) Is the question even well-posed?
Web contact: sss+www@cs