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

Zoe Paraskevopoulou will present her FPO "Verified Optimizations for Functional Languages" on Friday, 10/30/2020 at 3pm via Zoom.
by Nicki Mahler 23 Oct '20

23 Oct '20

Zoe Paraskevopoulou will present her FPO "Verified Optimizations for Functional Languages" on Friday, 10/30/2020 at 3pm via Zoom. Zoom link: [ https://princeton.zoom.us/j/5655804837 | https://princeton.zoom.us/j/5655804837 ] The members of her committee are as follows: Andrew Appel (Adviser); Readers: Davis Walker and Amal Ahmed (Northeastern University); Examiners: Zachary Kincaid, Aarti Gupta, Davis Walker, Andrew Appel, Amal Ahmed (Northeastern University) A copy of her thesis is available upon request. Please email ngotsis(a)cs.princeton if you would like a copy of the thesis. Everyone is invited to attend her talk. Abstract follows below: Coq is one of the most widely adopted proof development systems. It allows programmers to write purely functional programs and verify them against specifications with machine-checked proofs. After verification, one can use Coq’s extraction plugin to obtain a certified program (in OCaml, Haskell, or Scheme) that can be compiled and executed. However, bugs in either the extraction function or the compiler of the extraction language, can render source level verification useless. A verified compiler is a compiler whose output provably preserves the semantics of the source language. CertiCoq is a currently developed verified compiler for Gallina, Coq’s specification language. With CertiCoq, one could obtain an executable program that has is guaranteed to have the same behavior as the source program, bridging the gap between the formally verified source program and the executable. In this thesis, I present the implementation and verification of CertiCoq’s optimizing middle-end pipeline. CertiCoq’s middle end consists of seven di↵erent transformations and is responsible for eciently compiling an untyped purely functional intermediate language to a first-order subset of this language, which can be readily compiled to a first-order, low-level intermediate language. CertiCoq’s middle-end pipeline performs crucial optimizations for functional languages including closure conversion, uncurrying, shrink-reduction and inlining. It advances the state of the art of verified optimizing compilers for functional languages by implementing ecient closure-allocation strategies. For proving CertiCoq correct, I develop a framework based on the technique of logical relations, making novel technical contributions. I extend the logical relation with notions of precondition and postcondition showing how it can be used to reason about intensional properties of programs simultaneously with extensional properties. I demonstrate how this allows reasoning about divergence preservation, which is not supported by traditional logical relations. I develop a novel, lightweight technique that allows logical-relation proofs to be composed, enabling verified separate compilation of programs compiled with CertiCoq using di↵erent sets of optimizations. Lastly, I use the framework to prove that CertiCoq’s closure conversion is not only functionally correct but also safe for time and space, meaning that it is guaranteed to preserve the asymptotic time and space complexity of the source program.

1 0

Malte Moeser will present his Pre- FPO on Wednesday, October 28, 2020 via Zoom
by Nicki Mahler 21 Oct '20

21 Oct '20

Malte Moeser will present his Pre- FPO on Wednesday, October 28, 2020 via Zoom. Zoom link: [ https://princeton.zoom.us/j/92656073526 | https://princeton.zoom.us/j/92656073526 ] The members of his committee are as follows: Arvind Narayanan (advisor and examiner) Jonathan Mayer (examiner) Nicolas Christin (Carnegie Mellon University, examiner) Matt Weinberg (reader) Rainer Böhme (University of Innsbruck, reader) Link to abstract below: [ https://docs.google.com/document/d/1D6mJuNFLJRdfVIcr94jht1Vsk4kkM4bhB0PrXvD… | https://docs.google.com/document/d/1D6mJuNFLJRdfVIcr94jht1Vsk4kkM4bhB0PrXvD… ]

1 0

Laura Roberts will present her FPO, "Internet Measurement for the Prevention and Detection of Internet Surveillance" on Wednesday, 10/28/2020 at 2pm via Zoom.
by Nicki Mahler 21 Oct '20

21 Oct '20

Laura Roberts will present her FPO, "Internet Measurement for the Prevention and Detection of Internet Surveillance" on Wednesday, 10/28/2020 at 2pm via Zoom. Zoom link: [ https://princeton.zoom.us/j/96919654569 | https://princeton.zoom.us/j/96919654569 ] The members of her committee are as follows: Ed Felten (adviser); Readers: Prateek Mittal and Jonathan Mayer; Examiners: Jennifer Rexford, Arvind Narayanan, and Ed Felten. A copy of her thesis is available upon request. Please email ngotsis(a)cs.princeton if you would like a copy of the thesis. Everyone is invited to attend her talk. Abstract follows below: Surveillance is a tactic of societal control: Observation of people’s behavior allows the observer to manipulate and steer people’s future behavior in a way that serves the observer’s interests. With new technologies come new, easier ways of surveilling people. This dissertation concerns itself with Internet technologies in particular and presents how Internet measurement can be used to prevent and detect Internet surveillance. "Internet surveillance" is the observation of people’s online activities. "Internet measurement" comprises technical means of measuring interesting characteristics of the Internet (e.g. packet round-trip time, protocol usage, etc.) in order to gain better understanding of the Internet and improve its performance, security, etc. So in other words, this dissertation presents how various Internet measurement techniques can be used for preventing and detecting the observation of people’s online activities. In order to achieve the goal of preventing surveillance, we use Internet measurement techniques to strengthen the Tor anonymity network (a system that seeks to thwart Internet surveillance and censorship) by exposing vulnerabilities and suggesting possible solutions. In order to achieve the goal of detecting surveillance, we develop a proof of concept system that uses Internet measurement techniques to catch surveillants.

1 0

Friday, Oct 23 talk by Whitney Quesenbery, Center for Civic Design
by Emily C. Lawrence 20 Oct '20

20 Oct '20

The Electoral Innovation Lab at Princeton University presents a Friday Forum: Election Reform as a Design Challenge, featuring Whitney Quesenbery, Executive Director of the Center for Civic Design. Friday, October 23, at 1:30pm EDT via Zoom: [ https://princeton.zoom.us/j/273691213 | https://princeton.zoom.us/j/273691213 ] Please RSVP to [ mailto:coopersmith@princeton.edu | coopersmith(a)princeton.edu ] About the speaker: Whitney Quesenbery works with election offices around the country to improve the voter experience and introduce best practices for election design. Her work in civic design began with her appointment to the US Election Assistance Commission (EAC) federal advisory committee writing the Voluntary Voting System Guidelines, including the first usability requirements for voting systems. She is a co-author of the Brennan Center for Justice’s seminal publication, Better Ballots , and an expert in their Ballot Design project. As the coordinator for the EAC-funded Accessible Voting Technology Initiative, she has managed 15 grants on voting for people with disabilities, including the development of the Anywhere Ballot. Among her many professional commitments, Quesenbery is a member of the Election Modernization Advisory Committee for the state of Michigan.

1 0

Ashwini Raina will present his General Exam, "Read-Aware LSM for Disaggregated Heterogeneous Storage" on Monday, October 26, 2020 at 8:30am via Zoom.
by Nicki Mahler 19 Oct '20

19 Oct '20

Ashwini Raina will present his General Exam "Read-Aware LSM for Disaggregated Heterogeneous Storage" on Monday, October 26, 2020 at 8:30am via Zoom. Zoom link: [ https://princeton.zoom.us/j/94253551655 | https://princeton.zoom.us/j/94253551655 ] The members of his committee are as follows: Michael Freedman, Kyle Jamieson, and Wyatt Lloyd Link to Abstract and Reading List: [ https://docs.google.com/document/d/1tKGtWXGrKuzJbkGBw3Ite6t4gvUBjo0S5i9-Q8c… | https://docs.google.com/document/d/1tKGtWXGrKuzJbkGBw3Ite6t4gvUBjo0S5i9-Q8c… ] [ https://docs.google.com/document/d/1i_AaAf-P7_LxNugxrgNeRjaki6NVn27FmoXvN5W… | https://docs.google.com/document/d/1i_AaAf-P7_LxNugxrgNeRjaki6NVn27FmoXvN5W… ] Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

1 0

Reminder: ACEE Seminar tomorrow at 12:30 p.m.: Adam Wierman, Caltech
by Emily C. Lawrence 14 Oct '20

14 Oct '20

Adam Wierman , professor of computing and mathematical sciences at Caltech, will present “Online Optimization & Energy” as part of the 2020/2021 Andlinger Center Highlight Seminar Series. Oct 15, 2020 12:30 PM (ET) Register here: [ https://princeton.zoom.us/webinar/register/WN_lEqS6LEqQueku0tG72vBIg | https://princeton.zoom.us/webinar/register/WN_lEqS6LEqQueku0tG72vBIg ] TITLE Online Optimization & Energy ABSTRACT Online optimization is a powerful framework in machine learning that has numerous applications to problems in energy and sustainability. In my group at Caltech, we began by applying online optimization to ‘right-size’ capacity in data centers nearly a decade ago; and by now, tools from online optimization have been applied to develop algorithms for geographical load balancing among data centers, demand response, generation planning, energy storage management, and beyond. In this talk, I will highlight both the applications of online optimization and the theoretical progress that has been driven by applications in energy and sustainability. Over the last decade, we have moved from designing algorithms for one-dimensional problems with restrictive assumptions on costs to general results for high-dimensional, non-convex problems that highlight the role of constraints, predictions, delay, multi-timescale control, and more. BIO Adam Wierman is a Professor in the Department of Computing and Mathematical Sciences (CMS) at the California Institute of Technology. He is the director of the Information Science and Technology (IST) initiative and served as executive officer (a.k.a. department chair) of CMS from 2015-2020. He received his Ph.D., M.Sc. and B.Sc. in Computer Science from Carnegie Mellon University in 2007, 2004, and 2001, respectively, and has been a faculty member at Caltech since 2007. Wierman’s research strives to make the networked systems that govern our world sustainable and resilient. He develops new mathematical tools in machine learning, optimization, control, and economics and applies these tools to design new algorithms and markets that can be deployed in data centers, the electricity grid, transportation systems, and beyond. He is best known for his work spearheading the design of algorithms for sustainable data centers, which led to significant industry adoption and for which he was named a Computerworld Honors Laureate. He is a recipient of multiple awards, including the ACM SIGMETRICS Rising Star award, the IEEE Communications Society William R. Bennett Prize, an NSF Career award, and multiple teaching awards. He is also a coauthor on papers that have received best paper awards at a wide variety of conferences across computer science, power engineering, and operations research including ACM Sigmetrics, IEEE INFOCOM, IFIP Performance, and IEEE PES.

1 0

Nataly Brukhim will present her General Exam on Friday, October 23, 2020 at 3pm via Zoom.
by Nicki Mahler 13 Oct '20

13 Oct '20

Nataly Brukhim will present her General Exam on Friday, October 23, 2020 at 3pm via Zoom. Zoom link: https://princeton.zoom.us/j/98433840220 The members of her committee are as follows: Elad Hazan (adviser), Sanjeev Arora, and Robert Schapire Link to Abstract and Reading list: https://drive.google.com/file/d/1tj_qyC2mTdhYZxEe_Zy-eAYuYo5E9zmY/view?usp=… https://drive.google.com/file/d/1W8Q_Op0B8LW5AsZOwhxPX2xSce78w0Cj/view?usp=… Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

1 0

Elena Lucherini will present her General Exam "An Agent-Based Modeling framework to study socio-technical systems" on Friday, October 16, 2020 at 9am via Zoom
by Nicki Mahler 13 Oct '20

13 Oct '20

Elena Lucherini will present her General Exam "An Agent-Based Modeling framework to study socio-technical systems" on Friday, October 16, 2020 at 9am via Zoom. Zoom link: [ https://princeton.zoom.us/j/3276145367 | https://princeton.zoom.us/j/3276145367 ] The members of her committee are as follows: Arvind Narayanan (adviser), Brandon Stewart, and Barbara Engelhardt Link to Abstract and Reading list: [ https://docs.google.com/document/d/1sxCbAAMkcjMVsjSCv8FfLSFlVpOHc3QxWzE_85x… | https://docs.google.com/document/d/1sxCbAAMkcjMVsjSCv8FfLSFlVpOHc3QxWzE_85x… ] [ https://docs.google.com/document/d/1aHd1vfvZVYsWqKx9X7TJ4U7tdsOXDEGQglLmDUK… | https://docs.google.com/document/d/1aHd1vfvZVYsWqKx9X7TJ4U7tdsOXDEGQglLmDUK… ] Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

1 1

Edgar Minasyan will present his General Exam “Adaptive Regret for Control of Time-Varying Dynamics” on Thursday, October 15, 2020 at 10am via Zoom.
by Nicki Mahler 13 Oct '20

13 Oct '20

Edgar Minasyan will present his General Exam “Adaptive Regret for Control of Time-Varying Dynamics” on Thursday, October 15, 2020 at 10am via Zoom. Zoom link: [ https://princeton.zoom.us/j/6709784080 | https://princeton.zoom.us/j/6709784080 ] The members of his committee are as follows: Elad Hazan (adviser), Sanjeev Arora, and Mark Braverman Link to Abstract and Reading list: [ https://docs.google.com/document/d/1yxsZTKWAXhSwRf4i2je8C_gnpFFA7ccDAojhEqQ… | https://docs.google.com/document/d/1yxsZTKWAXhSwRf4i2je8C_gnpFFA7ccDAojhEqQ… ] [ https://docs.google.com/document/d/1bqlE6qJSZ9MIAG0CQdf645iWcGYOTgQOKkycSA4… | https://docs.google.com/document/d/1bqlE6qJSZ9MIAG0CQdf645iWcGYOTgQOKkycSA4… ] Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

1 0

Rachit Dubey will present his General Exam "Exploring the utility of happiness for adaptive agents" on Friday, October 23, 2020 at 12pm via Zoom.
by Nicki Mahler 12 Oct '20

12 Oct '20

Rachit Dubey will present his General Exam "Exploring the utility of happiness for adaptive agents" on Friday, October 23, 2020 at 12pm via Zoom. Zoom link: [ https://princeton.zoom.us/j/97484920081 | https://princeton.zoom.us/j/97484920081 ] The members of his committee are as follows: Tom Griffiths (Adviser), Jonathan Cohen, and Karthik Narasimhan Link to Abstract and Reading list: [ https://docs.google.com/document/d/1kO_3KIURooXDnALPZ5B8fs_snn_T5A8y4UOm6pr… | https://docs.google.com/document/d/1kO_3KIURooXDnALPZ5B8fs_snn_T5A8y4UOm6pr… ] Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.

1 0