October 2008 - talks - lists.cs.princeton.edu

E Schmidt FPO
by Melissa Lawson 17 Oct '08

17 Oct '08

Erich Schmidt will present his FPO on Thursday October 23 at 11AM in Room 302 (note room). The members of his committee are: J.P. Singh, advisor; Kai Li and Andrea LaPaugh, readers; Moses Charikar and Jennifer Rexford, nonreaders. A copy of his thesis, "Query-Independent Ranking for Large-Scale Persistent Search Systems", is on display in Room 310. Everyone is invited to attend his talk.

1 0

A Hobor FPO
by Melissa Lawson 10 Oct '08

10 Oct '08

Aquinas Hobor will present his Final Public Oral on Friday October 17 at 10AM in Room 402. The members of his committee are: Andrew Appel, advisor; David Walker and Peter O'Hearn, readers; Brian Kernighan and Vivek Pai, nonreaders. A copy of his thesis, "Oracle Semantics", is on display in Room 310. Everyone is invited to attend his talk.

1 0

cookies
by Ginny Hogan 09 Oct '08

09 Oct '08

Cookies are now available in the tea room followed by Ian Buck's talk at 4:30pm Computer Science Room 105 -

1 0

R Dockins general exam
by Melissa Lawson 09 Oct '08

09 Oct '08

Rob Dockins will present his research seminar/general exam on Thursday October 16 at 3PM in Room 402. The members of his committee are: Andrew Appel (advisor), David Walker, and Brian Kernighan. 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. ------------------------------------ Title: Modal Separation Logic for Program Verification and Metatheory Abstract: The construction of new logics for reasoning about programs has a long history in the field of program verification, going back at least to the seminal works of Floyd and Hoare. In this talk, I shall show how to combine separation logic with a generic multimodal logic using the proof assistant Coq. The logic that results is useful as a substrate for building higher-level program logics and as a tool for proving metatheoretic properties. The techniques I present can be readily generalized across different programming languages and support a large collection of features including mutable memory, unstructured control flow, explicit memory management, and shared-memory concurrency. I present examples from a toy language, the list machine benchmark, and from Concurrent C Minor, a realistic intermediate language for a concurrent C compiler. Reading List: Books: Benjamin Pierce. Types and Programming Languages. MIT Press. 2002. Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. Springer. 2004. G.E. Hughes and J.M. Cresswell. A New Introduction to Modal Logic. Routldge. 1996. Papers: Andrew W. Appel, Paul Andre Mellies, Christopher D. Richards and Jerome Vouillon. A Very Modal Model of a Modern, Major, General Type System. In Proc. Thirty-Fourth Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 2007. Chriatian Calcagno, Peter O'Hearn, Hongseok Yang. Local Action and Abstract Separation Logic. In Proc. Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS), July 2007. Alexy Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky and Mooly Sagiv. Local Reasoning for Storable Locks and Threads. In Proc. Fifth Asian Symposium on Programming Languages and Systems (APLAS), November 2007. Xavier Leroy and Sandrine Blazy. Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. Journal of Automated Reasoning, 41(1):1-31. July 2008. Greg Morrisett, David Walker, Karl Crary and Neal Glew. From System F to Typed Assembly Language. Twenty-Fifth ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 1998. Peter O'Hearn. Resources, Concurrency and Local Reasoning. Theoretical Computer Science 375(1):271-307, May 2007. Vaughan R. Pratt. Application of Modal Logic to Programming. Studia Logica, 39(2-3):257-274. June, 1980. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS), July 2002.

1 0

C Barnes general exam
by Melissa Lawson 09 Oct '08

09 Oct '08

Connelly Barnes will present his research seminar/general exam on Thursday October 16 at 10AM in Room 402. The members of his committee are: Adam Finkelstein (advisor), Perry Cook, and Tom Funkhouser. 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. ----------------------------------------- Video Puppetry: A Performative Interface for Cutout Animation Abstract We present a video-based interface that allows users of all skill levels to quickly create cutout-style animations by performing the character motions. The puppeteer first creates a cast of physical puppets using paper, markers and scissors. He then physically moves these puppets to tell a story. Using an inexpensive overhead camera our system tracks the motions of the puppets and renders them on a new background while removing the puppeteer's hands. Our system runs in real-time (at 30 fps) so that the puppeteer and the audience can immediately see the animation that is created. Our system also supports a variety of constraints and effects including articulated characters, multi-track animation, scene changes, camera controls, 21/2-D environments, shadows, and animation cycles. Users have evaluated our system both quantitatively and qualitatively: In tests of low-level dexterity, our system has similar accuracy to a mouse interface. For simple story telling, users prefer our system over either a mouse interface or traditional puppetry. We demonstrate that even first-time users, including an eleven-year-old, can use our system to quickly turn an original story idea into an animation. Book 3D Computer Graphics, 2nd Edition, Alan Watt Papers * Layered acting for character animation Dontcheva, M, Yngve, G, Popovic, Z. 2003. SIGGRAPH '03 * ARTag, a Fiducial Marker System Using Digital Techniques FIALA, M. 2005. Computer Vision and Pattern Recognition, 2005. CVPR '05. * OBBTree: A Hierarchical Structure for Rapid Interference Detection GOTTSCHALK, S., LIN, M. C., AND MANOCHA, D. 1996. SIGGRAPH. * Closed-Form Solution of Absolute Orientation using Unit Quaternions HORN, B. K. P. 1986. Journal of Optical Society of America * As-rigid-as-possible shape manipulation Igarashi, T, Moscovich, T, Hughes, J. 2005. ACM Trans. Graph. (Proc. SIGGRAPH), 1134-1141. * Tangible bits: towards seamless interfaces between people, bits and atoms Ishii, H, Ullmer, B. 1997. Proc. SIGCHI * Dinosaur input device Knep, B, Hayes, C, Sayre, R, Williams, T. 1995. Proc. SIGCHI * Object recognition from local scale-invariant features Lowe, D. 1999. International Conference on Computer Vision, 1150-1157. * A Taxonomy of Mixed Reality Visual Displays MILGRAM, P., AND KISHINO, F. 1994. IEICE Transactions on Information and Systems * Motion doodles: an interface for sketching character motion Thorne, M, Burke, D, Van de Panne, M. 2004. SIGGRAPH '04. * Detection and tracking of point features Tomasi, C, Kanade, T. 1991. Technical Report CMU-CS-91-132

1 0

Talk today - Ian Buck - NVIDIA
by Ginny Hogan 09 Oct '08

09 Oct '08

Ian Buck , NVIDIA, will present his talk "GPU Computing" at 4:30pm today - Computer Science Room 105 - Tea will be at 4:00pm -

1 0

Colloquium Speaker - Thursday Oct 9 -4:30PM
by Ginny Hogan 07 Oct '08

07 Oct '08

Ian Buck, NVIDIA, will present his talk "GPU Computing", Thursday, October 9th at 4:30pm Computer Science Room 105 - tea will be at 4:00pm.

1 0

Y Zhang general exam
by Melissa Lawson 07 Oct '08

07 Oct '08

Yun Zhang will present her research seminar/general exam on Tuesday October 14 at 11AM in Room 302. The members of her committee are: David August (advisor), Andrew Appel, and Doug Clark. Everyone is invited to attend her talk and those faculty wishing to remain for the oral exam following are welcome to do so. Her abstract and reading list follow below. ---------------------------- Abstract Shape Aware Memory Analysis for Multi-core Architecture Limited memory alias analysis inhibits automatic parallelization for multi-core architecture. Alias analysis generally considers memory accesses to separated parts of recursive data structures, especially cyclic ones, dependent since the analysis has no shape information indicating how the program traverses the data structure. For example, accesses to the left child of a binary tree node are separated from accesses to the right child, but current memory analysis methods conservatively conclude the accesses may alias with each other. This work proposes a three-step loop-aware memory analysis that performs dependence tests on loops that traverse recursive data structures to benefit automatic code parallelization.The first step captures shape information of recursive data structures using separation logic, the second traces two pointers' definition chains, and the third combines the two definition chains with the shape information of the data structure to see if the two pointer accesses separate or alias between loop iterations. Corresponding soundness proof in separation logic is demonstrated on a couple of typical examples. The experimental results show that this loop-aware alias analysis can effectively disprove false cross-iteration dependences, which unveils opportunities for automatic parallelization, eases the work of instruction distribution and reduces data communications between cores. Reading List Books: 1. Modern Compiler Implementation in ML, by A. W. Appel, Cambridge University Press, 1998 2. Advanced compiler design and implementation, by S. S. Muchnick, Morgan Kaufman, 1997 Papers: 3. Shape Analysis with Inductive Recursion Synthesis. B. Guo, N. Vachharajani, and D. I. August, Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI), June 2007. 4. Detecting Parallelism in C Programs with Recursive Data Sturctures, R. Ghiya, L. J. Hendren and Y. Zhu, Computational Complexity, page 159-173, 1998 5. Practical and Accurate Low-level Pointer Analysis, B. Guo, M.J. Bridges, S. Triantafyllis, G. Ottoni, E. Raman, and D. I. August, Proceedings of the Third International Symposium on Code Generation and Optimization (CGO), March 2005. 6. Identifying Parallelism in Programs with Cyclic Graphs, Y. Hwang and J. Saltz, Proceedings of the International Conference on Parallel Processing(ICPP), 2000 7. A Novel Approach for Detecting Heap-based Loop-carried Dependences, A. Tineo, F. Corbera, A. Navarro, R. Asenjo, and E.L. Zapata, Proceedings of the International Conference on Parallel Processing(ICPP), 2005 8. Analysis of Pointers and Structures, D. R. Chase, M. Wegman, F. K. Zadeck, Proceedings of the ACM SIGPLAN '90 Conference on Programming Language Design and Implementation, pp. 296-310, 1990. 9. Automatic Thread Extraction with Decoupled Software Pipelining, G. Ottoni, R. Rangan, A. Stoler, D. I. August, Proceedings of the 38th IEEE/ACM International Symposium on Microarchitecture (MICRO), November 2005 10. Revisiting the Sequential Programming Model for Multi-core, M. Bridges, N. Vachharajani, Y. Zhang, T. Jablin, D. I. August, Proceedings of the 40th IEEE/ACM International Symposium on Microarchitecture (MICRO), 2007 11. Points-to analysis by type inference in programs with structures and unions, B. Steensgaard, Lecture Notes in Computer Science, 1060 (T. Gyimothy, ed.), pp. 136-150, Springer-Verlag, 1996. Proceedings from the International Conference on Compiler Construction. 12. Relevant context inference, R. Chatterjee, B. G. Ryder, and W. A. Landi, Proceedings of the ACM Symposium on Principles of Programming Languages, pp. 133-146, January 1999.

1 0

FW: AT&T Shannon Labs Distinguished Speaker Series
by Melissa Lawson 07 Oct '08

07 Oct '08

If this is a series you think you will be interested in, please bookmark the website. Subject: AT&T Shannon Labs Distinguished Speaker Series Dear Colleagues, We are pleased to announce that AT&T Shannon Labs is hosting an ongoing Distinguished Speaker Series at our Florham Park, NJ facility. This series will feature talks from senior researchers, technology superstars, and policymakers from diverse backgrounds in computer science, telecommunications, science, and technology. We would like to invite members from the local research community to join us and hear from these experts about their views on the future of computing, communications and science, and its impact on our world. The talks will be made available through our research website at http://www.research.att.com. The first talk in the series is being held on Oct 15, from 3:30pm-4:30pm. The details follow. There is limited space available for visitors on a first come first serve basis. If you would like to come, please send us an email at dssorg(a)research.att.com by Oct. 12 so we can arrange to have visitor passes available. -- Speaker: Brian Snow Title: We Need Assurance Time: 3:30pm-4:30pm. Oct 15, 2008. Location: C050 (auditorium) Abstract: When will we be secure? Nobody knows for sure - but it cannot happen before commercial security products and services possess not only enough functionality to satisfy customers' stated needs, but also sufficient assurance of quality, reliability, safety, and appropriateness for use. Such assurances are lacking in most of today's commercial security products and services. I discuss paths to better assurance in Operating Systems, Applications, and Hardware through better development environments, requirements definition, systems engineering, quality certification, and legal/regulatory constraints. I also give some examples. Biography: Mathematician/computer scientist, Brian taught mathematics and helped found the computer science department at Ohio University in the late 1960's. He joined the National Security Agency in 1971 where he became a cryptologic designer and security systems engineer. Brian spent his first 20 years at NSA doing and directing research that developed cryptographic components and secure systems. Many cryptographic systems serving the U.S. government and military use his algorithms; they provide capabilities not previously available and span a range from nuclear command and control to tactical radios for the battlefield. Computer Security and Network Security were major aspects for these systems. He created and managed NSA's Secure Systems Design division in the 1980s. He has many patents, awards, and honors attesting to his creativity. His later years at NSA were the model for what it means to be a senior Technical Director at NSA (similar to a Chief Scientist or Senior Technical Fellow in industry); he served in that capacity in three major mission components - The Research Directorate (1994-1995), The Information Assurance Directorate (1996-2002), and The Directorate for Education and Training --NSA's Corporate University (2003-2006) He was the first Technical Director appointed at the "Key Component" level at NSA, and the only "techie" at NSA to serve in such a role across three different Directorates. In all of his positions, he insisted that the actions NSA took to provide intelligence for our national and military leaders should not put U.S. persons or their rights at risk. He was a leading voice for always assessing the unintended consequences of both success and failure prior to taking action. Brian retired in 2006 and is now an Independent Security Consultant and Ethics Advisor. --------------------------------------------------------------------------

1 0