# CS Department Colloquium Series

## Program Paths Simplified: Scalable Path-Sensitive Analysis without Heuristics

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.

## Precise and Fully-Automatic Verification of Container-Manipulating Programs

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.

## Differential Privacy: Recent Developments and Future Challenges

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.

## Beyond Naming: Image Understanding via Physical, Functional and Causal Relationships

Abhinav Gupta is a postdoctoral fellow at the Robotics Institute, Carnegie Mellon University working with Alexei Efros and Martial Hebert. His research is in the area of computer vision, and its applications to robotics and computer graphics. He is particularly interested in using physical, functional and causal relationships for understanding images and videos. His other research interests include exploiting relationship between language and vision, semantic image parsing, and exemplar-based models for recognition. Abhinav received his PhD in 2009 from the University of Maryland under Larry Davis. His dissertation was nominated for the ACM Doctoral Dissertation Award by the University of Maryland. Abhinav is a recipient of the ECCV Best Paper Runner-up Award(2010) and the University of Maryland Dean's Fellowship Award (2004).

## Next generation sequence characterization of complex genome structural variation

Can Alkan is currently a Senior Fellow in Professor Evan E. Eichler's group in the Department of Genome Sciences at the University of Washington. His current work includes computational prediction of human structural variation, and characterization of segmental duplications and copy-number polymorphisms using next generation sequencing data. He graduated from Bilkent University Dept. of Computer Engineering in 2000, and received his Ph.D. in Computer Science from Case Western Reserve University in 2005. During his Ph.D. he worked on the evolution of centromeric DNA, RNA-RNA interaction prediction and RNA folding problems.

## Towards a Highly Available Internet

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.

## Learning Hierarchical Generative Models

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.

## Deep Semantics from Shallow 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.

## Designing Maps to Help People

In this talk I'll present a user-centered view of map design. I'll describe some of the difficult spatial tasks people regularly face as they navigate the world and I'll draw on the long history of mapmaking to show a variety of maps that are carefully designed to address these tasks. Examples will include maps designed to help users find their way from one location to another, to aid viewers in better understanding the spatial layout of 3D environments, and to assist tourists in finding points of interest in a new city. I'll conclude with a set of open challenges for online map design.

Maneesh Agrawala is an Associate Professor in Electrical Engineering and Computer Science at the University of California, Berkeley. He received a B.S. in 1994 and a Ph.D. in 2002, both from Stanford University. Maneesh works on visualization, computer graphics and human computer interaction. His focus is on investigating how cognitive design principles can be used to improve the effectiveness of visual displays. The goals of this work are to discover the design principles and then instantiate them in both interactive and automated design tools. Recent projects based on this methodology include automated map design algorithms, systems for designing cutaway and exploded view illustrations of complex 3D objects, and interactive tools for manipulating digital photographs and video. He received an Okawa Foundation Research Grant in 2006, an Alfred P. Sloan Foundation Fellowship, an NSF CAREER award in 2007, the SIGGRAPH Significant New Researcher award in 2008 and MacArthur Foundation Fellowship in 2009.

## Formal Verification of Software Infrastructure: From Science to Engineering

I will discuss work in verifying the correctness of compilers and of low-level software like memory management and thread scheduling libraries. In each case, practical solutions have required both the "science" of choosing the right mathematical abstractions to frame the problem and the "art" of proof engineering to support code re-use and automation in proofs. Both of the examples I will discuss rely critically for their "science" pieces on higher-order logic, which allows logical quantifiers to range over functions and predicates, rather than just the basic mathematical objects supported by first-order logic. The "art" piece applies in dealing with the undecidability of the very expressive theories that are natural for these problems. My work has demonstrated the practicality of verification using expressive higher-order specifications, lowering the human cost of verification by an order of magnitude or more for several important kinds of software infrastructure.

Adam Chlipala's research applies computer theorem-proving and type systems to problems throughout the software stack, from assembly to high-level, higher-order languages. His focus is reducing the human cost of mathematically rigorous assurance about software. He finished his PhD at Berkeley in 2007, with a thesis on compiler verification for higher-order source languages. Since starting as a postdoc at Harvard, he has continued that line of work, as well as getting involved with semi-automated correctness verification for imperative programs via separation logic, first with the Ynot project, which focuses on high-level functional programs, and more recently with the Bedrock project, which deals with assembly-level reasoning. Adam also has a longstanding interest in web application programming, including the development of several domain-specific languages. Through his company Impredicative LLC, he has recently gotten involved in consulting based on his latest web language Ur/Web.