- talks - lists.cs.princeton.edu

Reminder: Colloquium Speaker Ravi Netravali, tomorrow at 12:30pm
by Emily C. Lawrence 22 Mar '20

22 Mar '20

CS Colloquium Speaker Speaker: Ravi Netravali, University of California, Los Angeles Date: Monday, March 23 - 12:30pm Host: Karthik Narasimhan Location: Remote via Zoom Link: https://princeton.zoom.us/j/645162020 Event page: https://www.cs.princeton.edu/events/25925 ***Due to the developing situation surrounding the COVID-19 virus, this talk will be available for remote viewing. See below for details.*** Title: Improving Stack-Wide Resource Utilization for a Faster Mobile Web Abstract: Mobile web pages are integral to today's society, supporting critical services such as education, e-commerce, and social networking. Despite considerable academic and industrial research efforts, and major improvements over the past decade across the client-side web stack (i.e., networks, device CPUs, and browser engines), page load performance has plateaued and continues to fall short of user performance demands in practice. The consequences of this are far reaching: users abandon pages early, costing content providers billions of dollars in lost revenue; or pages are unusably slow, particularly in developing regions where web pages are often the sole gateway to the aforementioned services. In this talk, I will describe the origin of this performance plateau in the context of serialized page load tasks that preclude effective utilization of the underlying network and CPU resources. Then, I will describe two complementary optimizations that my students and I have developed to eliminate these inefficiencies throughout the page load process and cut mobile load times in half. Key to these optimizations are judicious applications of programming languages (e.g., symbolic execution) and machine learning (e.g., reinforcement learning) techniques that enable us to 1) discover optimization knobs that preserve application correctness, and 2) tune those knobs according to stack-wide signals from the network, device, page, and browser, without developer intervention. I will conclude by describing how these underlying techniques can motivate and address a range of future challenges in networked applications and distributed systems. Bio: Ravi Netravali is an Assistant Professor of Computer Science at UCLA. His research interests are broadly in computer systems and networking, with a recent focus on building practical systems to improve the performance and debugging of large-scale, distributed applications for both end users and developers. His research has been recognized with an NSF CAREER Award, a Google Faculty Research Award, an ACM SoCC Best Paper Award, and an IRTF Applied Networking Research Prize. Prior to joining UCLA, Netravali received a PhD in Computer Science from MIT in 2018. Zoom information: Topic: Ravi Netravali CS Seminar Time: Mar 23, 2020 12:00 PM Eastern Time (US and Canada) Join Zoom Meeting https://princeton.zoom.us/j/645162020 Meeting ID: 645 162 020 One tap mobile +13126266799,,645162020# US (Chicago) +16465588656,,645162020# US (New York) Dial by your location +1 312 626 6799 US (Chicago) +1 646 558 8656 US (New York) +1 253 215 8782 US +1 301 715 8592 US +1 346 248 7799 US (Houston) +1 669 900 6833 US (San Jose) Meeting ID: 645 162 020 Find your local number: https://princeton.zoom.us/u/avcvlf1F3 Join by SIP 645162020(a)zoomcrc.com Join by H.323 162.255.37.11 (US West) 162.255.36.11 (US East) 221.122.88.195 (China) 115.114.131.7 (India Mumbai) 115.114.115.7 (India Hyderabad) 213.19.144.110 (EMEA) 103.122.166.55 (Australia) 209.9.211.110 (Hong Kong) 64.211.144.160 (Brazil) 69.174.57.160 (Canada) 207.226.132.110 (Japan) Meeting ID: 645 162 020

1 0

Anders Miltner will present his Pre FPO on Tuesday, March 24, 2020 at 11am
by Nicki Mahler 18 Mar '20

18 Mar '20

Anders Miltner will present his Pre FPO on Tuesday, March 24, 2020 at 11am. To attend the talk, you may log into the following Zoom Meeting: [ https://princeton.zoom.us/j/525520011 | https://princeton.zoom.us/j/525520011 ] The members of his committee are as follows: David Walker (reader, adviser); Kathleen Fisher (reader - Tufts University), Andrew Appel (examiner), Aarti Gupta (examiner), and Zak Kincaid (examiner) All are welcome to attend. Please see abstract below. Bidirectional transformations are groupings of transformations between pairs of data representations. A particularly well-studied class of bidirectional transformations are lenses, bidirectional transformations that satisfy a set of “round-tripping laws”. Lenses can implement serializer/deserializer pairs, parser/pretty printer pairs, and incremental data structure transformers. Domain-specific languages like Boomerang, Augeas, GRoundTram, BiFluX, BiYacc, Brul, BiGUL, and HOBiT allow programmers to write both transformations with a single program, and guarantee the transformations satisfy the round-tripping laws. As long as an expression is well-typed in these languages, the bidirectional transformation that expression represents is a lens. However, writing in domain-specific lens languages can be hard, requiring the user to reason about fiddly details of the transformations within the context of a complex type system. In this work we introduce Optician, which provides an alternative method of developing lenses – synthesis. We develop a synthesis engine for Boomerang, a lens language for string transformations. Pairs of regular expressions serve as types for Boomerang lenses, which transform between the languages of those regular expressions. Instead of manually writing Boomerang lenses, programmers merely need to provide the type of the desired lens and a set of input/output examples describing the lens’s behavior. Optician will then synthesize a lens between the provided types that exhibits the demonstrated behavior. We demonstrate how to synthesize three classes of lenses: bijective lenses, symmetric lenses, and quotient lenses. Bijective lenses encode bijections, symmetric lenses encode bidirectional transformations that permit losing information when going from one format to another, and quotient lenses satisfy the round-tripping laws modulo an equivalence relation. We define a synthesizer that involves two cooperating procedures. One procedure proposes a candidate spaces of lenses, the second procedures searches through that space. To synthesize symmetric lenses, regular expressions are augmented with probability distributions, and the synthesis algorithm aims to avoid information loss. To synthesize quotient lenses, regular expressions are augmented with equivalence information, and the synthesizer generates lenses between the representative elements of the equivalence classes. We evaluate Optician from a variety of benchmarks taken from the lens and synthesis literature, and find that we are able to synthesize all the lenses in our benchmark suite. We have integrated Optician into the Boomerang codebase, enabling users to either synthesize their lenses or write them by hand. Join Zoom Meeting [ https://princeton.zoom.us/j/525520011 | https://princeton.zoom.us/j/525520011 ]

1 0

Colloquium Speaker Ravi Netravali, Monday, Mar 23 at 12:30pm
by Emily C. Lawrence 16 Mar '20

16 Mar '20

CS Colloquium Speaker Speaker: Ravi Netravali, University of California, Los Angeles Date: Monday, March 23 - 12:30pm Host: Karthik Narasimhan Location: Remote via Zoom Link: https://princeton.zoom.us/j/645162020 Event page: https://www.cs.princeton.edu/events/25925 ***Due to the developing situation surrounding the COVID-19 virus, this talk will be available for remote viewing. See below for details.*** Title: Improving Stack-Wide Resource Utilization for a Faster Mobile Web Abstract: Mobile web pages are integral to today's society, supporting critical services such as education, e-commerce, and social networking. Despite considerable academic and industrial research efforts, and major improvements over the past decade across the client-side web stack (i.e., networks, device CPUs, and browser engines), page load performance has plateaued and continues to fall short of user performance demands in practice. The consequences of this are far reaching: users abandon pages early, costing content providers billions of dollars in lost revenue; or pages are unusably slow, particularly in developing regions where web pages are often the sole gateway to the aforementioned services. In this talk, I will describe the origin of this performance plateau in the context of serialized page load tasks that preclude effective utilization of the underlying network and CPU resources. Then, I will describe two complementary optimizations that my students and I have developed to eliminate these inefficiencies throughout the page load process and cut mobile load times in half. Key to these optimizations are judicious applications of programming languages (e.g., symbolic execution) and machine learning (e.g., reinforcement learning) techniques that enable us to 1) discover optimization knobs that preserve application correctness, and 2) tune those knobs according to stack-wide signals from the network, device, page, and browser, without developer intervention. I will conclude by describing how these underlying techniques can motivate and address a range of future challenges in networked applications and distributed systems. Bio: Ravi Netravali is an Assistant Professor of Computer Science at UCLA. His research interests are broadly in computer systems and networking, with a recent focus on building practical systems to improve the performance and debugging of large-scale, distributed applications for both end users and developers. His research has been recognized with an NSF CAREER Award, a Google Faculty Research Award, an ACM SoCC Best Paper Award, and an IRTF Applied Networking Research Prize. Prior to joining UCLA, Netravali received a PhD in Computer Science from MIT in 2018. Zoom information: Topic: Ravi Netravali CS Seminar Time: Mar 23, 2020 12:00 PM Eastern Time (US and Canada) Join Zoom Meeting https://princeton.zoom.us/j/645162020 Meeting ID: 645 162 020 One tap mobile +13126266799,,645162020# US (Chicago) +16465588656,,645162020# US (New York) Dial by your location +1 312 626 6799 US (Chicago) +1 646 558 8656 US (New York) +1 253 215 8782 US +1 301 715 8592 US +1 346 248 7799 US (Houston) +1 669 900 6833 US (San Jose) Meeting ID: 645 162 020 Find your local number: https://princeton.zoom.us/u/avcvlf1F3 Join by SIP 645162020(a)zoomcrc.com Join by H.323 162.255.37.11 (US West) 162.255.36.11 (US East) 221.122.88.195 (China) 115.114.131.7 (India Mumbai) 115.114.115.7 (India Hyderabad) 213.19.144.110 (EMEA) 103.122.166.55 (Australia) 209.9.211.110 (Hong Kong) 64.211.144.160 (Brazil) 69.174.57.160 (Canada) 207.226.132.110 (Japan) Meeting ID: 645 162 020

1 0

Ruth Dannenfelser will present her FPO "Data-Driven Approaches and Systems to Interrogate Complex Disease" on Monday, 3/30/2020 at 1:00 pm in CS 301
by Nicki Mahler 13 Mar '20

13 Mar '20

Ruth Dannenfelser will present her FPO "Data-Driven Approaches and Systems to Interrogate Complex Disease" on Monday, 3/30/2020 at 1:00 pm in CS 301. The members of her committee are as follows: Olga Troyanskaya (adviser); Readers: Wendell Lim (UCSF) and Kai Li; Examiners: Yibin Kang (Mol Bio), Mona Singh, and Olga Troyanskaya. 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. The talk abstract follows below. Large-scale genomic studies now give more predictive power than ever, allowing us to profile the composition of tissues, study cellular functions, and understand organismal traits at an unprecedented level of detail. This is particularly important for studying heterogeneous diseases, such as cancer, where small patient-specific differences play critical roles in disease development and progression. As the these studies accumulate, it is increasingly important to develop methods to discover novel biology while considering tissue and cell type specificity, and develop systems to help make this data explosion easily manageable, accessible, and interpretable. Towards these goals, in this dissertation, we build off the wealth of publicly available data to examine the interplay between cancer and the immune system, then develop two query-based visualization systems that enable interactive data exploration for the wider biomedical community. The first part of this work presents two perspectives on cancer and the immune system. Using derived immune markers we found that estrogen receptor activity and genomic complexity are key factors driving changes in breast cancer lymphocytic infiltration. Our method enabled discoveries on existing samples even when this was not the original intent of the study, without the need for additional experiments. Next, we leveraged public expression data to further the development of targeted immunotherapeutics for solid tumors. Working closely with experimental collaborators, we developed a method to prioritize pairs of antigen targets that will help engineered T cells hone in on tumor targets while minimizing damage to healthy tissues. The second half covers how we can extract unbiased signals from large collections of biomedical data in the form of abstracts and repositories of transcriptomics data. We develop a method to obtain informative tissue-disease-gene relationships from abstracts and integrate them into a system that presents different snapshots of curated interactions. Next, we extend a gene expression search engine that simultaneously returns coexpressed genes and relevant datasets. Our extension expands the search space across the major model organisms and provides a new cross-organism exploration interface to help facilitate translational research. Both systems will help experimentalists leverage existing knowledge to better explain the larger implications of their specific findings.

1 0

Colloquium Speaker Adji Bousso Dieng TODAY at 12:30pm
by Emily C. Lawrence 12 Mar '20

12 Mar '20

***Due to the developing coronavirus situation, this talk will now be available for remote viewing via Zoom. See below for full details.*** CS Colloquium Speaker Adji Bousso Dieng, Columbia University Thursday, March 12 - 12:30pm Location: Zoom Meeting Link: [ https://princeton.zoom.us/j/384273957 | https://princeton.zoom.us/j/384273957 ] *see below for more info Host: Ryan Adams [ https://www.cs.princeton.edu/events/25924 | https://www.cs.princeton.edu/events/25924 ] Title: Deep Probabilistic Graphical Modeling Abstract: Deep learning (DL) is a powerful approach to modeling complex and large scale data. However, DL models lack interpretable quantities and calibrated uncertainty. In contrast, probabilistic graphical modeling (PGM) provides a framework for formulating an interpretable generative process of data and a way to express uncertainty about what we do not know. How can we develop machine learning methods that bring together the expressivity of DL with the interpretability and calibration of PGM to build flexible models endowed with an interpretable latent structure that can be fit efficiently? I call this line of research deep probabilistic graphical modeling (DPGM). In this talk, I will discuss my work on developing DPGM both on the modeling and algorithmic fronts. In the first part of the talk I will show how DPGM enables learning document representations that are highly predictive of sentiment without requiring supervision. In the second part of the talk I will describe entropy-regularized adversarial learning, a scalable and generic algorithm for fitting DPGMs. Bio: Adji Bousso Dieng is a PhD Candidate at Columbia University where she is jointly advised by David Blei and John Paisley. Her research is in Artificial Intelligence and Statistics, bridging probabilistic graphical models and deep learning. Dieng is supported by a Dean Fellowship from Columbia University. She won a Microsoft Azure Research Award and a Google PhD Fellowship in Machine Learning. She was recognized as a rising star in machine learning by the University of Maryland. Prior to Columbia, Dieng worked as a Junior Professional Associate at the World Bank. She did her undergraduate studies in France where she attended Lycee Henri IV and Telecom ParisTech --France's Grandes Ecoles system. She spent the third year of Telecom ParisTech's curriculum at Cornell University where she earned a Master in Statistics. --- Topic: Adji Bousso Dieng CS Seminar Time: Mar 12 , 2020 12:30 PM Eastern Time (US and Canada) Join Zoom Meeting [ https://princeton.zoom.us/j/384273957 | https://princeton.zoom.us/j/384273957 ] Meeting ID: 384 273 957 One tap mobile [ callto:+16465588656,,384273957 | +16465588656,,384273957 ] # US (New York) [ callto:+16699006833,,384273957 | +16699006833,,384273957 ] # US (San Jose) Dial by your location [ callto:+1 646 558 8656 | +1 646 558 8656 ] US (New York) [ callto:+1 669 900 6833 | +1 669 900 6833 ] US (San Jose) Meeting ID: 384 273 957 Find your local number: [ https://princeton.zoom.us/u/abUHt2KPwU | https://princeton.zoom.us/u/abUHt2KPwU ] Join by SIP 384273957(a)zoomcrc.com Join by H.323 [ callto:162.255.37.11 | 162.255.37.11 ] (US West) [ callto:162.255.36.11 | 162.255.36.11 ] (US East) [ callto:221.122.88.195 | 221.122.88.195 ] (China) [ callto:115.114.131.7 | 115.114.131.7 ] (India Mumbai) [ callto:115.114.115.7 | 115.114.115.7 ] (India Hyderabad) [ callto:213.19.144.110 | 213.19.144.110 ] (EMEA) [ callto:103.122.166.55 | 103.122.166.55 ] (Australia) [ callto:209.9.211.110 | 209.9.211.110 ] (Hong Kong) [ callto:64.211.144.160 | 64.211.144.160 ] (Brazil) [ callto:69.174.57.160 | 69.174.57.160 ] (Canada) [ callto:207.226.132.110 | 207.226.132.110 ] (Japan) Meeting ID: 384 273 957

1 0

Reminder: Colloquium Speaker Adji Bousso Dieng tomorrow at 12:30pm
by Emily C. Lawrence 11 Mar '20

11 Mar '20

***Due to the developing coronavirus situation, this talk will now be available for remote viewing via Zoom. See below for full details.*** CS Colloquium Speaker Adji Bousso Dieng, Columbia University Thursday, March 12 - 12:30pm Location: Zoom Meeting Link: [ https://princeton.zoom.us/j/384273957 | https://princeton.zoom.us/j/384273957 ] *see below for more info Host: Ryan Adams [ https://www.cs.princeton.edu/events/25924 | https://www.cs.princeton.edu/events/25924 ] Title: Deep Probabilistic Graphical Modeling Abstract: Deep learning (DL) is a powerful approach to modeling complex and large scale data. However, DL models lack interpretable quantities and calibrated uncertainty. In contrast, probabilistic graphical modeling (PGM) provides a framework for formulating an interpretable generative process of data and a way to express uncertainty about what we do not know. How can we develop machine learning methods that bring together the expressivity of DL with the interpretability and calibration of PGM to build flexible models endowed with an interpretable latent structure that can be fit efficiently? I call this line of research deep probabilistic graphical modeling (DPGM). In this talk, I will discuss my work on developing DPGM both on the modeling and algorithmic fronts. In the first part of the talk I will show how DPGM enables learning document representations that are highly predictive of sentiment without requiring supervision. In the second part of the talk I will describe entropy-regularized adversarial learning, a scalable and generic algorithm for fitting DPGMs. Bio: Adji Bousso Dieng is a PhD Candidate at Columbia University where she is jointly advised by David Blei and John Paisley. Her research is in Artificial Intelligence and Statistics, bridging probabilistic graphical models and deep learning. Dieng is supported by a Dean Fellowship from Columbia University. She won a Microsoft Azure Research Award and a Google PhD Fellowship in Machine Learning. She was recognized as a rising star in machine learning by the University of Maryland. Prior to Columbia, Dieng worked as a Junior Professional Associate at the World Bank. She did her undergraduate studies in France where she attended Lycee Henri IV and Telecom ParisTech --France's Grandes Ecoles system. She spent the third year of Telecom ParisTech's curriculum at Cornell University where she earned a Master in Statistics. --- Topic: Adji Bousso Dieng CS Seminar Time: Mar 12, 2020 12:30 PM Eastern Time (US and Canada) Join Zoom Meeting [ https://princeton.zoom.us/j/384273957 | https://princeton.zoom.us/j/384273957 ] Meeting ID: 384 273 957 One tap mobile +16465588656,,384273957# US (New York) +16699006833,,384273957# US (San Jose) Dial by your location +1 646 558 8656 US (New York) +1 669 900 6833 US (San Jose) Meeting ID: 384 273 957 Find your local number: https://princeton.zoom.us/u/abUHt2KPwU Join by SIP 384273957(a)zoomcrc.com Join by H.323 162.255.37.11 (US West) 162.255.36.11 (US East) 221.122.88.195 (China) 115.114.131.7 (India Mumbai) 115.114.115.7 (India Hyderabad) 213.19.144.110 (EMEA) 103.122.166.55 (Australia) 209.9.211.110 (Hong Kong) 64.211.144.160 (Brazil) 69.174.57.160 (Canada) 207.226.132.110 (Japan) Meeting ID: 384 273 957

1 0

Colloquium Speaker Wenting Zheng TODAY at 12:30pm
by Emily C. Lawrence 10 Mar '20

10 Mar '20

***Due to the developing coronavirus situation, we want to reduce the number of attendees at invited talks this week. Attendance at the following talk will now be limited to "Princeton University faculty only". For other people who want to watch the talk, it will be available by live stream only, via the Princeton Broadcast Center (link: http://bc.princeton.edu/live/7/), for individual viewing; we will not be hosting a separate room for the live stream. For members of the CS department, a recording of the talk will be made available afterwards.*** CS Colloquium Speaker Wenting Zheng, University of California, Berkeley Tuesday, March 10 - 12:30pm Computer Science - Room 105 Host: Amit Levy [ https://www.cs.princeton.edu/events/25923 | https://www.cs.princeton.edu/events/25923 ] Title: Sharing without Showing: Building Secure Collaborative Systems In many domains such as finance and medicine, organizations have encountered obstacles in data acquisition because their target applications need sensitive data that reside across multiple parties. However, such data cannot be shared today due to data privacy concerns, policy regulation, and business competition. My graduate research focused on solving this problem by enabling organizations to run complex computations on the joint dataset without revealing their sensitive input to the other parties. My overall approach is to co-design systems with cryptography to build practical and functional systems that provide strong and provable security. In this talk, I will focus on two systems — Opaque and Helen — which secure SQL analytics and machine learning, respectively. My open source has been used by organizations such as IBM Research, Ericsson, Alibaba, and Microsoft. Bio: Wenting Zheng is a Ph.D. candidate at UC Berkeley, co-advised by Raluca Ada Popa and Ion Stoica . She completed her bachelor’s and master of engineering at MIT, where she was advised by Barbara Liskov . Her research interests are in computer systems, security, and applied cryptography. She is the recipient of a Berkeley Fellowship from 2014-2016, an IBM Research fellowship from 2017-2018, and was an invited participant at the 2019 EECS Rising Stars workshop.

1 0

Colloquium Speaker Wenting Zheng tomorrow at 12:30pm - LIVESTREAM ONLY
by Emily Lawrence 09 Mar '20

09 Mar '20

***Due to the developing coronavirus situation, we want to reduce the number of attendees at invited talks this week. Attendance at the following talk will now be limited to "Princeton University faculty only". For other people who want to watch the talk, it will be available by live stream only, via the Princeton Broadcast Center (link: <http://bc.princeton.edu/live/7/> http://bc.princeton.edu/live/7/), for individual viewing; we will not be hosting a separate room for the live stream. For members of the CS department, a recording of the talk will be made available afterwards.*** Regards, Emily CS Colloquium Speaker Wenting Zheng, University of California, Berkeley Tuesday, March 10 - 12:30pm Computer Science - Room 105 Host: Amit Levy https://www.cs.princeton.edu/events/25923 Title: Sharing without Showing: Building Secure Collaborative Systems In many domains such as finance and medicine, organizations have encountered obstacles in data acquisition because their target applications need sensitive data that reside across multiple parties. However, such data cannot be shared today due to data privacy concerns, policy regulation, and business competition. My graduate research focused on solving this problem by enabling organizations to run complex computations on the joint dataset without revealing their sensitive input to the other parties. My overall approach is to co-design systems with cryptography to build practical and functional systems that provide strong and provable security. In this talk, I will focus on two systems — Opaque and Helen — which secure SQL analytics and machine learning, respectively. My open source has been used by organizations such as IBM Research, Ericsson, Alibaba, and Microsoft. Bio: Wenting Zheng is a Ph.D. candidate at UC Berkeley, co-advised by Raluca Ada Popa and Ion Stoica. She completed her bachelor’s and master of engineering at MIT, where she was advised by Barbara Liskov. Her research interests are in computer systems, security, and applied cryptography. She is the recipient of a Berkeley Fellowship from 2014-2016, an IBM Research fellowship from 2017-2018, and was an invited participant at the 2019 EECS Rising Stars workshop.

1 0

Santiago Cuellar will present his FPO "Concurrent Permission Machine for modular proofs of optimizing compilers with shared memory concurrency" on Friday, March 13, 2020 in CS 402 at 10:30am
by Nicki Mahler 09 Mar '20

09 Mar '20

Santiago Cuellar will present his FPO "Concurrent Permission Machine for modular proofs of optimizing compilers with shared memory concurrency" on Friday, March 13, 2020 in CS 402 at 10:30am. The members of his committee are Andrew Appel (adviser); Readers: Zachary Kincaid and Gil Hur (Seoul National University); Examiners: Lennart Beringer, Aarti Gupta, and Andrew Appel. A copy of his 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 his talk. The talk abstract follows below: Optimizing compilers change a program based on a formal analysis of its code, and modern processors further rearrange the program order. It is hard to reason about such transformations, which makes them a source of bugs, particularly for concurrent shared-memory programs where the order of execution is critical. On the other hand, programmers should reason about their program in the source language, which abstracts such low level details. We present the Concurrent Permission Machine (CPM), a semantic model for shared-memory concurrent programs, which is: (1) sound for higerh-order Concurrent Separation Logic, (2) convenient to reason about compiler correctness, and (3) useful for proving reduction theorems on weak memory models. The key feature of the CPM is that it exploits the fact that correct shared-memory programs are permission coherent: threads have (at any given time) noncompeting permission to access memory, and their load/store operations respect those permissions. Compilers are often written with sequential code in mind, and proving the correctness of those compilers is hard enough without concurrency. Indeed, the machinechecked proof of correctness for the CompCert C compiler was a major advance in the field. Using the CPM to conveniently distinguish sequential execution from concurrent interactions, I show how to reuse the (sequential) CompCert proof, without major changes, to guarantee a stronger concurrent-permission-aware notion of correctness

1 0

Before the colloquium, wash your hands
by Emily Lawrence 09 Mar '20

09 Mar '20

For the duration of the coronavirus emergency, before any CS department event at which lunch is served, wash your hands before getting in line for lunch. In the serving line, you touch utensils used by many others. Washing your hands is one of the most effective ways of limiting the spread of the virus. Here's how <https://www.cdc.gov/handwashing/when-how-handwashing.html> : Follow these five steps every time. 1. Wet your hands with clean, running water (warm or cold), turn off the tap, and apply soap. 2. Lather your hands by rubbing them together with the soap. Lather the backs of your hands, between your fingers, and under your nails. 3. Scrub your hands for at least 20 seconds. Need a timer? Hum the “Happy Birthday” song from beginning to end twice. 4. Rinse your hands well under clean, running water. 5. Dry your hands using a clean towel or air dry them. (And then, between washing your hands and filling your plate, don't touch your face...) This starts with today's colloquium.

1 0