- talks - lists.cs.princeton.edu

Qinxiang Cao will present his Pre FPO, "Separation-logic-based program verification in Coq" on Thursday, December 14th, 2017 at 8am in CS 402.
by Nicki Gotsis 27 Nov '17

27 Nov '17

Qinxiang Cao will present his Pre FPO, "Separation-logic-based program verification in Coq" on Thursday, December 14th, 2017 at 8am in CS 402. The members of his committee are as follows: Andrew W. Appel (advisor), Lars Birkedal (Aarhus University), Zachary Kincaid (reader), Aarti Gupta (non-reader) and Lennart Beringer (non-reader). Everyone is welcome to join. Talk title and abstract follow below. "Separation-logic-based program verification in Coq" Abstract In our interconnected world, software bugs can seriously compromise our safety and security. To provide adequate safety or protection, security-critical kernels (of large systems) must be functionally correct. To ensure functional correctness of C programs, we can use Hoare logic and its extensions such as separation logic. But such correctness proofs are large and complex enough that we cannot trust them unless they are machine-checked. This dissertation shows how we can construct mechanized proofs of program correctness using separation logic. I answer three questions: How shall we specify our programs? How shall we prove our programs’ correctness w.r.t. their specifications? How shall we mechanize such correctness proofs? In this dissertation, I present practical techniques for separation-logic-based program verification and demonstrate them on several examples. I introduce VST-Floyd, a tool for users to build formal C program correctness proofs in Coq using separation logic. VST-Floyd is built based on Verifiable C, a proved sound separation logic; I show how to reformulate its rules to make them practical for use in verification. Finally, I introduce a unifying semantics in separation logic so that research results of one separation logic can be generalized to all separation logics. Thus the techniques used in VST-Floyd can be used in other separation logics in the future.

1 0

Distinguished Colloquium Speaker James Landay Friday Dec 1
by Emily Lawrence 27 Nov '17

27 Nov '17

Distinguished Colloquium Speaker Prof. James A. Landay, Stanford University Friday, December 1, 2017 - 12:30pm Computer Science - Room 105 Host: Prof. Olga Russakovsky "From On Body to Out of Body User Experience" Today's most common user interfaces represent an incremental change from the GUI popularized by the Apple Macintosh in 1984. Over the last 30 years the dominant hardware has changed drastically while the user interface has barely moved: from one hand on a mouse to two fingers on a panel of glass. I will illustrate how we are building on-body interfaces of the future that further engage our bodies by using muscle sensing for input and vibrotactile output, offering discrete and natural interaction on the go. I will also show how other interfaces we are designing take an even more radical approach, moving the interface off the human body altogether and onto drones that project into the space around them. Finally, I will introduce a new project where we envision buildings as hybrid physical-digital spaces that both sense and actuate to improve human wellbeing. Bio: James Landay is a Professor of Computer Science and the Anand Rajaraman and Venky Harinarayan Professor in the School of Engineering at Stanford University. He specializes in human-computer interaction. He is the founder and co-director of the World Lab, a joint research and educational effort with Tsinghua University in Beijing. Previously, Landay was a Professor of Information Science at Cornell Tech in New York City and prior to that he was a Professor of Computer Science & Engineering at the University of Washington and a Professor in EECS at UC Berkeley. From 2003 through 2006 he was the Laboratory Director of Intel Labs Seattle, a university affiliated research lab that explored the new usage models, applications, and technology for ubiquitous computing. He was also the chief scientist and co-founder of NetRaker, which was acquired by KeyNote Systems in 2004. Landay received his BS in EECS from UC Berkeley in 1990, and MS and PhD in Computer Science from Carnegie Mellon University in 1993 and 1996, respectively. He is a member of the ACM SIGCHI Academy and he is an ACM Fellow.

1 0

Reminder: Distinguished Colloquium Speaker Mary Czerwinski TODAY at 12:30
by Emily Lawrence 20 Nov '17

20 Nov '17

Distinguished Colloquium Speaker Dr. Mary Czerwinski from Microsoft Research Monday, November 20, 2017 - 12:30pm Computer Science - Room 105 Host: Szymon Rusinkiewicz Abstract: Affective computing is emerging as an important field in the design of emotional, intelligent, conversational agents that can be used in the healthcare arena, but also in everyday life. In addition, ubiquitous recording, both in the field and in the doctor's office/patient's home, has influenced how we think about wellbeing in the future. In our research, we use sensing technologies to develop contextualized and precise delivery of interventions, both in terms of the content and in the timing the intervention delivery, using machine learning algorithms. I will discuss how we use affective computing technologies to deliver just in time health interventions for improved health and for personal, behavioral reflection. For example, I will describe the Entendre project, which has implications for the design of visual feedback to encourage empathic patient-centered communication. I will also talk about ParentGuardian, a wearable sensing system that delivers just in time interventions to parents with ADHD children. In addition, I'll present our findings from two applications that deliver interventions and skills from psychology for coping with conditions ranging from general stress and depression to serious mental illness, like the intent to commit suicide, using conversational agents that users trust. Finally, I'll briefly touch on some of our designs for helping users to reflect on their daily behaviors in order to improve general well-being. Bio: Dr. Mary Czerwinski is a Principle Researcher and Research Manager of the Visualization and Interaction (VIBE) Research Group. Mary's latest research focuses primarily on emotion tracking and intervention design and delivery, information worker task management and health and wellness for individuals and groups. Her research background is in visual attention and multitasking. She holds a Ph.D. in Cognitive Psychology from Indiana University in Bloomington. Mary was awarded the ACM SIGCHI Lifetime Service Award, was inducted into the CHI Academy, and became an ACM Distinguished Scientist in 2010. She also received the Distinguished Alumni award from Indiana University's Brain and Psychological Sciences department in 2014. Mary became a Fellow of the ACM in 2016.

1 0

Colloquium Speaker Christopher Manning,TODAY at 12:30
by Emily Lawrence 16 Nov '17

16 Nov '17

Colloquium Speaker Prof. Christopher Manning, from Stanford University Thursday, November 16, 2017 - 12:30pm Computer Science - Room 105 Host: Dr. Sanjeev Arora *Please note, arrive early as seating and lunch may run out. Deep learning has had enormous success on perceptual tasks but still struggles in providing a model for inference. To address this gap, we have been developing Compositional Attention Networks (CANs). The CAN design provides a strong prior for explicitly iterative reasoning, enabling it to support explainable and structured learning, as well as generalization from a modest amount of data. The model builds on the great success of existing recurrent cells such as LSTMs: A CAN is a sequence of a single recurrent Memory, Attention, and Control (MAC) cell, and by careful design imposes structural constraints on the operation of each cell and the interactions between them, incorporating explicit control and soft attention mechanisms into their interfaces. We demonstrate the model's strength and robustness on the challenging CLEVR dataset for visual reasoning (Johnson et al. 2016), achieving a new state-of-the-art 98.9% accuracy, halving the error rate of the previous best model. More importantly, we show that the new model is more computationally efficient and data-efficient, requiring an order of magnitude less time and/or data to achieve good results. Joint work with Drew Arad. Bio: Christopher Manning is the Thomas M. Siebel Professor in Machine Learning, Linguistics and Computer Science at Stanford University. He works on software that can intelligently process, understand, and generate human language material. He is a leader in applying Deep Learning to Natural Language Processing, including exploring Tree Recursive Neural Networks, sentiment analysis, neural network dependency parsing, the GloVe model of word vectors, neural machine translation, and deep language understanding. He also focuses on computational linguistic approaches to parsing, robust textual inference and multilingual language processing, including being a principal developer of Stanford Dependencies and Universal Dependencies. Manning is an ACM Fellow, a AAAI Fellow, an ACL Fellow, and a Past President of ACL. He has coauthored leading textbooks on statistical natural language processing and information retrieval. He is a member of the Stanford NLP group (@stanfordnlp) and manages development of the Stanford CoreNLP software.

1 0

CORRECTION: Distinguished Colloquium Speaker Mary Czerwinski MONDAY Nov 20
by Emily Lawrence 15 Nov '17

15 Nov '17

Correction: This event in on MONDAY, Nov 20. Distinguished Colloquium Speaker Dr. Mary Czerwinski from Microsoft Research MONDAY, November 20, 2017 - 12:30pm Computer Science - Room 105 Host: Szymon Rusinkiewicz Abstract: Affective computing is emerging as an important field in the design of emotional, intelligent, conversational agents that can be used in the healthcare arena, but also in everyday life. In addition, ubiquitous recording, both in the field and in the doctor's office/patient's home, has influenced how we think about wellbeing in the future. In our research, we use sensing technologies to develop contextualized and precise delivery of interventions, both in terms of the content and in the timing the intervention delivery, using machine learning algorithms. I will discuss how we use affective computing technologies to deliver just in time health interventions for improved health and for personal, behavioral reflection. For example, I will describe the Entendre project, which has implications for the design of visual feedback to encourage empathic patient-centered communication. I will also talk about ParentGuardian, a wearable sensing system that delivers just in time interventions to parents with ADHD children. In addition, I'll present our findings from two applications that deliver interventions and skills from psychology for coping with conditions ranging from general stress and depression to serious mental illness, like the intent to commit suicide, using conversational agents that users trust. Finally, I'll briefly touch on some of our designs for helping users to reflect on their daily behaviors in order to improve general well-being. Bio: Dr. Mary Czerwinski is a Principle Researcher and Research Manager of the Visualization and Interaction (VIBE) Research Group. Mary's latest research focuses primarily on emotion tracking and intervention design and delivery, information worker task management and health and wellness for individuals and groups. Her research background is in visual attention and multitasking. She holds a Ph.D. in Cognitive Psychology from Indiana University in Bloomington. Mary was awarded the ACM SIGCHI Lifetime Service Award, was inducted into the CHI Academy, and became an ACM Distinguished Scientist in 2010. She also received the Distinguished Alumni award from Indiana University's Brain and Psychological Sciences department in 2014. Mary became a Fellow of the ACM in 2016.

1 0

Distinguished Colloquium Speaker Mary Czerwinski, Monday Nov 20
by Emily Lawrence 15 Nov '17

15 Nov '17

Distinguished Colloquium Speaker Dr. Mary Czerwinski from Microsoft Research Thursday, November 20, 2017 - 12:30pm Computer Science - Room 105 Host: Szymon Rusinkiewicz Abstract: Affective computing is emerging as an important field in the design of emotional, intelligent, conversational agents that can be used in the healthcare arena, but also in everyday life. In addition, ubiquitous recording, both in the field and in the doctor's office/patient's home, has influenced how we think about wellbeing in the future. In our research, we use sensing technologies to develop contextualized and precise delivery of interventions, both in terms of the content and in the timing the intervention delivery, using machine learning algorithms. I will discuss how we use affective computing technologies to deliver just in time health interventions for improved health and for personal, behavioral reflection. For example, I will describe the Entendre project, which has implications for the design of visual feedback to encourage empathic patient-centered communication. I will also talk about ParentGuardian, a wearable sensing system that delivers just in time interventions to parents with ADHD children. In addition, I'll present our findings from two applications that deliver interventions and skills from psychology for coping with conditions ranging from general stress and depression to serious mental illness, like the intent to commit suicide, using conversational agents that users trust. Finally, I'll briefly touch on some of our designs for helping users to reflect on their daily behaviors in order to improve general well-being. Bio: Dr. Mary Czerwinski is a Principle Researcher and Research Manager of the Visualization and Interaction (VIBE) Research Group. Mary's latest research focuses primarily on emotion tracking and intervention design and delivery, information worker task management and health and wellness for individuals and groups. Her research background is in visual attention and multitasking. She holds a Ph.D. in Cognitive Psychology from Indiana University in Bloomington. Mary was awarded the ACM SIGCHI Lifetime Service Award, was inducted into the CHI Academy, and became an ACM Distinguished Scientist in 2010. She also received the Distinguished Alumni award from Indiana University's Brain and Psychological Sciences department in 2014. Mary became a Fellow of the ACM in 2016.

1 0

Reminder: Colloquium Speaker Christopher Manning, tomorrow at 12:30
by Emily Lawrence 15 Nov '17

15 Nov '17

Colloquium Speaker Prof. Christopher Manning, from Stanford University Thursday, November 16, 2017 - 12:30pm Computer Science - Room 105 Host: Dr. Sanjeev Arora *Please note, arrive early as seating and lunch may run out. Deep learning has had enormous success on perceptual tasks but still struggles in providing a model for inference. To address this gap, we have been developing Compositional Attention Networks (CANs). The CAN design provides a strong prior for explicitly iterative reasoning, enabling it to support explainable and structured learning, as well as generalization from a modest amount of data. The model builds on the great success of existing recurrent cells such as LSTMs: A CAN is a sequence of a single recurrent Memory, Attention, and Control (MAC) cell, and by careful design imposes structural constraints on the operation of each cell and the interactions between them, incorporating explicit control and soft attention mechanisms into their interfaces. We demonstrate the model's strength and robustness on the challenging CLEVR dataset for visual reasoning (Johnson et al. 2016), achieving a new state-of-the-art 98.9% accuracy, halving the error rate of the previous best model. More importantly, we show that the new model is more computationally efficient and data-efficient, requiring an order of magnitude less time and/or data to achieve good results. Joint work with Drew Arad. Bio: Christopher Manning is the Thomas M. Siebel Professor in Machine Learning, Linguistics and Computer Science at Stanford University. He works on software that can intelligently process, understand, and generate human language material. He is a leader in applying Deep Learning to Natural Language Processing, including exploring Tree Recursive Neural Networks, sentiment analysis, neural network dependency parsing, the GloVe model of word vectors, neural machine translation, and deep language understanding. He also focuses on computational linguistic approaches to parsing, robust textual inference and multilingual language processing, including being a principal developer of Stanford Dependencies and Universal Dependencies. Manning is an ACM Fellow, a AAAI Fellow, an ACL Fellow, and a Past President of ACL. He has coauthored leading textbooks on statistical natural language processing and information retrieval. He is a member of the Stanford NLP group (@stanfordnlp) and manages development of the Stanford CoreNLP software.

1 0

Ryan Beckett will present his Pre-FPO on Tuesday, November 14, 2017 at 11:30am in CS 233
by Nicki Gotsis 14 Nov '17

14 Nov '17

Ryan Beckett will present his Pre-FPO on Tuesday, November 14, 2017 at 11:30am in CS 233. The members of his committee are as follows: Advisor: David Walker Readers: Aarti Gupta, Ratul Mahajan (Microsoft) Non-Readers: Jennifer Rexford, Nick Feamster Everyone is invited to attend his talk. The talk title and abstract follow below Title: Network Control Plane Verification and Synthesis Abstract: Network control planes for traditional networks are highly complex distributed systems. Network devices use multiple protocols to exchange routing information about available paths to a destination, and how they process this information depends on their local configuration files. Each configuration file often consists of thousands of lines of assembly-like directives -- making it hard for humans to reason about individual device behaviors and even harder to reason about the network behavior that emerges through the distributed interactions of all devices. Consequently, network misconfiguration caused by human error remains a leading cause of network downtime. In my thesis, I develop novel approaches to automatically verify and synthesize network device configurations in a scalable manner from high-level specifications about their correctness. In the first part of this talk, I will describe a general approach to network control plane verification based on translating unmodified network configurations into logical formulae that capture both the stable states to which the network protocols converge as well as their impact on packet forwarding. Using an off-the-shelf Satisfiability Modulo Thoery (SMT) solver, we can verify adherence to a wide range of properties including reachability, fault-tolerance, router equivalence, and load balancing, for all possible outcomes of the control plane. In the second part of my talk, I will describe a new high-level network routing language and associated compilation techniques to generate device configurations that are correct-by-construction. Throughout both parts of the talk, I will describe the role of network abstraction in making these approaches scale to large, modern networks.

1 1

Chris Manning's two talks on Wed/Thurs
by Sanjeev Arora 13 Nov '17

13 Nov '17

Chris Manning of Stanford, an expert in deep learning and NLP is visiting on Wed and Thurs. On Wed he will give a popular talk at the IAS at 5pm. https://www.ias.edu/events/manning-publiclecture On Thurs he speaks in the small auditorium (in case of overcrowding, large auditorium) in CS at 12:30. Same title; more technical talk suited to CS audiences. http://www.cs.princeton.edu/events/25598 There are a 3 or so meeting slots with him open for Thurs afternoon; pls let me know if you'd like to meet him. Best, Sanjeev

1 0

Distinguished Colloquium Speaker Lorrie Faith Cranor, TODAY at 12:30
by Emily Lawrence 13 Nov '17

13 Nov '17

Distinguished Colloquium Speaker Prof. Lorrie Faith Cranor, from Carnegie Mellon University Monday, November 13, 2017 - 12:30pm Computer Science - Room 105 Host: Dr. Marshini Chetty User studies are critical to understanding how users perceive and interact with security and privacy software and features. While it is important that users be able to configure and use security tools when they are not at risk, it is even more important that the tools continue to protect users during an attack. Conducting user studies in the presence of (simulated) risk is complicated. We would like to observe how users behave when they are actually at risk, but at the same time we cannot harm user study participants or subject them to increased risk. Often the risky situations we are interested in occur relatively infrequently in the real world, and thus can be difficult to observe in the wild. Researchers use a variety of strategies to overcome these challenges and place participants in situations where they will believe their security or privacy is at risk, without subjecting them to increases in actual harm. In some studies, researchers recruit participants to perform real tasks not directly related to security so that they can observe how participants respond to simulated security-related prompts or cues that occur while users are focused on primary tasks. In other studies, researchers create a hypothetical scenario and try to get participants sufficiently engaged in it that they will be motivated to avoid simulated harm. Sometimes researchers have the opportunity to observe real, rather than simulated attacks, although these opportunities are usually difficult to come by. Researchers can monitor real world user behavior over long periods of time (in public or with permission of participants) and observe how users respond to risks that occur naturally, without researcher intervention. In this talk I will motivate the importance of security user studies and talk about a number of different user study approaches we have used at the CyLab Usable Privacy and Security Lab at Carnegie Mellon University. Lorrie Faith Cranor is a Professor of Computer Science and of Engineering and Public Policy at Carnegie Mellon University where she is director of the CyLab Usable Privacy and Security Laboratory (CUPS). She is associate department head of the Engineering and Public Policy Department and co-director of the MSIT-Privacy Engineering masters program. In 2016 she served as Chief Technologist at the US Federal Trade Commission, working in the office of Chairwoman Ramirez. She is also a co-founder of Wombat Security Technologies, Inc, a security awareness training company. She has authored over 150 research papers on online privacy, usable security, and other topics. She has played a key role in building the usable privacy and security research community, having co-edited the seminal book Security and Usability (O'Reilly 2005) and founded the Symposium On Usable Privacy and Security (SOUPS). She also chaired the Platform for Privacy Preferences Project (P3P) Specification Working Group at the W3C and authored the book Web Privacy with P3P (O'Reilly 2002). She has served on a number of boards, including the Electronic Frontier Foundation Board of Directors, and on the editorial boards of several journals. In her younger days she was honored as one of the top 100 innovators 35 or younger by Technology Review magazine. More recently she was elected to the ACM CHI Academy, named an ACM Fellow for her contributions to usable privacy and security research and education, and named an IEEE Fellow for her contributions to privacy engineering. She was previously a researcher at AT&T-Labs Research and taught in the Stern School of Business at New York University. She holds a doctorate in Engineering and Policy from Washington University in St. Louis. In 2012-13 she spent her sabbatical as a fellow in the Frank-Ratchye STUDIO for Creative Inquiry at Carnegie Mellon University where she worked on fiber arts projects that combined her interests in privacy and security, quilting, computers, and technology. She practices yoga, plays soccer, and runs after her three children.

1 0