- talks - lists.cs.princeton.edu

R Dockins preFPO
by Melissa M. Lawson 22 Nov '11

22 Nov '11

Rob Dockins will present his preFPO on Tuesday November 29 at 10AM in Room 402. The members of his committee are: Andrew Appel, advisor; David Walker and Xavier Leroy (INRIA), readers; David August and Mark Braverman, nonreaders. Everyone is invited to attend his talk. His abstract follows below. ---------------------- Title ========== Behavioral Refinement Abstract ======================== What does it mean for a compiler to be correct? This question is of central importance for anyone attempting to prove a compiler correct, or for users of a compiler to understand what they should expect the compiler to do. Surprisingly, no real consensus has emerged as to the best answer to this question. As a result, it can be rather difficult to understand what a particular compiler correctness proof actually proves, and it is especially difficult to understand the relationship between various different compiler verification efforts. In this thesis, I will propose a specific approach to the question of compiler correctness which is simple and easy to understand, but is also capable of expressing the correctness statement for the majority of compiler correctness projects that currently exist. In other words, I will develop a single parametrized theory of correctness which can be instantiated multiple ways to achieve a theory specific to a particular language and compiler. To accomplish this, I borrow the idea of bisimulations from the concurrency calculus community and adjust it somewhat to fulfill our needs. The main strength of bisimulations is that they easily handle nondeterministic computation. Although popular programming languages rarely feature explicitly nondeterministic features, nondeterminism is nonetheless frequently introduced through interaction with the environment and/or via concurrency primitives. Thus, it is important to smoothly handle nondeterminism in our theory of program semantics. However, the bisimulations developed for concurrency calculi lack a feature we will find very important in our compiler correctness setting: they cannot reason about programs which may go wrong, or exhibit undefined behavior. In situations where undefined behavior occurs, the compiler writer wishes to have freedom to replace the undefined behavior with arbitrary behavior. Bisimulations to not allow us to express this sort of transformation. Thus, we develop a notion of program refinement, which weakens the notion of bisimulation just enough to allow the proper handling of undefined behavior. This notion of refinement provides exactly what we need to answer our motivating question: "A correct compiler is one which outputs a program which is a refinement of the input program." I defend the notion of refinement by relating to an axiomatic semantics based on a variant of Hennessy-Milner logic. The formulae of Hennessy-Milner logic allow one to express specifications of the observable behavior of a program. We show that refinement is precisely the same as preserving all observable specifications in the logic. I will also develop a theory of safe programs. Safe programs are those which will never exhibit undefined behavior. We show that for the safe programs, our notion of refinement collapses back into the more traditional notion of bisimulation. In addition, we demonstrate an interesting and unexpected result: program safety is intimately related to the axiom of the excluded middle (EM) in the logic of observable specifications. Safe programs enjoy EM, whereas unsafe programs do not. In this thesis, I will examine three different variations of bisimulation of increasing complexity (strong, branching and environmental), and show how they can all be relaxed into refinements. For each, we will give a logical characterization which will precisely capture the properties preserved by refinement, and for each we will develop the theory of safe programs. I intend to show that environmental refinement provides an excellent theory for reasoning about realistic languages and execution contexts. In particular, I shall argue that it provides just the right abstraction for discussing the correctness of the verified C compiler CompCert.

1 0

Colloquium talk starting now
by Nicole E. Wagenblast 21 Nov '11

21 Nov '11

Automating End-user Programming and Education using Program Synthesis Sumit Gulwani, Microsoft Research Monday, November 21, 2011, 1:30 PM Computer Science Small Auditorium (Room 105) Recent research in program synthesis has made it possible to effectively synthesize small programs in a variety of domains. In this talk, I will describe two useful applications of this technology that have the potential to influence daily lives of billions of people. One application involves automating end-user programming using examples or keywords, which can allow non-programmers to effectively use computational devices such as computers, smartphones (and in the future robots) to perform a variety of repetitive tasks. Another application involves building intelligent tutoring systems that can help teachers and students with a variety of educational activities such as synthesizing problems, hints, solutions in various domains including math, science, and programming. Sumit Gulwani is a senior researcher in the RiSE group at Microsoft Research, Redmond. His primary research interest is in the area of program synthesis with applications to automating end user programming and building intelligent tutoring systems. Sumit obtained his PhD in computer science from UC-Berkeley in 2005, and was awarded the C.V. Ramamoorthy Award and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in computer science and engineering from the Indian Institute of Technology (IIT) Kanpur in 2000 and was awarded the President's Gold Medal.

1 0

Colloquium speaker Sumit Gulwani Monday Nov 21- 1:30pm
by Nicole E. Wagenblast 18 Nov '11

18 Nov '11

Automating End-user Programming and Education using Program Synthesis Sumit Gulwani, Microsoft Research Monday, November 21, 2011, 1:30 PM Computer Science Small Auditorium (Room 105) Recent research in program synthesis has made it possible to effectively synthesize small programs in a variety of domains. In this talk, I will describe two useful applications of this technology that have the potential to influence daily lives of billions of people. One application involves automating end-user programming using examples or keywords, which can allow non-programmers to effectively use computational devices such as computers, smartphones (and in the future robots) to perform a variety of repetitive tasks. Another application involves building intelligent tutoring systems that can help teachers and students with a variety of educational activities such as synthesizing problems, hints, solutions in various domains including math, science, and programming. Sumit Gulwani is a senior researcher in the RiSE group at Microsoft Research, Redmond. His primary research interest is in the area of program synthesis with applications to automating end user programming and building intelligent tutoring systems. Sumit obtained his PhD in computer science from UC-Berkeley in 2005, and was awarded the C.V. Ramamoorthy Award and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in computer science and engineering from the Indian Institute of Technology (IIT) Kanpur in 2000 and was awarded the President's Gold Medal.

1 1

A Primer on Patents - TODAY @ 5:30pm in Friend 101
by Stephen Schultze 16 Nov '11

16 Nov '11

A Primer on Patents – Manny Schecter, Chief Patent Counsel, IBM Date: Wednesday, November 16, 2011 Time: 5:30 PM – 7:00 PM Location: 101 Friend Center Patents are often opaque and confusing for everyone except patent attorneys. Engineers and scientists are nevertheless encouraged to pursue patents and warned to avoid patent infringement. Policy makers continue to debate about whether the United States’ approach to patents fosters innovation. Companies like Google have paid billions for patent portfolios of their competitors. Congress recently passed new patent legislation. Manny Schecter will present an overview of how patents are created, what makes for strong patents, and why they exist in the first place. Manny W. Schecter is Chief Patent Counsel, Associate General Counsel, and Managing IP Attorney at IBM. In his current position, Mr. Schecter leads IBM’s worldwide intellectual property law organization on patent matters and advises on intellectual property strategy and policy. Mr. Schecter has been employed in the IP organization of IBM for over 20 years, including positions in Vermont, Virginia, Arizona, and New York. His current position is at IBM corporate headquarters in Armonk, NY. Mr. Schecter is an active member of several IP related organizations. He currently serves on the board of directors of the Intellectual Property Owners Association (IPO), the IPO Education Foundation, and Allied Security Trust. He is also the vice-chair of the Professional Programs Committee and the immediate past chair of the Electronic and Computer Law Committee of the American Intellectual Property Law Association (AIPLA). Mr. Schecter organized the patent quality initiative which became the Peer-to-Patent project that has been piloted in the US and several other countries and for which he continues to serve on the Steering Committee. He has spoken at numerous IP related events, he has authored several articles on patent quality, and he blogs at ibmip.com. Mr. Schecter is a graduate of Cornell University and the George Washington University Law School. This event is co-sponsored by The Center for Information Technology Policy and the Keller Center To receive emails about future CITP events and to subscribe to the CITP events calendar, visit: http://citp.princeton.edu/about/subscribe/

1 0

Colloquium Speaker Nickolai Zeldovich Thrus Nov 17th-4pm
by Nicole E. Wagenblast 16 Nov '11

16 Nov '11

CryptDB: Protecting Confidentiality with Encrypted Query Processing Nickolai Zeldovich, Massachusetts Institute of Technology Thursday, November 17, 2011, 4:30 PM - 5:30 PM Computer Science Small Auditorium (Room 105) Online applications are vulnerable to theft of sensitive information because adversaries can exploit software bugs to gain access to private data, and because curious or malicious administrators may capture and leak data. In this talk, I will describe CryptDB, a system that provides practical and provable confidentiality in the face of these attacks for applications backed by SQL databases. It works by executing SQL queries over encrypted data using a collection of efficient SQL-aware encryption schemes. CryptDB can also chain encryption keys to user passwords, so that a data item can be decrypted only by using the password of one of the users with access to that data. As a result, a database administrator never gets access to decrypted data, and even if all servers are compromised, an adversary cannot decrypt the data of any user who is not logged in. An analysis of a trace of 126 million SQL queries from a production MySQL server shows that CryptDB can support operations over encrypted data for 99.5% of the 128,840 columns seen in the trace. Our evaluation shows that CryptDB has low overhead, reducing throughput by 14.5% for phpBB, a web forum application, and by 26% for queries from TPC-C, compared to unmodified MySQL. Nickolai Zeldovich is Douglas T. Ross Career Development Assistant Professor at MIT's EECS department and a member of the Computer Science and Artificial Intelligence Laboratory. His research interests are in building practical secure systems, from operating systems and hardware to programming languages and security analysis tools. He received his PhD from Stanford University in 2008, where he developed HiStar, an operating system designed to minimize the amount of trusted code by controlling information flow. In 2005, he co-founded MokaFive, a company focused on improving desktop management and mobility using x86 virtualization. Prof. Zeldovich received a Sloan fellowship in 2010, and an NSF CAREER award in 2011.

1 1

T Jablin preFPO
by Melissa M. Lawson 14 Nov '11

14 Nov '11

Tom Jablin will present his preFPO on Monday November 21 at 3PM in Room 402. The members of his committee are: David august, advisor; Doug Clark and Scott Mahlke (UMichigan), readers; Margaret Martonosi and David Walker, nonreaders. Everyone is invited to attend his talk. His abstract follows below. ----------------- GPUs are flexible parallel processors capable of accelerating real applications. To exploit them, programmers rewrite programs in new languages using intimate knowledge of the underlying hardware. This is a step backwards in abstraction and ease of use from sequential programming. When implementing sequential applications, programmers focus on programs' high-level algorithmic structure, allowing the compiler to target the peculiarities of specific hardware. Automatic parallelization can return ease of use and hardware abstraction to programmers. This proposal suggests techniques for automatically parallelizing ordinary sequential C codes for GPUs using DOALL, pipelined, and speculative techniques. The key contributions are: the first software-only shared memory system for GPUs, and the first fully-automatic pipeline parallelization system for GPUs. Combining these three components yields a fully-automatic parallelizing compiler for GPUs that is applicable to many general purpose applications.

1 0

Colloquium Speaker Erik Sudderth Wed Nov 9- 4:30pm
by Nicole E. Wagenblast 08 Nov '11

08 Nov '11

Uncertainty in Natural Image Segmentation Eric Sudderth, Brown University Wednesday, November 9, 2011, 4:30 PM Computer Science Small Auditorium (Room 105) We explore nonparametric Bayesian statistical models for image partitions which coherently model uncertainty in the size, shape, and structure of human image interpretations. Examining a large set of manually segmented scenes, we show that object frequencies and segment sizes both follow power law distributions, which are well modeled by the Pitman-Yor (PY) process. This generalization of the Dirichlet process leads to segmentation algorithms which automatically adapt their resolution to each image. Generalizing previous applications of PY priors, we use non-Markov Gaussian processes (GPs) to infer spatially contiguous segments which respect image boundaries. We show how GP covariance functions can be calibrated to accurately match the statistics of human segmentations, and that robust posterior inference is possible via a variational method, expectation propagation. The resulting method produces highly accurate segmentations of complex scenes, and hypothesizes multiple image partitions to capture the variability inherent in human scene interpretations.

1 1

Z Wang FPO
by Melissa M. Lawson 07 Nov '11

07 Nov '11

Zhe Wang will present his FPO on Monday November 14 at 10AM in Room 402. The members of his committee are: Kai Li, advisor; Moses Charikar and Olga Troyanskaya, readers; Jennifer Rexford and Andrea LaPaugh, nonreaders. A copy of his thesis, "Similarity Search with Multimodal Data" is on display in Room 310. Everyone is invited to attend his talk.

1 0

Colloquioum Speaker Gerry Tesauro Wed Oct 26 4:30pm
by Nicole E. Wagenblast 24 Oct '11

24 Oct '11

How Watson Learns Superhuman Jeopardy! Strategies Gerry Tesauro, IBM Research Wednesday, October 26, 2011, 4:30 PM Computer Science Small Auditorium (Room 105) Major advances in Question Answering technology were needed for Watson to play Jeopardy! at championship level -- the show requires rapid-fire answers to challenging natural language questions, broad general knowledge, high precision, and accurate confidence estimates. In addition, Jeopardy! features four types of decision making carrying great strategic importance: (1) selecting the next clue when in control of the board; (2) deciding whether to attempt to buzz in; (3) wagering on Daily Doubles; (4) wagering in Final Jeopardy. This talk describes how Watson makes the above decisions using innovative quantitative methods that, in principle, maximize Watson's overall winning chances. We first describe our development of faithful simulation models of human contestants and the Jeopardy! game environment. We then present specific learning/optimization methods used in each strategy algorithm: these methods span a range of popular AI research topics, including Bayesian inference, game theory, Dynamic Programming, Reinforcement Learning, and real-time "rollouts." Application of these methods yielded superhuman game strategies for Watson that significantly enhanced its overall competitive record. Joint work with David Gondek, Jon Lenchner, James Fan and John Prager. Gerald Tesauro is a Research Staff Member at IBM's TJ Watson Research Center. He is best known for developing TD-Gammon, a self-teaching neural network that learned to play backgammon at human world championship level. He has also worked on theoretical and applied machine learning in a wide variety of other settings, including multi-agent learning, dimensionality reduction, computer virus recognition, computer chess (Deep Blue), intelligent e-commerce agents and autonomic computing. Dr. Tesauro received BS and PhD degrees in physics from University of Maryland and Princeton University, respectively.

1 1

October 20: SIGGRAPH Computer Graphics Film Show
by Nicole E. Wagenblast 19 Oct '11

19 Oct '11

The Princeton ACM / IEEE-CS Chapters present the 32nd annual SIGGRAPH Computer Graphics Film Show. This meeting features the latest and greatest computer animations direct from the ACM SIGGRAPH conference and Computer Animation Festival, held this summer in Vancouver. Szymon Rusinkiewicz of Princeton University is again the host and presenter. This meeting is free and open to the public. Students and their parents are welcome. There is no admission charge, and refreshments are served. Date: Thursday October 20, 2011, 8:00 pm (Refreshments and networking at 7:30 pm) Place: Friend Center Auditorium, Room 101, Olden and William Streets, Princeton University See princetonacm.acm.org for more details.

1 0