- talks - lists.cs.princeton.edu

Colloquium Speaker Isil Dillig Tuesday April 5
by Nicole E. Wagenblast 04 Apr '11

04 Apr '11

Precise and Fully-Automatic Verification of Container-Manipulating Programs Isil Dillig, Stanford University Tuesday April 5, 4:30pm Computer Science 105 One of the key challenges in automated software verification is obtaining a conservative, yet sufficiently precise understanding of the contents of data structures in the heap. A particularly important and widely-used class of heap data structures is containers, which support operations such as inserting, retrieving, removing, and iterating over elements. Examples of containers include arrays, lists, vectors, sets, maps, stacks, queues, etc. In this talk, I will describe a sound, precise, scalable, and fully-automatic static analysis technique for reasoning about the contents of container data structures. This technique is capable of tracking position-value and key-value correlations, supports reasoning about arbitrary nestings of these data structures, and integrates container reasoning directly into a heap analysis, allowing, for the first time, the verification of complex programs that manipulate heap objects through container data structures. More specifically, I will describe a symbolic heap abstraction that augments a graph representation of the heap with logical formulas and that reduces some of the difficulty of heap reasoning to standard logic operations, such as existential quantifier elimination and satisfiability. I will present experimental results demonstrating that our technique is very useful for verifying memory safety in complex heap- and container-manipulating C and C++ programs that use arrays and other container data structures from the STL and QT libraries. Isil Dillig is a PhD candidate at the Computer Science Department at Stanford University, advised by Prof. Alex Aiken. Her research interests include software verification, static analysis, and constraint solving. Isil received her undergraduate degree from Stanford in 2006, with a major in computer science with honors and distinction. She is the recipient of Frederick Emmons Terman Engineering Scholastic Award at Stanford, as well as the recipient of Forbes School of Engineering and Stanford Graduate Fellowships.

1 1

Colloquium Speaker, Thomas Dillig, Monday April 4
by Nicole E. Wagenblast 01 Apr '11

01 Apr '11

Program Paths Simplified: Scalable Path-Sensitive Analysis without Heuristics Thomas Dillig, Stanford University Monday, April 4, 4:30pm Computer Science 105 A path-sensitive static analysis considers each possible execution path through a program separately, potentially yielding much more precise results than an analysis that makes fewer distinctions among paths. While precise path-sensitive reasoning is known to be necessary to prove many interesting facts about programs, fully path-sensitive analyses have not scaled well because standard representations of program paths quickly grow out of control. In this talk, I will describe two techniques that allow path-sensitive program analyses to scale. I will first introduce on-line constraint simplification, which eliminates redundant subparts of logical formulas used to distinguish execution paths. In practice, the formulas used to describe program paths are highly redundant; thus, techniques for keeping path formulas concise can have a dramatic impact on analysis scalability. A second, complementary technique reduces formula size even further: Because static analyses are typically only interested in answering may (i.e., satisfiability) and must (i.e., validity) queries, I will show how to extract from the original path formulas a pair of satisfiabilty- and validity-preserving formulas that contain many fewer variables and that are as good as the original path formula for answering may and must queries about the program. I will demonstrate that these techniques allow a fully path-sensitive analysis to scale to very large, multi-million line programs for the first time. Thomas Dillig is a PhD candidate at Stanford University. Thomas obtained his undergraduate degree in computer science from Stanford University in 2006 with distinction and honors. His main research interests are program verification, programming languages and constraint solving.

1 0

Colloquium Speaker, Percy Liang, Wed. April 6
by Nicole E. Wagenblast 31 Mar '11

31 Mar '11

Deep Semantics from Shallow Supervision Percy Liang, UC Berkeley Wednesday, April 6, 4:30pm Computer Science 105 What is the total population of the ten largest capitals in the US? Building a system to answer free-form questions such as this requires modeling the deep semantics of language. But to develop practical, scalable systems, we want to avoid the costly manual annotation of these deep semantic structures and instead learn from just surface-level supervision, e.g., question/answer pairs. To this end, we develop a new tree-based semantic representation which has favorable linguistic and computational properties, along with an algorithm that induces this hidden representation. Using our approach, we obtain significantly higher accuracy on the task of question answering compared to existing state-of-the-art methods, despite using less supervision. Percy Liang obtained a B.S. (2004) and an M.S. (2005) from MIT and is now completing his Ph.D. at UC Berkeley with Michael Jordan and Dan Klein. The general theme of his research, which spans machine learning and natural language processing, is learning richly-structured statistical models from limited supervision. He has won a best student paper at the International Conference on Machine Learning in 2008, received the NSF, GAANN, and NDSEG fellowships, and is also a 2010 Siebel Scholar.

1 0

Q Xi preFPO
by Melissa Lawson 31 Mar '11

31 Mar '11

Qian Xi will present her preFPO on Tuesday April 5 at 1PM in Room 301 (note room). The members of her committee are David Walker, advisor; Andrew Appel and Yitzhak Mandelbaum (AT&T), readers; Brian Kernighan and Andrea LaPaugh, nonreaders. Everyone is invited to attend her talk. Her abstract follows below. Title: Generation of Data Processing Tools for Context-free and Context Dependent Grammars Abstract: An ad hoc data format is any nonstandard, semi-structured data format for which robust data processing tools are not easily available. Ad hoc data exists in many domains, but processing it is challenging. The goal of this research is to find a generic, reliable and efficient method to extract the structural information from ad hoc data files, which is the key step to complete before generating auxiliary data processing tools, such as parsers, pretty printers, query engines, XML converters etc. In this dissertation, we first focus on the context-free grammars in ad hoc data sources. We design a markup language called Anne that programmers can use to annotate raw text with a set of grammatical directives. The Anne system then uses a combination of user annotations and the raw data itself to extract a context-free grammar from which the system further generates a PADS description, a Yakker description, and an XML representation of the data. To thoroughly understand Anne, we formalize a semantic theory to capture the core features of the language. This semantic theory includes the editing process, which translates a raw, unannotated document into an annotated one, and the grammar extraction process, which generates a context-free grammar from the annotated document. When reasoning about the relationship between the raw data and the generated grammar, we also find an interesting connection to the field of classic relevance logic. This relevance analysis allows us to prove important theorems concerning the expressiveness of the language. We implement the system and conduct two major experiments measuring the amount of effort needed to annotate documents and the quality of the generated grammars. Then we extend the coverage of Anne to context dependent grammars by adding new features in the syntax and semantic rules of the formalization, including variable bindings, data-dependent constraint, and transformations. We demonstrate the relevance analysis is a robust theory by proving all the principle theorems still hold after this extension. Our experience of using dependent parser generator shows that arbitrary dependent grammars can be costly to parse, and thus we are motivated to build more efficient parsers. We apply an analysis of dependent grammars to find particular subparts that do not rely on general dependent parsing and can therefore use conventional optimization techniques. We give formal definitions of the analysis and use it to guide implementation. The results of the implementation demonstrate that the efficiency of parsing is improved by the analysis.

1 0

Phillipa Gill's talk on March 29 at 12:30PM
by Michael Schapira 29 Mar '11

29 Mar '11

Talk details below. Please send me an e-mail if you're interested in meeting with the speaker. Let the Market Drive Deployment: A Strategy for Transitioning to BGP Security Phillipa Gill, University of Toronto Tuesday, March 29 Talk at 12:30-1:30PM and food at 12:00PM Computer Science 402 With a cryptographic root-of-trust for Internet routing (RPKI) on the horizon, we can finally start planning the deployment of one of the secure interdomain routing protocols proposed over a decade ago (Secure BGP, secure origin BGP). However, if experience with IPv6 is any indicator, this will be no easy task. Security concerns alone seem unlikely to provide sufficient local incentive to drive the deployment process forward. Worse yet, the security benefits provided by the S*BGP protocols do not even kick in until a large number of ASes have deployed them. Instead, we appeal to ISPs' interest in increasing revenue-generating traffic. We propose a strategy that governments and industry groups can use to harness ISPs' local business objectives and drive global S*BGP deployment. We evaluate our deployment strategy using theoretical analysis and large-scale simulations on empirical data. Our results give evidence that the market dynamics created by our proposal can transition the majority of the Internet to S*BGP. Joint work with Sharon Goldberg and Michael Schapira

1 3

Colloquium Speaker, Guy Rothblum, Wed March 30
by Nicole E. Wagenblast 28 Mar '11

28 Mar '11

Differential Privacy: Recent Developments and Future Challenges Guy Rothblum, Princeton University Wednesday March 30, 4:30pm Computer Science Department, 105 Consider a database of sensitive information about a set of participants. Statistical analysis of the data may yield valuable results, but it also poses serious threats to participants' privacy. A successful research program has, in the last few years, attempted to address these conflicting concerns. This line of work formulated the rigorous privacy guarantee of differential privacy [Dwork McSherry Nissim and Smith '06] and showed that, in some cases, data analyses can provide accurate answers while protecting participants' privacy. I will review some of this past work, and then introduce new general-purpose tools for privacy preserving data analysis: 1. A "multiplicative weights" framework for fast and accurate differentially private algorithms. 2. New privacy analysis techniques, including robust privacy guarantees for differential privacy under composition. We will use these tools to show that differential privacy permits surprisingly rich and accurate data analyses. I will then highlight some of the intriguing challenges that remain open for future work in this field. No prior knowledge will be assumed. Guy Rothblum is a postdoctoral research fellow at Princeton University, supported by a Computing Innovation Fellowship. He completed his Ph.D. in computer science at MIT, advised by Shafi Goldwasser. His research interests are in theoretical computer science, especially privacy-preserving data analysis, cryptography and complexity theory.

1 1

Y Zhang preFPO
by Melissa Lawson 25 Mar '11

25 Mar '11

Yun Zhang will present her preFPO on Friday April 1 at 2PM in Room 301. The members of her committee are: David August, advisor; David Walker and Scott Mahlke (Michigan), readers; Doug Clark and Jen Rexford, nonreaders. Everyone is invited to attend her talk. Her abstract follows below. ----------------------------------- Title: Decouple Redundant Execution for Transient Fault Tolerance Abstract: As semiconductor technology continues to scale, transient faults are emerging as a critical reliability concern in modern microprocessors. The increasing density of transistors on chip, reduced noise margin of each transistor, and voltage scaling are making chips more susceptible to transient faults than ever. Both hardware or software solutions have been proposed for transient fault detection and recovery. The hardware approach adds redundant hardware modules to the system, thus requiring extra chip area as well as hardware design and veri?cation cost. In addition, the scope and mechanism of fault tolerance are hardwired at design time, which could be suboptimal depending on deployment environment. Software-only solutions do not require any specialized hardware extensions and are more ?exible. However, even the best-performing software-only fault tolerance techniques have signi?cant performance cost. The overhead of prior work comes from doubled register usage, frequent inter-core communication, or barrier synchronizations. These factors prevent prior techniques from being adopted widely. To address these problems, this dissertation proposes a software-only decoupled program execution framework for fault tolerance. A compiler automatically transforms a program into its corresponding redundant execution version. Only the values that escape the scope of replication may affect the externally behavior of the program and therefore need to be veri?ed for correctness. At program runtime, the program speculates that transient fault detection code never detects a fault, thus allowing decoupled execution of program code, transient fault detection, I/O operations and system calls. A comprehensive misspeculation detection and recovery framework is also described for programs to detect a transient fault and recover from it with low runtime cost. The prototype of this framework was implemented as a set of automatic compiler transformations and evaluated on a commodity multi-core system. The evaluation demonstrated that with this framework, transient fault tolerance can achieve best-in-class performance, high fault coverage, and fast recovery with no hardware module involved.

1 0

Colloquium Speaker, Thomas Anderson, Mon. March 28
by Nicole E. Wagenblast 25 Mar '11

25 Mar '11

Towards a Highly Available Internet Thomas Anderson, University of Washington Monday March 28, 4:30pm Computer Science 105 Internet availability -- the ability for any two nodes in the Internet to communicate — is essential to being able to use the Internet for delivery critical applications such as real-time health monitoring and response. Despite massive investment by ISPs worldwide, Internet availability remains poor, with literally hundreds of outages occurring daily, even in North America and Europe. Some have suggested that addressing this problem requires a complete redesign of the Internet, but in this talk I will argue that considerable progress can be made with a small set of backwardly compatible changes to the existing Internet protocols. We take a two-pronged approach. Many outages occur on a fine-grained time scale due to the convergence properties of BGP, the Internet’s interdomain routing system. We describe a novel set of additions to BGP that retains its structural properties, but applies lessons from fault tolerant distributed systems research to radically improve its availability. Other outages are longer-lasting and occur due to complex interactions between router failures and router misconfiguration. I will describe some ongoing work to build an automated system to quickly localize and repair these types of problems. Thomas Anderson is the Robert E. Dinning Professor of Computer Science and Engineering at the University of Washington. His research interests span all aspects of building practical, robust, and efficient computer systems, including distributed systems, operating systems, computer networks, multiprocessors, and security. He is an ACM Fellow, winner of the ACM SIGOPS Mark Weiser Award, winner of the IEEE Bennett Prize, past program chair of SIGCOMM and SOSP, and he has co-authored seventeen award papers.

1 1

Colloquium Speaker- Ruslan Salakhutdinov Thurs March 23
by Nicole E. Wagenblast 22 Mar '11

22 Mar '11

Learning Hierarchical Generative Models Ruslan Salakhutdinov, Massachusetts Institute of Technology Thursday, March 23, 4:30pm Computer Science 105 Building intelligent systems that are capable of extracting meaningful representations from high-dimensional data lies at the core of solving many Artificial Intelligence tasks, including visual object recognition, information retrieval, speech perception, and language understanding. My research aims to discover such representations by learning rich generative models which contain deep hierarchical structure and which support inferences at multiple levels. In this talk, I will introduce a broad class of probabilistic generative models called Deep Boltzmann Machines (DBMs), and a new algorithm for learning these models that uses variational methods and Markov chain Monte Carlo. I will show that DBMs can learn useful hierarchical representations from large volumes of high-dimensional data, and that they can be successfully applied in many domains, including information retrieval, object recognition, and nonlinear dimensionality reduction. I will then describe a new class of more complex probabilistic graphical models that combine Deep Boltzmann Machines with structured hierarchical Bayesian models. I will show how these models can learn a deep hierarchical structure for sharing knowledge across hundreds of visual categories, which allows accurate learning of novel visual concepts from few examples. Ruslan Salakhutdinov received his PhD in computer science from the University of Toronto in 2009, and he is now a postdoctoral associate at CSAIL and the Department of Brain and Cognitive Sciences at MIT. His research interests lie in machine learning, computational statistics, and large-scale optimization. He is the recipient of the NSERC Postdoctoral Fellowship and Canada Graduate Scholarship.

2 3

Colloquium Speaker Abhinav Gupta March 23
by Nicole E. Wagenblast 21 Mar '11

21 Mar '11

Beyond Naming: Image Understanding via Physical, Functional and Causal Relationships Abhinav Gupta, Carnegie Mellon University Wednesday, March 23, 4:30pm Computer Science 105 What does it mean to "understand" an image? One popular answer is simply naming the objects seen in the image. During the last decade most computer vision researchers have focused on this "object naming" problem. While there has been great progress in detecting things like "cars" and "people", such a level of understanding still cannot answer even basic questions about an image such as "What is the geometric structure of the scene?", "Where in the image can I walk?" or "What is going to happen next?". In this talk, I will show that it is beneficial to go beyond mere object naming and harness relationships between objects for image understanding. These relationships can provide crucial high-level constraints to help construct a globally-consistent model of the scene, as well as allow for powerful ways of understanding and interpreting the underlying image. Specifically, I will present image and video understanding systems that incorporate: (1) physical relationships between objects via a qualitative 3D volumetric representation; (2) functional relationships between objects and actions via data-driven physical interactions; and (3) causal relationships between actions via a storyline representation. I will demonstrate the importance of these relationships on a diverse set of real-world images and videos.

1 1