- talks - lists.cs.princeton.edu

Qinshi Wang will present his General Exam "Decision procedures useful in separation-logic proofs of functional correctness" on Thursday, May 9, 2019 at 3:30pm in Friend 203.
by Nicki Mahler 02 May '19

02 May '19

Qinshi Wang will present his General Exam "Decision procedures useful in separation-logic proofs of functional correctness" on Thursday, May 9, 2019 at 3:30pm in Friend 203. The members of his committee are as follows: Andrew Appel (adviser), Zak Kincaid, and Aarti Gupta. 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. Research talk title: Decision procedures useful in separation-logic proofs of functional correctness Abstract: VST has been used successfully to verify C programs with rich specifications. However, proofs in Verifiable C require substantial human work, which prevents applications in larger programs. We have improved VST’s proof automation in two ways. The first is term inference in existential variables, heap lemmas and function calls. The second is an automatic prover that solves relations on lists. Our list/array theory contains list concatenations, which occur frequently in array content specifications, and are undecidable in general. But we show a decidable fragment, in which relations between different positions in the same list are prohibited. We show this fragment covers many useful verification goals found in existing VST verifications. Reading list: 1. Bradley, Aaron R., and Zohar Manna. The calculus of computation: decision procedures with applications to verification. Springer Science & Business Media, 2007. 2. Pierce, Benjamin C., et al. "Software foundations." Volumes 1 & 2. [ https://softwarefoundations.cis.upenn.edu/ | Webpage: https://softwarefoundations.cis.upenn.edu/ ] (2010). 3. Bradley, Aaron R. "Safety analysis of systems." Chapter 2. PhD diss., Stanford University, 2007. 4. Habermehl, Peter, Radu Iosif, and Tomáš Vojnar. "What else is decidable about integer arrays?." International Conference on Foundations of Software Science and Computational Structures. Springer, Berlin, Heidelberg, 2008. 5. Lothaire, Monsieur, and M. Lothaire. Algebraic combinatorics on words. Chapter 12. Cambridge university press, 2002. 6. Furia, Carlo A. "What’s Decidable About Sequences?." International Symposium on Automated Technology for Verification and Analysis. Springer, Berlin, Heidelberg, 2010. 7. Le, Xuan-Bach, and Aquinas Hobor. "Logical reasoning for disjoint permissions." European Symposium on Programming. Springer, Cham, 2018. 8. Jacobs, Bart, et al. "VeriFast: A powerful, sound, predictable, fast verifier for C and Java." NASA Formal Methods Symposium. Springer, Berlin, Heidelberg, 2011. 9. Calcagno, Cristiano, et al. "Compositional shape analysis by means of bi-abduction." ACM SIGPLAN Notices. Vol. 44. No. 1. ACM, 2009. 10. Brotherston, James, Nikos Gorogiannis, and Max Kanovich. "Biabduction (and related problems) in array separation logic." International Conference on Automated Deduction. Springer, Cham, 2017. 11. Appel, Andrew W. "VeriSmall: verified smallfoot shape analysis." International Conference on Certified Programs and Proofs. Springer, Berlin, Heidelberg, 2011.

1 0

TODAY at 4:30pm in B205 - Asu Ozdaglar, MIT
by Emily Lawrence 02 May '19

02 May '19

EE SEMINAR Speaker: Prof. Asu Ozdaglar, Massachusetts Institute of Technology Title: Network Games Day: Thursday, May 2, 2019 Time: 4:30 pm Room: B205 Engineering Quadrangle Host: Ozge Akmandor Abstract: In many social and economic settings, decisions of individuals are affected by the actions of their friends, colleagues, and peers. Examples include adoption of new products and innovations, opinion formation and social learning, public good provision, financial exchanges and international trade. Network games have emerged as a powerful framework to study these settings with particular focus on how the underlying patterns of interactions, governed by a network, affect the economic outcomes. For tractability reasons, much of the work in this area studied games with special structure (e.g., quadratic cost functions, scalar non-negative strategies) or special properties (e.g., games of strategic complements or substitutes). In this talk, we will present a unified framework based on a variational inequality reformulation of the Nash equilibrium to study equilibrium properties of network games including existence and uniqueness, convergence of the best response dynamics and comparative statics. Our framework extends the literature in multiple dimensions, covering games with general strategic interactions and multidimensional and constrained strategy sets. In the second part of the talk, we will present a new class of infinite populations games, graphon games, that can capture heterogenous local interactions. We will show how graphon games can approximate strategic behavior and allow design of intervention policies for sampled network games that are robust to stochastic variations. This is joint work with Francesca Parise. Bio: Asu Ozdaglar received the B.S. degree in electrical engineering from the Middle East Technical University, Ankara, Turkey, in 1996, and the S.M. and the Ph.D. degrees in electrical engineering and computer science from the Massachusetts Institute of Technology, Cambridge, in 1998 and 2003, respectively. She is the Distinguished Professor of Engineering in the Electrical Engineering and Computer Science (EECS) Department at the Massachusetts Institute of Technology. She is also the department head of EECS. Her research expertise includes optimization theory, with emphasis on nonlinear programming and convex analysis, game theory, with applications in communication, social, and economic networks, distributed optimization and control, and network analysis with special emphasis on contagious processes, systemic risk and dynamic control. Professor Ozdaglar is the recipient of a Microsoft fellowship, the MIT Graduate Student Council Teaching award, the NSF Career award, the 2008 Donald P. Eckman award of the American Automatic Control Council, the Class of 1943 Career Development Chair, the inaugural Steven and Renee Innovation Fellowship, and the 2014 Spira teaching award. She served on the Board of Governors of the Control System Society in 2010 and was an associate editor for IEEE Transactions on Automatic Control. She was the inaugural area co-editor for the area entitled "Games, Information and Networks" in the journal Operations Research .She is the co-author of the book entitled "Convex Analysis and Optimization" (Athena Scientific, 2003). This seminar is supported with funds from the Bede Liu Fund for Excellence in Engineering.

1 0

Reminder: Michael Uhlar and Sathya Gunasekar tomorrow at 12:30
by Emily C. Lawrence 02 May '19

02 May '19

Michael Uhlar and Sathya Gunasekar from Facebook Friday, May 3 at 12:30pm Computer Science - Room 104 (large auditorium) [ https://www.cs.princeton.edu/events/25851 | https://www.cs.princeton.edu/events/25851 ] CacheLib - Unifying & Abstracting HW for caching @ Facebook In order to operate with high efficiency, Facebook’s infrastructure relies on caching in many different backend services. These services place very different demands on their caches, e.g., in terms of working set sizes, access patterns, and throughput requirements. Historically, each service used a different cache implementation, leading to inefficiency, duplicated code and effort. CacheLib is an embedded caching engine, which addresses this requirement with a unified API for building a cache implementation across many HW mediums. CacheLib transparently combines volatile and non-volatile storage in a single caching abstraction. To meet the varied demands, CacheLib successfully provides a flexible, high-performance solution for many different services at Facebook. In this talk, we describe CacheLib’s design, challenges, and several lessons learned.

1 0

Ross Teixeira will present his MSE thesis talk “SwitchScope: A View from the Inside” on Wednesday, May 8th, 2019 at 3pm in CS 402.
by Nicki Mahler 01 May '19

01 May '19

Ross Teixeira will present his MSE thesis talk “SwitchScope: A View from the Inside” on Wednesday, May 8th, 2019 at 3pm in CS 402. The members of his committee are Jennifer Rexford (adviser) and David Walker. Everyone is invited to attend his talk. His abstract follows below. Title: “SwitchScope: A View from the Inside” Abstract: Running a modern network requires constant diligence to maintain efficiency and reliability for customers. This is made challenging by the fact that the life of a packet inside each switch is complex, and yet currently quite hard to observe and debug. Packets entering a switch may be dropped (by access control policy or a full queue), or delayed (by a long queue) or modified (by policy) before heading to the next hop. Prior telemetry systems allow network operators to analyze flows that a switch sees, but they do not grapple with the internals of the switch’s multiple pipelines. In this talk, I will discuss our contributions towards SwitchScope, a flexible telemetry system that utilizes programmable (PISA) switches, and which allows debugging switch configurations and determining the source of bottlenecks or lost packets. I will detail our work on an expressive query language that provides network operators insight into the life of packets in a switch, as well as our compilation strategies to support useful queries about lost packets while minimizing the use of switch resources.

1 0

PACM COLLOQUIUM - Monday, May 6 - Yuxin Chen, Princeton University
by Emily Lawrence 01 May '19

01 May '19

DATE/LOCATION: Monday, May 6, 2019, 4:00 – 5:00 PM / 214 Fine Hall SPEAKER: Yuxin Chen (Princeton University) TITLE: Bridging convex and nonconvex optimization in noisy matrix completion: Stability and uncertainty quantification ABSTRACT: This talk is concerned with noisy matrix completion: given partial and corrupted entries of a large low-rank matrix, how to estimate and infer the underlying matrix? Arguably one of the most popular paradigms to tackle this problem is convex relaxation, which achieves remarkable efficacy in practice. However, the statistical stability guarantees of this approach is still far from optimal in the noisy setting, falling short of explaining the empirical success. Moreover, it is generally very challenging to pin down the distributions of the convex solution, which presents a major roadblock in assessing the uncertainty, or “confidence”, for the obtained estimates --- a crucial task at the core of statistical inference. Our recent work makes progress towards understanding stability and uncertainty quantification for matrix completion. When the rank of the unknown matrix is a constant: (1) we demonstrate that convex programming achieves near-optimal estimation errors vis-a-vis random noise; (2) we develop a de-biased estimator that admits accurate distributional characterizations, thus enabling asymptotically optimal inference. All of this is enabled by bridging convex relaxation with the nonconvex Burer-Monteiro approach, a seemingly distinct algorithmic paradigm that is provably robust against noise. This is joint work with Cong Ma, Yuling Yan, Yuejie Chi, and Jianqing Fan.

1 0

Reminder: Angela Zhou, TODAY at 12:30, Friend 112
by Emily Lawrence 30 Apr '19

30 Apr '19

Informal Research Talk Angela Zhou from Cornell Tuesday, April 30 - 12:30 pm Friend Center - Room 112 Host: Barbara Engelhardt Safely Learning to Personalize from Observational Data Some of the most impactful applications of machine learning are not just about prediction but are rather about taking the right action, directed at the right target, at the right time. The goal of our work is to extract causal-effect-maximizing personalized decision rules from observational data in sensitive applications. Observational data, the norm rather than the exception in domains such as medicine and civics, lack experimental manipulation so that isolated causal effects are obscured by complex selection processes, a phenomenon known as confounding. We develop a framework for learning personalized decision policies from observational data while accounting for possible unobserved confounding in the data-generating process. In contrast, the previous literature assumes that all confounders are observed, an unverified assumption that is generally violated in practice. Under the Neyman-Rubin potential outcomes framework, policy evaluation is analogous to assessing subgroup treatment effects: policy learning parametrizes the subgroup by a machine learning predictor of who should be treated. We calibrate policy learning for realistic violations of this unverifiable assumption with uncertainty sets for inverse propensity weights motivated by sensitivity analysis in causal inference. Our framework for confounding-robust policy improvement optimizes the minimax regret of a candidate policy against a baseline standard-of-care policy over an uncertainty set. We prove that if the uncertainty set is well-specified, our robust policy, when applied in practice, will do no worse than the baseline and improve upon it if possible, and that it is asymptotically minimax optimal. We use efficient algorithmic solutions to optimize over parametrized spaces of decision policies such as logistic treatment assignment and decision trees. We assess our methods on synthetic data and on a large clinical trial, demonstrating that hidden confounding can hinder existing policy learning approaches, while our robust approach guarantees safety and focuses on well-evidenced improvement, a necessity for making personalized treatment policies learned from observational data reliable in practice. A conference version of this work appeared at Neurips 2018 and an extended version is under Major Revision at Management Science. Bio: Angela Zhou is a third-year PhD student at Cornell in Operations Research and Information Engineering. She is currently located at Cornell Tech (NYC) where she is very fortunate to be advised by Nathan Kallus. Her work is supported on a NDSEG fellowship. Previously, she studied Operations Research and Financial Engineering at Princeton University. -- Jonathan Lu | Princeton University | Class of 2019 Department of Computer Science, Master's Program jhlu(a)princeton.edu | (510) 779-4158

1 0

Tomorrow: Angela Zhou Tuesday April 30 12:30-1:30 PM Friend 112
by Emily Lawrence 29 Apr '19

29 Apr '19

Angela Zhou (ORFE '15), currently a third-year PhD student at Cornell in Operations Research and Information Engineering working with Nathan Kallus, will be speaking about her machine learning and causal inference work: "Safely Learning to Personalize from Observational Data". She does thoughtful and fascinating work. Y'all should come out-- there will be lunch (vegan options available)! Informal Research Talk Angela Zhou from Cornell Tuesday, April 30 - 12:30 pm Friend Center - Room 112 Host: Barbara Engelhardt Safely Learning to Personalize from Observational Data Some of the most impactful applications of machine learning are not just about prediction but are rather about taking the right action, directed at the right target, at the right time. The goal of our work is to extract causal-effect-maximizing personalized decision rules from observational data in sensitive applications. Observational data, the norm rather than the exception in domains such as medicine and civics, lack experimental manipulation so that isolated causal effects are obscured by complex selection processes, a phenomenon known as confounding. We develop a framework for learning personalized decision policies from observational data while accounting for possible unobserved confounding in the data-generating process. In contrast, the previous literature assumes that all confounders are observed, an unverified assumption that is generally violated in practice. Under the Neyman-Rubin potential outcomes framework, policy evaluation is analogous to assessing subgroup treatment effects: policy learning parametrizes the subgroup by a machine learning predictor of who should be treated. We calibrate policy learning for realistic violations of this unverifiable assumption with uncertainty sets for inverse propensity weights motivated by sensitivity analysis in causal inference. Our framework for confounding-robust policy improvement optimizes the minimax regret of a candidate policy against a baseline standard-of-care policy over an uncertainty set. We prove that if the uncertainty set is well-specified, our robust policy, when applied in practice, will do no worse than the baseline and improve upon it if possible, and that it is asymptotically minimax optimal. We use efficient algorithmic solutions to optimize over parametrized spaces of decision policies such as logistic treatment assignment and decision trees. We assess our methods on synthetic data and on a large clinical trial, demonstrating that hidden confounding can hinder existing policy learning approaches, while our robust approach guarantees safety and focuses on well-evidenced improvement, a necessity for making personalized treatment policies learned from observational data reliable in practice. A conference version of this work appeared at Neurips 2018 and an extended version is under Major Revision at Management Science. Bio: Angela Zhou is a third-year PhD student at Cornell in Operations Research and Information Engineering. She is currently located at Cornell Tech (NYC) where she is very fortunate to be advised by Nathan Kallus. Her work is supported on a NDSEG fellowship. Previously, she studied Operations Research and Financial Engineering at Princeton University. -- Jonathan Lu | Princeton University | Class of 2019 Department of Computer Science, Master's Program jhlu(a)princeton.edu <mailto:jhlu@princeton.edu> | (510) 779-4158

1 0

Jake Silverman will present his General Exam on May 7, 2019 at 2pm in CS 302
by Nicki Mahler 29 Apr '19

29 Apr '19

Jake Silverman will present his General Exam on May 7, 2019 at 2pm in CS 302. The members of his committee are as follows: Zak Kincaid (adviser), Aarti Gupta, and Andrew Appel. 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: Loop Summarization with Rational Vector Addition Systems Abstract: Modern software verification techniques employ a number of heuristics for reasoning about loops. While these heuristics are often effective, they are unpredictable. For example, abstract interpretation analyses sometimes have an unobtainable least fixed and rely on widening and narrowing operations. In this talk, I present a predictable abstract-interpretation based technique for computing numerical loop summaries. The technique works by first synthesizing a rational vector addition system with resets (Q-VASR) that simulates the action of an input loop, and then uses the (polytime computable) reachability relation of Q-VASRs to over-approximate the behavior of the loop. The key contribution presented (and the crux behind the predictability claim) is the ability to synthesize a Q-VASR that is a best abstraction of a LRA loop in the sense that (1) it simulates the loop and (2) it is simulated by any other Q-VASR that simulates the loop. In addition, I present a technique for improving the precision of the analysis by using Q-VASR with states to capture loop control structure. These techniques have been benchmarked against state-of-the-art tools; experiments show that these techniques are both precise and performant. The reading list papers are C. Calcagno, D. Distefano, P. W. O’Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction, in: Proc. Symposium on Principles of Programming Languages (POPL ’09), pages 289–300. ACM Press, 2009. M. Colon, S. Sankaranarayanan, and H. Sipma, Linear invariant generation using non-linear constraint solving, in: International Conference on Computer-Aided Verification (CAV ‘03), pages 420–432 P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proc. Symposium on Principles of Programming Languages (POPL ‘77). ACM Press, New York, 1977. A. Farzan and Z. Kincaid. Compositional Recurrence Analysis. In: Proc Formal Methods in Computer-Aided Design (FMCAD ’15). C. Haase and S. Halfon. Integer vector addition systems with states. in Proc: International Workshop on Reachability Problems (RP ‘14), volume 8762 of Lecture Notes in Computer Science, pages 112–124. Springer, 2014 F. Konecny. PTIME computation of transitive closures of octagonal relations. in Proc: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016). K. L. McMillan. Lazy abstraction with interpolants. in: Proc International Conference on Computer-Aided Verification (CAV ‘06), pages 123–136. Springer-Verlag, Berlin, Germany, M. Müller-Olm and H. Seidl. Precise interprocedural analysis through linear algebra. in Proc: Symposium on Principles of Programming Languages (POPL ’04). T. Reps, S. Horwitz and M. Sagiv, Precise interprocedural dataflow analysis via graph reachability, in Proc: ACM Symposium on Principles of Programming Languages (POPL ‘95), pages 49-61. T. Reps, M. Sagiv, and G. Yorsh. Symbolic implementation of the best transformer. in Proc. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI ‘04). R. E. Tarjan, A unified approach to path problems, J. ACM, 28(3), 577–593 (1981). The reading list books are A.R. Bradley, Z. Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Heidelberg (2007) F. Nielson, H. Riis Nielson, and C. Hankin, Principles of Program Analysis, Springer-Verlag, 1999.

1 0

Michael Uhlar and Sathya Gunasekar from Facebook, Friday, May 3
by Emily C. Lawrence 29 Apr '19

29 Apr '19

Michael Uhlar and Sathya Gunasekar from Facebook Friday, May 3 at 12:30pm Computer Science - Room 104 (large auditorium) [ https://www.cs.princeton.edu/events/25851 | https://www.cs.princeton.edu/events/25851 ] CacheLib - Unifying & Abstracting HW for caching @ Facebook In order to operate with high efficiency, Facebook’s infrastructure relies on caching in many different backend services. These services place very different demands on their caches, e.g., in terms of working set sizes, access patterns, and throughput requirements. Historically, each service used a different cache implementation, leading to inefficiency, duplicated code and effort. CacheLib is an embedded caching engine, which addresses this requirement with a unified API for building a cache implementation across many HW mediums. CacheLib transparently combines volatile and non-volatile storage in a single caching abstraction. To meet the varied demands, CacheLib successfully provides a flexible, high-performance solution for many different services at Facebook. In this talk, we describe CacheLib’s design, challenges, and several lessons learned.

1 0

Bill Buxton Seminar, Monday April 29, 4:30pm. Friend Convocation Room
by Margaret Martonosi 26 Apr '19

26 Apr '19

Hello all- Dr. Bill Buxton, Principal Researcher at Microsoft, will be on campus Monday April 29. He’s giving a seminar at 4:30pm in the Friend Convocation room and we really hope lots of you will be there. Please forward to students as well, particularly those interested in Graphics, HCI, and Design. thanks, mrm > Buxton-Microsoft Collection On the Importance of History Shaping the Future > Monday, April 29th 4:30pm > Friend Center, Convocation Room > Speaker: Bill Buxton, Principal Researcher at Microsoft Research > Free and open to the public. Registration required. > > https://www.tfaforms.com/4734441 > > History, backed up by current data, tells us that what we perceive as rapid technological change is generally due to a large number of technologies evolving slowly. > > Over the past 45 years I have accumulated a collection of gadgets that captures the history of technological growth. For you, the value may just be nostalgia. However, my hope is this. In this age where the things which we produce create such a strong cultural impact, can we really afford not to take advantage of the learnings of the past hidden in plain sight? > > BIO > A Principal Researcher at Microsoft Research, Bill has had a 40- year involvement in research, practice and commentary around design, innovation and human aspects of technology. Following a 20-year career as a professional musician, he morphed into a researcher and interaction designer, at the University of Toronto, Xerox PARC, Alias Research and SGI Inc. He has been awarded four honourary doctorates, is co-recipient of an Academy Award for Scientific and Technical Achievement, received an ACM/SIGCHI Lifetime Achievement Award, and is a Fellow of the ACM. Bill has published, lectured and consulted widely, and is an Adjunct Professor at the University of Toronto, and a Distinguished Professor of Industrial Design at the Technical University Eindhoven. Other than his family, mountains and rivers are his first love. For more information, see billbuxton.com Margaret Martonosi H. T. Adams '35 Professor of Computer Science. Director, Keller Center for Innovation in Engineering Education Princeton University ■ mrm(a)princeton.edu ■ http://www.princeton.edu/~mrm

1 0