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

Colloquium Speaker Elad Hazan, Thurs April 3, 4:30pm
by Nicole E. Wagenblast 03 Apr '14

03 Apr '14

Sublinear Optimization for Machine Learning Elad Hazan, Technion, Israel Institute of Technology Thursday, April 3, 4:30pm Computer Science 105 In many modern optimization problems, particularly those arising in machine learning, the amount data is too large to apply standard convex optimization methods. We'll discuss new optimization algorithms that make use of randomization to prune the data produce a correct solution albeit running in time which is smaller than the data representation, i.e. sublinear running time. We'll present such sublinear-time algorithms for linear classification, support vector machine training, semi-definite programming and other optimization problems. These new algorithms are based on a primal-dual approach, and use a combination of novel sampling techniques and the randomized implementation of online learning algorithms. We'll describe information-theoretic lower bounds that show our running times to be nearly best possible in the unit-cost RAM model. The talk will be self contained - no prior knowledge in convex optimization or machine learning is assumed. Elad Hazan is an associate professor of operations research at the Technion, Israel Institute of Technology. His main research area is machine learning and its relationship to optimization, game theory and computational complexity. Elad received his Ph.D. in computer science from Princeton University. He is the recipient of several best paper awards including the Goldberg Best Paper award (twice), and the European Research Council starting grant.

1 1

Colloquium Speaker Arti Gupta Weds April 2, 4:30pm
by Nicole E. Wagenblast 02 Apr '14

02 Apr '14

Software Verification: Locks and MLoCs* Arti Gupta ( NEC Labs America ) Wednesday, April 2, 4:30pm Computer Science 105 Software verification deals with proving or falsifying correctness properties of programs, and has broad applications from ensuring safety of mission-critical software to improving program robustness and programmer productivity. This area has long held theoretical interest, but the inherent undecidability of the general problem and intractability of specific formulations have been barriers to practical success. Approaches based on automatic techniques for state space exploration, such as model checking and symbolic execution, have seen a resurgence of interest in recent years, driven largely by advancements in solvers for Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT). These solvers perform the underlying search for proofs or bugs, typically by reasoning over abstract models of programs. While abstraction is critical in scaling to real-life programs, it is equally important to ensure enough precision in the models and the analysis to verify specific properties of interest. In this talk, I will describe my work in foundational techniques that address these twin challenges of precision and scalability in verifying sequential and multi-threaded programs. I will also share the lessons learnt in my efforts in driving them to industry practice where they are routinely used in a modular methodology to find complex bugs in software projects, some with millions of lines of code. Finally, I will discuss future extensions and applications of this verification framework. *MLoC: Million Lines of Code Aarti Gupta received her PhD in Computer Science from Carnegie Mellon University. Her broad research interests are in the areas of formal analysis of programs/systems and automatic decision procedures. At NEC Labs she leads research in systems analysis and verification. She has given several invited keynotes highlighting the foundational research contributions of her group in verification and their successful industrial deployment. She has served as an Associate Editor for Formal Methods in System Design (since 2005) and for the ACM Transactions on Design Automation of Electronic Systems (2008-2012). She has also served as Co-Chair for the International Workshop on Satisfiability Modulo Theories (SMT) 2010, the International Conference on Computed Aided Verification (CAV) 2008, and Formal Methods in Computer Aided Design (FMCAD) 2006. She is currently serving on the Steering Committee of CAV.

1 2

Colloquium Speaker Emina Torlak, Today 4:30pm
by Nicole E. Wagenblast 31 Mar '14

31 Mar '14

Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond Emina Torlak ( University of California, Berkeley ) Monday, March 31, 4:30pm Computer Science 105 We live in a software-driven world. Software helps us communicate and collaborate; create art and music; and make discoveries in biological, physical, and social sciences. Yet the growing demand for new software, to solve new kinds of problems, remains largely unmet. Because programming is still hard, developer productivity is limited, and so is end-users' ability to program on their own. In this talk, I present a new approach to constructing programs, which exploits advances in constraint solving to make programming easier for experts and more accessible to everyone else. The approach is based on two observations. First, much of everyday programming involves the use of domain-specific languages (DSLs) that are embedded, in the form of APIs and interpreters, into modern host languages (for example, JavaScript, Scala or Racket). Second, productivity tools based on constraint solvers (such as verification or synthesis) work best when specialized to a given domain. Rosette is a new kind of host language, designed for easy creation of DSLs that are equipped with solver-based tools. These Solver-Aided DSLs (SDSLs) use Rosette's symbolic virtual machine (SVM) to automate hard programming tasks, including verification, debugging, synthesis, and programming with angelic oracles. The SVM works by compiling SDSL programs to logical constraints understood by SMT solvers, and then translating the solver's output to counterexamples (in the case of verification), traces (in the case of angelic execution), or code snippets (in the case of synthesis and debugging). Rosette has hosted several new SDSLs, including imperative SDSLs for data-parallel and spatial programming; a functional SDSL for specifying executable semantics of secure stack machines; and a declarative SDSL for web scraping by example. Emina Torlak is a researcher at U.C. Berkeley, working at the intersection of software engineering, formal methods, and programming languages. Her focus is on developing tools that help people build better software more easily. She received her B.Sc. (2003), M.Eng. (2004) and Ph.D. (2009) from MIT, where she developed Kodkod, an efficient SAT-based solver for relational logic. Kodkod has since been used in over 70 tools for verification, debugging, and synthesis of code and specifications. Emina has also worked on a wide range of domain-specific formal methods. She won an ACM SIGSOFT distinguished paper award for her work at LogicBlox, where she built a system for synthesizing massive data sets, used in testing of decision support applications. As a member of IBM Research, she led the development of a tool for bounded verification of memory models, enabling the first fully automatic analysis of the Java Memory Model. These experiences inspired her current research on solver-aided languages, which aims to reduce the effort of applying formal methods to new problem domains.

1 0

Colloquium Speaker Keith Winstein Thurs March 27, 4:30pm
by Nicole E. Wagenblast 27 Mar '14

27 Mar '14

Transport Architectures for an Evolving Internet Keith Winstein, Massachusetts Institute of Technology Thursday, March 27, 4:30pm Computer Science 105 The technologies that make up the Internet are changing every year, but some transport protocols continue to act as though the Internet behaved as it did 20 years ago. This can cause poor performance on newer networks -- cellular networks, datacenters -- and makes it more challenging to roll out networking technologies that break markedly with the past. How do we make applications and protocols keep up with an evolving network? I will describe the Sprout algorithm, a transport protocol designed for videoconferencing over cellular networks, that uses probabilistic inference to forecast network congestion in advance. On commercial cellular networks, Sprout gives 2-to-4 times the throughput and 7-to-9 times less delay than Skype, Apple Facetime, and Google+ Hangouts. This work led to Remy, a computer program that generates transport protocols automatically, as a function of a protocol designer's assumptions about the network and statement of an objective function. Remy's computer-generated algorithms can achieve higher performance and greater fairness than some sophisticated human-designed schemes. I will discuss our work on using Remy to probe open questions of Internet congestion control -- what's the cost of maintaining backwards compatibility with existing algorithms, including the Transmission Control Protocol as it exists today ? Is there a tradeoff between a protocol's performance today and its ability to adapt to networks of the future? This talk includes joint work with Anirudh Sivaraman, Pratiksha Thaker, and Hari Balakrishnan. URL: http://mit.edu/keithw Keith Winstein is a doctoral candidate at MIT's Computer Science and Artificial Intelligence Laboratory. His work applies statistical and predictive approaches to teach computers to design better network protocols and applications. He created the Mosh (mobile shell) tool for remote access to Unix-like systems and the Sprout algorithm for cellular networks, which was awarded a 2014 Applied Networking Research Prize. From 2007 to 2010, Keith worked as a staff reporter at The Wall Street Journal, covering science and medicine.

1 1

CJ Bell FPO
by Melissa M. Lawson 25 Mar '14

25 Mar '14

CJ Bell will present his Final Public Oral on Tuesday April 1 at 1:30PM in Room 402. The members of his committee are: David Walker, advisor; Andrew Appel and David August, readers; Ed Felten and Sharad Malik, nonreaders. A copy of his thesis, "A Proof Theory for Loop-Parallelizing Transformations", is on display in Room 310. Everyone is invited to attend his talk.

1 0

Colloquium Speaker Gabe Cohn Tuesday March 25, 4:30pm
by Nicole E. Wagenblast 25 Mar '14

25 Mar '14

Building Embedded Sensor Systems to Bring Ubicomp to Life Gabe Cohn ( University of Washington ) Tuesday, March 25, 4:30pm Computer Science 105 Although we have successfully created smaller, faster, and cheaper computer devices, several adoption barriers remain to realize the dream of Ubiquitous Computing (Ubicomp). By lowering these barriers, we can seamlessly embed human-computer interfaces into our home and work environments. My work focuses on building integrated hardware/software sensing systems for Ubicomp applications using my expertise in embedded systems, low-energy hardware design, and sensing, in addition to integrating communications, signal processing, and machine learning. In this talk, I will use my research to present three main techniques to lower the installation, maintenance, and scalability adoption barriers and bring Ubicomp to life. First, I will discuss my work on using the existing infrastructure in buildings to reduce the number of sensors required to enable many Ubicomp applications. Second, I will discuss how the conductive properties of the human body can be leveraged to enable novel human-computer interactions and health sensing opportunities. Finally, I will describe techniques for dramatically reducing the power consumption of embedded sensor systems for Ubicomp applications. By continually working on application-driven interdisciplinary research, we can lower the adoption barriers and enable many new high-impact application domains. Gabe Cohn is a Ph.D. candidate in Electrical Engineering in the Ubiquitous Computing (Ubicomp) Lab at the University of Washington, advised by Shwetak Patel. His research focuses on (1) designing and implementing ultra-low-power embedded sensing systems , (2) leveraging physical phenomena to enable new sensing modalities for human-computer interaction , and (3) developing sensor systems targeted at realizing immediate change in high-impact application domains . He was awarded the Microsoft Research Ph.D. Fellowship in 2012, the National Science Foundation Graduate Research Fellowship in 2010, and 6 Best Paper awards and nominations. He is the co-founder of SNUPI Technologies ( www.wallyhome.com ), a sensor and services company focused on home safety, security, and loss prevention. He received his B.S. with honors in Electrical Engineering from the California Institute of Technology in 2009, where he specialized in embedded systems, computer architectures, and digital VLSI.

1 1

Colloquium Speaker Michael Carbin Monday, March 24, 4:30pm
by Nicole E. Wagenblast 24 Mar '14

24 Mar '14

Verified Approximate Computing Michael Carbin , Massachusetts Institute of Technology Monday, March 24, 4:30pm Computer Science 105 Many modern applications implement large-scale computations (e.g., machine learning, big data analytics, and financial analysis) in which there is a natural trade-off between the quality of the results that the computation produces and the performance and cost of executing the computation. Exploiting this fact, researchers have recently developed a variety of new mechanisms that automatically manipulate an application to enable it to execute at a variety of points in its underlying trade-off space. The resulting approximate application can navigate this trade-off space to meet its performance and cost requirements. I present a program verification and analysis system, Rely, for answering fundamental questions that arise when manipulating an application that implements an approximate computation. Examples of the questions that Rely is designed to answer include: What is the probability that the approximate application produces the same result as the original application? How much do the approximate application’s results differ from those of the original application? And is the approximate application safe and secure? Rely answers these questions with a novel analysis and verification method for reasoning about the safety and accuracy of approximate applications. Rely also provides a novel language and program analysis for verifying quantitative reliability: the probability that the new approximate application produces the same result as the original computation. Michael Carbin is a Ph.D. Candidate in Electrical Engineering and Computer Science at MIT. Michael started his research career as undergraduate student, working on BDD-based program analysis at Stanford University and on type-safe compile-time metaprogramming at Microsoft Research. His work at Stanford received an award for Best Computer Science Undergraduate Honors Thesis. As a graduate student, Michael has worked as a MIT Lemelson Presidential Fellow and a Microsoft Research Graduate Fellow on both the theory and practice of verified approximate computing and software self-healing. His recent research on verifying the reliability of programs that execute on unreliable hardware won a best paper award at OOPSLA 2013: Object-Oriented Programming, Systems, Languages & Analysis.

1 2

11am Wed Mar 19 talk on optimal network traffic engineering
by Jennifer Rexford 17 Mar '14

17 Mar '14

Speaker: Kevin Tang, Cornell Title: Traffic Engineering: From Distributed Static Optimization to Centralized Transient Control Date/time: 11am-12pm on Wed March 19 Location: CS 402 Abstract: Traffic Engineering is of fundamental importance for network operation. Traditionally, it assumes static traffic input and then looks for distributed routing solutions to optimize certain objective. Along this line, in the first part of this talk, we will present HALO (Hop-by-hop Adaptive Link-state Optimal) routing. It is the first provable optimal link-state routing solution with hop-by-hop forwarding. Furthermore, our solution does not require traffic matrix as an explicit input and can adapt to changing traffic input. We prove our solution converges and solves the standard MCF (Multi-Commodity Flow) problem. Recently, there has been tremendous interest in SDN (Software-Defined Networking), which is an emerging network architecture that separates control and data planes. Conceivably, that means network managers can first solve Traffic Engineering optimization in a centralized manner and then translate the solution to configure network switches. Within this context, in the second part of this talk, we consider the problem of avoiding transient congestion while reconfiguring the routing paths. We formulate a flow-based and a switch-based model. For the flow-based model, we demonstrate that an optimal sequence of minimum update steps could always be found when the dependency graph is acyclic. For the switched model, we find a way to translate a feasible flow-based updating sequence to a feasible switch-based sequence subject to a tree topology constraint on the routing paths.

1 0

Colloquium Speaker Ameet Talwalkar Thurs March 13, 4:30pm
by Nicole E. Wagenblast 13 Mar '14

13 Mar '14

Machine Learning in the Wild Ameet Talwalkar ( University of California, Berkeley ) Thursday, March 13, 4:30pm Computer Science 105 Modern datasets are rapidly growing in size and complexity, and this wealth of data holds the promise for many transformational applications. Machine learning is seemingly poised to deliver on this promise, having proposed and rigorously evaluated a wide range of data processing techniques over the past several decades. However, concerns over scalability and usability present major roadblocks to the wider adoption of these methods, and in this talk I will present work that addresses these concerns. In terms of scalability, my work relies on a careful application of divide-and-conquer methodology. In terms of usability, I focus on developing tools to diagnose the applicability of learning techniques and to autotune components of typical machine learning pipelines. I will discuss applications in the context of matrix factorization, estimator quality assessment and genomic variant calling. Ameet Talwalkar is a postdoctoral fellow in the Computer Science Division at UC Berkeley. He obtained a Ph.D. in Computer Science from the Courant Institute at New York University, and prior to that graduated summa cum laude from Yale University. His work addresses scalability and ease-of-use issues in the field of machine learning, as well as applications related to large-scale genomic sequencing analysis. He has won the Janet Fabri Prize for best doctoral dissertation and the Henning Biermann Award for exceptional service at NYU, received Yale's undergraduate prize in Computer Science, and is an NSF OCI postdoctoral scholar.

1 2

4:30pm talk today on evolution of the Internet (doors open 4pm, reception afterwards)
by Jennifer Rexford 12 Mar '14

12 Mar '14

Begin forwarded message: > Resent-From: <jrex(a)Princeton.EDU> > From: "Heather L. Evans" <heathere(a)Princeton.EDU> > Subject: Seminar Announcement - Fathers of the Internet Reflecting on the Internet Evolution- Today at 4:30 pm > Date: March 12, 2014 9:03:57 AM EDT > To: "ee-seminar(a)princeton.edu" <ee-seminar(a)Princeton.EDU> > > > > Speakers: > Vinton Cerf, Chief Internet Evangelist, Google & Robert Kahn, CEO of Corporation for National Research Initiatives > Title: > Fathers of the Internet Reflecting on the Evolution of the Internet > Day: > Wednesday, March 12, 2014 > > > Time: > 4:30 pm > Room: > Friend Center Auditorium 101 > Host: > Mung Chiang > > > > > > > > > > Vinton Cerf (Chief Internet Evangelist at Google) and Robert Kahn (CEO of Corporation for National Research Initiatives), whose pioneering work on the Internet has been widely recognized by numerous awards, including the US Presidential Medal of Freedom, the US National Medal of Technology, and the ACM Turing Award, will together give a public duet lecture on “Perspectives on the Internet and its Evolution > > This is an open lecture to the general public. No fee or ticket required. Seating available on a first-come-first serve basis. Seating will begin at 4pm. Reception will follow. > > Additional information available at http://edgelab-events.princeton.edu/. > > > Heather Evans > Assistant to the Chair > Department of Electrical Engineering > Princeton University > Engineering Quadrangle, B-210 > Olden Street > Princeton, NJ 08544 > (p): 609-258-7282 > (f): 609-258-0119 > heathere(a)princeton.edu > >

1 0