March 2011 - talks - lists.cs.princeton.edu

4:30pm Mon Mar 28 talk on highly-available Internet
by Jennifer Rexford 15 Mar '11

15 Mar '11

Department colloquium talk: Speaker: Professor Tom Anderson, U. Washington Title: Towards a Highly-Reliable Internet Date/time: 4:30-5:30pm Monday March 28 Place: CS 105 (small auditorium), with tea 4-4:30pm in the CS tea room Abstract: 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 0

Colloquium Speaker Adam Chlipala Tues March 8
by Nicole E. Wagenblast 07 Mar '11

07 Mar '11

Formal Verification of Software Infrastructure: From Science to Engineering Adam Chlipala, Harvard Tuesday, March 8, 4:30pm Computer Science 105 Is there anything to be done about the low reliability of software systems? Formal verification has already become part of standard practice in some domains where the cost of failure is especially high. Can the cost of verification be brought low enough that we can make it part of the standard development process for our servers, desktops, and so on? This talk summarizes my experience addressing this question through formal, machine-checked proof about some of the key low-level pieces of software systems. 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 U! r/Web.

1 1

Colloquium Speaker, Sepandar Kamvar, Wed. 3/9, 4:30pm
by Nicole E. Wagenblast 07 Mar '11

07 Mar '11

Search and the Social Web: Organizing the World's People and Making them Accessible and Useful Sepandar Kamvar, Stanford University Wednesday, March 9, 4:30pm Computer Science 105 In the past few years, we have seen a tremendous growth in public human communication and self-expression, through blogs, microblogs, and social networks. In addition, we are beginning to see the emergence of a social technology stack on the web, where profile and relationship information gathered by some applications can be used by other applications. This technology shift, and the cultural shift that has accompanied it, offers a great opportunity for computer scientists, artists, and sociologists to study (and organize) people at scale. In this talk I will discuss how the changing web suggests new paradigms for search and discovery. I will discuss some recent projects that use web search to study human nature, and human nature to improve web search. I will describe the underlying principles behind these projects and suggest how they might inform future work in search, data mining, and social computing. Sep Kamvar is a consulting professor of Computational and Mathematical Engineering at Stanford University. His research focuses on social computing and information retrieval. From 2003 to 2007, Sep was the head of personalization at Google. Prior to Google, he was founder and CEO of Kaltix, a personalized search company that was acquired by Google in 2003. Sep is the author of two books and over 40 technical publications and patents in the fields of search and social computing. His artwork is in the permanent collections of the Museum of Modern Art in New York and the Museum of Fine Arts in Houston, and has been exhibited in a number of other museums, including the Victoria and Albert Musem in London and the National Museum of Contemporary Art in Athens. He holds a Ph.D. in Scientific Computing and Computational Mathematics from Stanford University, and an A.B. in Chemistry from Princeton University.

1 0