- talks - lists.cs.princeton.edu

Colloquium Speaker, Mark Braverman, Tuesday Feb 15
by Nicole E. Wagenblast 14 Feb '11

14 Feb '11

Average-case solutions to hard problems Mark Braverman , University of Toronto Tuesday, February 15, 2011- 4:30pm Computer Science, 105 Many important computational problems are affected by various computational barriers that make them intractable in the worst case. In spite of this, it is often possible to get around these barriers and produce useful, if not optimal solutions for most instances of the problem. I will use several examples from my work to illustrate how considering an average or a typical case of the problem can be used to produce useful algorithms and mechanisms. The first example deals with the problem of assigning medical graduates to residency programs in the presence of married couples. The problem of finding a stable matching between residency programs and doctors without couples is solved by the famous Gale-Shapley algorithm. In the presence of couples, such a matching may not exist, and it is NP-hard to determine whether it exists or not. Still, in a large random market we show how to find a good stable outcome with high probability. The second example deals with aggregating noisy comparison signals, such as sport competition results, into a ranking most consistent with the observed signals. The worst-case version of the problem, known as the Minimum Feedback Arcset problem is NP-hard. We give an efficient algorithm for the average-case version of the problem.

1 0

Physics Colloquium-"Computer vision and optics in the study of fine art"
by Andrew W. Appel 04 Feb '11

04 Feb '11

1 0

S Jafarpour preFPO
by Melissa Lawson 04 Feb '11

04 Feb '11

Sina Jafarpour will present his preFPO on Friday February 11 at 2PM in Room 402. The members of his committee are: Robert Calderbank; advisor, Rob Schapire and Ingrid Daubechies (Duke); readers, and David Blei and Amit Singer (PACM and Math); non-readers. Everyone is invited to attend his talk. His abstract follows below. --------------------------------------------- Title: Deterministic Compressed Sensing The central goal of compressed sensing is to capture attributes of a signal using very few measurements. The initial publications by Donoho and by Candes and Tao have been followed by applications to image compression, data streaming, medical signal processing, digital communication and many others. The emphasis has been on random sensing but the limitations of this framework include performance guarantees, storage requirements, and computational cost. This talk will describe two deterministic alternatives. The first is based on expander graphs. We show that by reformulating signal reconstruction as a zero-sum game we can efficiently recover any sparse vector. We also demonstrate resilience to Poisson noise. The second is based on error correcting codes. We show that deterministic sensing matrices based on second order Reed Muller codes optimize average case performance. We also describe a very simple algorithm, one-step thresholding, that succeeds where more sophisticated algorithms, developed in the context of random sensing, fail completely. The talk is based on joint work with Waheed Bajwa, Robert Calderbank, Volkan Cevher, Marco Duarte, Zachary Harmany, Stephen Howard, Maxim Raginsky, Rob Schapire, and Rebecca Willett.

1 0

M Carroll FPO
by Melissa Lawson 20 Jan '11

20 Jan '11

Melissa Carroll will present her FPO on Wednesday January 26 at 2:30PM in Room 402. The members of her committee are: Rob Schapire, advisor; Ken Norman (PSY) and Irina Rish (IBM), readers; David Blei and Peter Ramadge (ELE), nonreaders. A copy of her thesis, "FMRI "Mind Readers": Sparsity, Spatial Structure, and Reliability", is on display in Room 310. Everyone is invited to attend her talk.

1 0

G Stewart General Exam
by Melissa Lawson 12 Jan '11

12 Jan '11

Gordon Stewart will present his research seminar/general exam on Wednesday January 19 at 2PM in Room 402. The members of his committee are: Andrew Appel 9advisor), David Walker, and David August. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. ----------------------------------- Abstract ======== Soundness proofs of program logics such as Hoare logics and type systems are often made easier by decorating the operational semantics with information that is useful in the proof. However, modifying the operational semantics to carry around such information can make it more difficult to show that the operational semantics corresponds to what actually occurs on a real machine. In this work we present a program logic framework targeting operational semantics in Curry-style--that is, operational semantics without proof decora- tions such as separation algebras, share models, and step indexes. Although we target Curry-style operational semantics, our framework permits local reason- ing via the frame rule and retains expressive assertions in the program logic. Soundness of the program logic is derived mechanically from simple properties of primitive commands and expressions. We demonstrate our framework by deriving a separation logic for the model of a core imperative programming language with external function calls. We also apply our framework in a more realistic setting in the soundness proof of a separation logic for CompCert's Cminor. Our proofs are machine-checked in Coq. Research Papers =============== [Appel and Blazy 2007] A. W. Appel and S. Blazy. Separation logic for small- step Cminor. In 20th Intl Conference on Theorem Proving in Higher-Order Logics, pages 5-21, 2007. [Calcagno et al. 2007] C. Calcagno, P. W. O'Hearn, and H. Yang. Local ac- tion and abstract separation logic. In LICS'07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, pages 366-378, 2007. ISBN 0-7695-2908-9. doi: http://dx.doi.org/10.1109/LICS.2007.30. [Dockins et al. 2009] R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation algebras and share accounting. In The 7th Asian Symposium on Programming Languages and Systems. Springer ENTCS, 2009. URL http://msl.cs.princeton.edu/fresh-sa.pdf. [Lahiri 2008] S. Lahiri, S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In POPL'08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008. [Lerner 2003] S. Lerner, T. Millstein, and C. Chambers. Automatically Proving the Correctness of Compiler Optimizations. In PLDI'03: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2003. [Leroy 2009] X. Leroy. Formal verification of a realistic compiler. Communica- tions of the ACM, 52(7):107-115, 2009. [Leroy and Blazy 2008] X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. J. Au- tomated Reasoning, 41(1):1-31, 2008. [Necula 1997] G. Necula. Proof-Carrying Code. In POPL'97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997. [Parkinson 2010] M. Parkinson. The next 700 separation logics. In G. Leavens, P. O'Hearn, and S. Rajamani, editors, Verified Software: Theories, Tools, Experiments, volume 6217 of Lecture Notes in Computer Science, pages 169-182. Springer Berlin / Heidelberg, 2010. [Parkinson et al. 2006] M. Parkinson, R. Bornat, and C. Calcagno. Variables as resource in Hoare logics. Proc. of 21st Annual IEEE Symp. on Logic in Computer Science, 0:137-146, 2006. ISSN 1043-6871. [Reynolds 2002] J.C. Reynolds. Separation Logic: a Logic for Shared Mutable Data Structures. In LICS'02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 55 - 74, 2002. Textbooks ========= [Pierce 2002] B. Pierce. Types and Programming Languages. 2002. [Winskell 1993] G. Winskell. The Formal Semantics of Programming Languages (Chapters 1-7). 1993.

1 0

W Josephson FPO
by Melissa Lawson 04 Jan '11

04 Jan '11

William Josephson will present his FPO on Tuesday January 11 at 2:30 PM in Room 302 (note Room!) The members of his committee are: Kai Li, advisor; Jen Rexford and Brian Kernighan, readers; Mike Freedman and Doug Clark, nonreaders. A copy of his thesis, "A Direct-Access File System for a New Generation of Flash Memory", is on display in Room 310. Everyone is invited to attend his talk.

1 0

S Ihm preFPO
by Melissa Lawson 13 Dec '10

13 Dec '10

Sunghwan Ihm will present his preFPO on Friday December 17 at 2PM in Room 401 (note room!) The members of his committee are: Vivek Pai, advisor; Jen Rexford and Larry Peterson, readers; Mike Freedman and Andrea LaPaugh, nonreaders. Everyone is invited to attend his talk. His abstract follows below. ---------------------- Title: Understanding and Improving Modern Web Traffic Caching As Web sites move from relatively static displays of simple pages to rich media applications with heavy client-side interaction, the nature of the resulting Web traffic changes as well. At the same time, Web traffic also increases due to the popularity of social networking, video streaming, file-hosting sites, and consolidation of existing applications to the Web. Understanding the nature of these changes grows more difficult without a better characterization of the underlying traffic, which is necessary to improve response time, analyze caching effectiveness, and to design intermediary systems, such as firewalls, security analyzers, and reporting/management systems. Unfortunately, while the Web has been studied heavily in the past, we still have little understanding of today's Web - what has been changed, and what we can do better about it. In this thesis, we revisit the previous issues with today's Web, focusing on characterizing traffic and developing a new caching technique which outperforms previous approaches. Specifically, we analyze five years (2006-2010) of real Web traffic from a globally-distributed proxy system, which captures the browsing behavior of over 50,000 users. Using this data set, we also develop a new page detection algorithm that is better suited for the modern Web page interactions, and investigate the redundancy of this traffic, using both traditional object-level caching as well as content-based approaches. Among many findings, we observe a huge potential benefit of the content-based caching approach in today's Web - the byte hit rate is almost twice larger than that of the traditional object-level caching approach. Motivated by the promising benefit of content-based caching, we also develop Wanax, a scalable and flexible wide-area network (WAN) accelerator. It uses a novel multiresolution chunking (MRC) scheme that provides high compression rates and high disk performance for a variety of content, while using much less memory than existing approaches. Wanax exploits the design of MRC to perform intelligent load shedding to maximize throughput even when running on resource-limited shared platforms. Finally, Wanax exploits mesh network environments, instead of just the star topologies common in enterprise branch offices.

1 0

Colloquium Speaker Monday 12/13- Dan Morris
by Nicole E. Wagenblast 10 Dec '10

10 Dec '10

What Human-Computer Interaction and Medicine Can Offer Each Other Dan Morris, Microsoft Research Monday, December 13, 2010, 4:30pm Computer Science Small Auditorium, CS105 Our work sits at the intersection of Human-Computer Interaction (HCI) and Medicine. That means that 50% of what we do is applying HCI methodology to problems in medicine, so we can spend the other 50% of our time "borrowing" technologies from medicine and applying them to HCI. This talk, therefore, will focus on two topics: (a) patient-friendly medical information displays, and (b) sensing physiological signals for computer input. In the first part of the talk, I'll present our work on making electronic medical record data more useful to patients, work that spans both qualitative research ("what *should* patient interfaces look like?") and technology research ("how do we actually build that without asking doctors to spend hours explaining everything to us?"). In the second part of the talk, I'll present our work on using sensing techniques that medical science has known about for centuries (like measuring electrical muscle activity, and measuring body acoustics) to build new computer input systems. This part of the talk will have cool videos, so bring your popcorn. Dan Morris is a researcher in the Computational User Experiences group at Microsoft Research; he is interested in novel input devices, patient-facing medical technology, and computer support for music and creativity. Dan studied neurobiology as an undergraduate at Brown, and developed brain-computer interfaces: first at Brown, and later as an engineer at Cyberkinetics, Inc. His PhD thesis at Stanford focused on haptic rendering and physical simulation for virtual surgery, and his work since coming to MSR (in 2006) has included using physiological signals for input systems, designing patient-friendly information displays for hospitals, and generating automatic accompaniment for sung melodies. If you would like to see both his research talents and his (lack of) performance talents showcased in one four-minute masterpiece, search for "Microsoft Songsmith Commercial".

1 1

M Burns FPO
by Melissa Lawson 08 Dec '10

08 Dec '10

Michael Burns will present his FPO on Tuesday December 14 at 10AM in Room 402. The members of his committee are: Adam Finkelstein, advisor; Szymon Rusinkiewicz and Doug DeCarlo (Rutgers), readers; Perry Cook and Tom Funkhouser, nonreaders. A copy of his thesis, "Efficient and Comprehensible Visualization of Complex 3-D Scenes", is on display in Room 310. Everyone is invited to attend his talk.

1 0

colloquium speaker Wed. 12/8- Xiaowei Yang
by Nicole E. Wagenblast 07 Dec '10

07 Dec '10

Bootstrapping Accountability in the Internet We Have Xiaowei Yang, Duke University Wednesday December 8, 4:30pm Computer Science Building small auditorium, CS105 The lack of accountability makes the Internet vulnerable to numerous attacks, including prefix hijacking, route forgery, source address spoofing, and DoS flooding attacks. This work takes a "dirty-slate" approach to bring accountability to the present Internet with low-cost and deployable enhancements. In this talk, we will present IPA, a network architecture that uses the readily available top-level DNSSEC infrastructure and BGP to bootstrap accountability. We integrate IPA with a suite of security building blocks to combat various network-layer attacks. Our evaluation shows that IPA introduces modest overhead, is gradually deployable , and offers security incentives to early adopters. Xiaowei Yang is an assistant professor in the Department of Computer Science at Duke University. Before joining Duke, she was an assistant professor in the Department of Computer Science at the University of California at Irvine. She received a PhD in Computer Science from Massachusetts Institute of Technology, and a BE from Tsinghua University. She is a receipt of the NSF CAREER award.

1 1