09:30 – 10:00 Welcome Coffee
11:30 – 13:00 Lunch Break
14:30 – 15:30 Coffee Break and Poster Session
15:30 – 17:00 The Early Days of Interactive Proofs - Lance Fortnow [slides]
09:30 – 10:00 Welcome Coffee
11:30 – 13:00 Lunch Break
14:30 – 15:30 Coffee Break and Poster Session
15:30 – 17:00 The Power of Encounters - Peter Druschel
09:30 – 10:00 Welcome Coffee
10:00 – 11:30 Compressed Sensing and Generative Models - Eric Price [slides]
11:30 – 13:00 Lunch Break
14:30 – 15:30 Coffee Break and Poster Session
Monday, 6/1/2020, 10:00 – 11:30
Could Earphones be The Next Computing Platform after Smartphones? – Romit Roy Choudhury
This talk will argue that “earables” is the next significant mobile computing platform after smartphones. With numerous sensors, processors, and radios getting embedded into modern earphones, we envision these devices to create a new eco-system in the next 5 years. Earables will run voice assistants like Alexa; will sense human motion and gestures; will track health metrics through the ear; and will open new forms of interactions, such as acoustic AR/VR. The leap from today’s ear-phones to “earables” will mimmic the transformation from basic-phones to smart phones. Today’s smartphones are hardly a calling device anymore, much like how tomorrow’s earables will hardly be a wireless speaker or microphone. This talk will attempt to foresee the road ahead, starting with a broader vision, and followed by concrete research questions that emerge from it.
Romit Roy Choudhury is a Jerry Sanders Scholar and Professor of ECE and CS at the University of Illinois at Urbana Champaign (UIUC). He joined UIUC from Fall 2013, prior to which he was an Associate Professor at Duke University. His research interests are in wireless networking, embedded sensing, and applied signal processing. Along with his students, he received a few research awards, including the ACM Sigmobile Rockstar Award, the UIUC Distinguished Alumni Award, the 2017 ACM MobiSys Best Paper Award, etc. He was elevated to IEEE Fellow in 2018. Visit Romit's Systems Networking Research Group (SyNRG) at http://synrg.csl.illinois.edu.
Monday, 6/1/2020, 13:00 – 14:30
Legal Theorems of Privacy – Kobbi Nissim
There are significant gaps between legal and technical thinking around data privacy. Technical standards such as k-anonymity and differential privacy are described using mathematical language and strive for mathematical rigor whereas legal standards are not rigorous from a mathematical point of view and often resort to concepts such as de-identification and anonymization which they only partially define. As a result, arguments about the adequacy of technical privacy measures for satisfying legal privacy often lack rigor, and their conclusions are uncertain. The uncertainty is exacerbated by a litany of successful privacy attacks on privacy measures thought to meet legal expectations but then shown to fall short of doing so. We ask whether it is possible to introduce mathematical rigor into such analyses so as to make formal claims and prove “legal theorems” that technical privacy measures meet legal expectations. For that, we explore some of the gaps between these two very different approaches, and present initial strategies towards bridging these gaps. In particular, we focus on the concept of singling out from the EU’s General Data Protection Regulation (GDPR). To capture this concept, we define a new type of privacy attack, predicate singling out, where an adversary finds a predicate matching exactly one row in a database with probability significantly better then a statistical baseline. We then argue that any data release mechanism that purports to “render anonymous” data under the GDPR should prevent predicate singling out. Hence, the concept has legal consequences as it can be used as a yardstick for arguing whether data release mechanisms meet the GDPR standard of data anonymization.
Professor Kobbi Nissim is a McDevitt Chair at the department of Computer Science, Georgetown University and affiliated with Georgetown Law. Nissim’s work is focused on the mathematical formulation and understanding of privacy. His work from 2003 and 2004 with Dinur and Dwork initiated rigorous foundational research of privacy and in 2006 he introduced differential privacy with Dwork, McSherry and Smith. Nissim was awarded the Caspar Bowden Privacy for research in Privacy Enhancing Technology in 2019, the Gödel Prize in 2017, IACR TCC Test of Time Awards in 2016 and in 2018, and the ACM PODS Alberto O. Mendelzon Test-of-Time Award in 2013.
Monday, 6/1/2020, 15:30 – 17:00
The Early Days of Interactive Proofs – Lance Fortnow
Consider the clique problem, given a graph is there a collection of vertices of a given size that are all connected to each other. A powerful wizard could convince you that a large clique exists, just provide the set of vertices and you can check that all pairs are connected. This notion made formal the class NP, the basis of the famous P v NP problem.
What if the wizard wanted to convince you that no clique existed? You would seemingly need to check all large subsets. Thirty years ago, Lund, Fortnow, Karloff and Nisan showed that a wizard can convince a mere mortal, if the mortal can ask random questions. Shamir shortly thereafter extended these results to everything computable in a reasonable amount of memory, the IP = PSPACE result.
This talk will go over the early history of interactive proofs, a series of exciting results in the late 80’s and early 90’s, from its roots in cryptography and group theory to its applications in approximation and beyond.
Lance Fortnow is Dean of the College of Science at the Illinois Institute of Technology. Fortnow received his Ph.D. in Applied Mathematics at MIT in 1989 under the supervision of Michael Sipser. Before he joined Illinois Tech in 2019, Fortnow was the chair of the School of Computer Science at the Georgia Institute of Technology and previously was a professor at Northwestern University and the University of Chicago, a senior research scientist at the NEC Research Institute and a one-year visitor at CWI and the University of Amsterdam. From 2007 to 2018 Fortnow held an adjoint professorship at the Toyota Technological Institute at Chicago.
Fortnow's research spans computational complexity and its applications. His work on interactive proof systems and time-space lower bounds for satisfiability have led to his election as a 2007 ACM Fellow. In addition he was an NSF Presidential Faculty Fellow from 1992-1998 and a Fulbright Scholar to the Netherlands in 1996-97.
Among his many activities, Fortnow served as the founding editor-in-chief of the ACM Transaction on Computation Theory, served as chair of ACM SIGACT and on the Computing Research Association board of directors. He served as chair of the IEEE Conference on Computational Complexity from 2000-2006. Fortnow originated and co-authors the Computational Complexity weblog since 2002, the first major theoretical computer science blog. He has thousands of followers on Twitter.
Fortnow's survey The Status of the P versus NP Problem is one of the CACM's most downloaded article. Fortnow has written a popular science book The Golden Ticket: P, NP and the Search for the Impossible loosely based on that article.
Tuesday, 7/1/2020, 10:00 – 11:30
Safety Verification for Learning-enabled Control Systems – Rajeev Alur
Autonomous systems interacting with the physical world, collecting data, processing it using machine learning algorithms, and making decisions, have the potential to transform a wide range of applications including medicine and transportation. Realizing this potential requires that the system designers can provide high assurance regarding safe and predictable behavior. This motivates research on formally verifying safety (such as avoidance of collisions) of closed-loop systems with controllers based on learning algorithms. In this talk, I will use the experimental platform of the autonomous F1/10 racing car to highlight research challenges for verifying safety for systems with neural-network-based controllers. Our solution to safety verification, incorporated in the tool Verisig at Penn, builds upon techniques for symbolic computation of the set of reachable states of hybrid (mixed discrete-continuous) systems. The case study consists of training the controller using reinforcement learning in a simulation environment, verifying the trained controller using Verisig, and validating the controller by deploying it on the F1/10 racing car.
Rajeev Alur is Zisman Family Professor of Computer and Information Science at University of Pennsylvania. He obtained his bachelor's degree in computer science from IIT Kanpur in 1987 and PhD in computer science from Stanford University in 1991. Before joining Penn in 1997, he was with Computing Science Research Center at Bell Labs. His research is focused on formal methods for system design, and spans cyber-physical systems, programming languages, and theoretical computer science. He is a Fellow of the AAAS, a Fellow of the ACM, a Fellow of the IEEE, an Alfred P. Sloan Faculty Fellow, and a Simons Investigator. He was awarded the inaugural CAV (Computer-Aided Verification) award, ACM/IEEE Logic in Computer Science (LICS) Test-of-Time award, the inaugural Alonzo Church award by ACM SIGLOG / EATCS / EACSL / Kurt Goedel Society, Distinguished Alumnus Award by IIT Kanpur for his work on timed automata. Prof. Alur has served as the chair of ACM SIGBED (Special Interest Group on Embedded Systems), the general chair of LICS, and the lead PI of the NSF Expeditions in Computing center ExCAPE (Expeditions in Computer Augmented Program Engineering). He is the author of the textbook Principles of Cyber-Physical Systems (MIT Press, 2015).
Tuesday, 7/1/2020, 13:00 – 14:30
Automated Program Repair – Orna Grumberg
In the process of software development and maintenance, much efforts are invested in order to ensure that the product is as bug free as possible. When a bug is found, automating the repair process is highly desired. In this talk we present two approaches to automated program repair.
The first approach automatically repairs an erroneous program using a predefined set of mutations to the code (e.g., replacing ‘+’ with ‘-‘ ; ‘’ with ‘’, etc.). The repair algorithm goes through generate-validate iterations, which involve fault localization mechanism in order to disregard sets of unsuccessful repairs. The approach guarantees soundness and completeness with respect to a bounded notion of correctness.
The second approach intertwines compositional Assume-Guarantee verification with repair. Automata learning is used to verify the program or find an erroneous behavior. In the latter case, abduction assists in repairing the system by inferring new constraints that eliminate the error. Then, the verification proceeds for the repaired system.
The needed background for the talk will be presented. This is a joint work with: Hadar Frenkel, Corina Pasareanu, Bat-chen Rothenberg and Sarai Sheinvald.
Orna Grumberg is the Leumi Chair Professor of Computer Science at the Technion. She is a member of the Academia Europea and an ACM fellow. She holds a Ph.D. from the Computer Science Department at the Technion, and an Honorary Doctorate from the Technical University of Munich.
Her research interests include automated verification of software and hardware; Automated program repair; Exploiting model checking to finding security vulnerabilities; Abstraction, refinement and modularity in model checking; Temporal logics; and automata on infinite objects.
Grumberg serves on the steering committee of the main conference on model checking - Computer-aided Verification (CAV). She serves on numerous program committees of leading conferences.
Grumberg is co-author of the highly-cited book “Model Checking”, which is the main reference for the field of Formal Verification. She published numerous papers in top journals and leading conferences in the field and is highly cited. Her work on counterexample-guided abstraction refinement (CEGAR) has won the CAV award. Grumberg’s M.Sc. and Ph.D. students form the basis of the strong verification groups in Israeli branches of international companies such as IBM, Intel, Cadence and Nvidia.
Tuesday, 7/1/2020, 15:30 – 17:00
The Power of Encounters – Peter Druschel
A secure encounter is an agreement by two anonymous devices to have met at a given time and place. An associated shared secret enables the devices to subsequently confirm their encounter and communicate securely. In this talk, I will sketch how this simple idea enables fascinating new forms of privacy-preserving, contextual, secure communication among personal and IoT devices, and enables users to produce selective evidence of their personhood and physical whereabouts.
Encounters enable powerful forms of secure group communication among devices connected by chains of encounters, subject to spatial, temporal, and causality constraints. Applications range from connecting event attendees and virtual guest books to disseminating targeted health risk warnings, soliciting information and witnesses related to an incident, and tracing missing persons, all while maintaining users' privacy. Encounters also enable selective proofs of device (co-)location at a given time and place. Finally, encounters can provide evidence of a unique physical trajectory, which suggests a human user and promises a new defense to Sybil attacks.
Peter Druschel is the founding director of the Max Planck Institute for Software Systems (MPI-SWS) and Associate Chair of the Chemistry, Physics, and Technology Section of the Max Planck Society in Germany. Previously, he was a Professor of Computer Science and Electrical and Computer Engineering at Rice University in Houston, Texas. His research interests include distributed systems, mobile systems, privacy and compliance. He is the recipient of an NSF CAREER Award, an Alfred P. Sloan Fellowship, the ACM SIGOPS Mark Weiser Award, a Microsoft Research Outstanding Collaborator Award, and the EuroSys Lifetime Achievement Award. Peter is a member of Academia Europaea and the German Academy of Sciences Leopoldina.
Wednesday, 8/1/2020, 10:00 – 11:30
Compressed Sensing and Generative Models – Eric Price
The goal of compressed sensing is make use of image structure to estimate an image from a small number of linear measurements. The structure is typically represented by sparsity in a well-chosen basis. We show how to achieve guarantees similar to standard compressed sensing but without employing sparsity at all -- instead, we suppose that vectors lie near the range of a generative model G: R^k -> R^n. Our main theorem here is that, if G is L-Lipschitz, then roughly O(k log L) random Gaussian measurements suffice; this is O(k d log n) for typical d-layer neural networks.
The above result describes how to use a model to recover a signal from noisy data. But if the data is noisy, how can we learn the generative model in the first place? The second part of my talk will describe how to incorporate the measurement process in generative adversarial network (GAN) training. Even if the noisy data does not uniquely identify the non-noisy signal, the _distribution_ of noisy data may still uniquely identify the distribution of non-noisy signals.
This talk is based on joint works with Ashish Bora, Ajil Jalal, and Alex Dimakis.
Eric Price is an assistant professor in the Department of Computer Science at UT Austin, where he studies how algorithms can produce more accurate results with less data. He received a Ph.D. in computer science from MIT in 2013. Eric's research was featured in Technology Review's TR10 list of 10 breakthrough technologies of 2012, his thesis received a George M. Sprowls award for best doctoral thesis in computer science at MIT, and he has received an NSF CAREER award. Two themes of his research are adaptivity, where initial data can guide future data collection, and signal structure, where a structural assumption can yield provable improvements in space or sample complexity.
Wednesday, 8/1/2020, 13:00 – 14:30
Internet of Things — The Quest for Dependability – Lothar Thiele
If visions and forecasts of industry come true then we will be soon surrounded by billions of interconnected embedded devices. We will interact with them in a cyber-human symbiosis, they will not only observe us but also our environment, and they will be part of many visible and ubiquitous objects around us. We have the legitimate expectation that the individual devices as well as the overall system behaves in a reliable, predictable and trustworthy manner.
Besides, there are many application domains where we rely on a correct and fault-free system behavior. We expect trustworthy results from sensing, computation, communication and actuation due to economic importance or even catastrophic consequences if the overall system is not working correctly, e.g., in industrial automation, distributed control of energy systems, surveillance, medical applications, or early warning scenarios in the context of building safety or environmental catastrophes. Finally, trustworthiness and reliability are mandatory for the societal acceptance of human-cyber interaction and cooperation.<
It will be argued that we need novel architectural concepts, an associated design process and validations strategies to satisfy the strongly conflicting requirements and associated design challenges of platforms for the Internet of Things: Handle at the same time limited available resources, adaptive run-time behavior, and predictability. These challenges concern all components and functions of an IoT system, e.g., information extraction from global data, local decision making, computation, storage, wireless communication, energy management, energy harvesting, sensors, sensor interfaces, and actuation. The focus of the presentation is on new models and methods as well as examples from various fields in environmental monitoring.
Lothar Thiele joined ETH Zurich, Switzerland, as a full Professor of Computer Engineering, in 1994. His research interests include models, methods and software tools for the design of embedded systems, internet of things, cyberphysical systems, sensor networks, embedded software and bioinspired optimization techniques.
Lothar Thiele is associate editor of INTEGRATION - the VLSI Journal, Journal of Signal Processing Systems, IEEE Transaction on Industrial Informatics, Journal of Systems Architecture, IEEE Transactions on Evolutionary Computation, Journal of Real-Time Systems, ACM Transactions on Sensor Networks, ACM Transactions on Cyberphysical Systems, and ACM Transaction on Internet of Things.
In 1986 he received the "Dissertation Award" of the Technical University of Munich, in 1987, the "Outstanding Young Author Award" of the IEEE Circuits and Systems Society, in 1988, the Browder J. Thompson Memorial Award of the IEEE, and in 2000-2001, the "IBM Faculty Partnership Award". In 2004, he joined the German Academy of Sciences Leopoldina. In 2005, he was the recipient of the Honorary Blaise Pascal Chair of University Leiden, The Netherlands. Since 2009 he is a member of the Foundation Board of Hasler Foundation, Switzerland. Since 2010, he is a member of the Academia Europaea. In 2013, he joined the National Research Council of the Swiss National Science Foundation SNF. Lothar Thiele received the "EDAA Lifetime Achievement Award" in 2015. Since 2017, Lothar Thiele is Associate Vice President of ETH Zurich for Digital Transformation.
Wednesday, 8/1/2020, 15:30 – 17:00
Autonomous robotic systems by combining control and learning – Pan Jia
Thanks to the progress of control and machine learning techniques, robots nowadays are more intelligent than their predecessors 30 years ago. Advanced control techniques have enabled industrials robots to be faster, stronger, and more accurately than human workers in repetitive, structured tasks, though they are still difficult to solve everyday tasks in unstructured scenarios. Machine learning techniques have brought a revolution in perception and decision making, which allows a robot to explore new situations smartly according to its experience. However, its performance in many robotics tasks in terms of accuracy and robustness is far from being satisfactory. Control or machine learning alone is not enough for building an intelligent robot. An open problem in robotics is thus about how to combine control and machine learning in the most appropriate way in order to solve the bottleneck of applying robotics techniques in everyday life. In this talk, we will introduce our solutions to this non-trivial challenge using two challenging robotic tasks as examples: one is the autonomous robotic navigation in the dense pedestrian crowd, and the other is the deformable object manipulation for cloth assembly and suturing.
Pan Jia is currently an assistant professor in the Department of Computer Science at the University of Hong Kong. Prior to joining HKU, he was an assistant professor at the Mechanical Department at the City University of Hong Kong and a postdoc in the EECS department at the University of California at Berkeley. He received his BEng in Control Engineering from Tsinghua University in 2008, MEng in Pattern Recognition from the Chinese Academy of Sciences, and Ph.D. in Computer Science from the University of North Carolina at Chapel Hill. His research interests are robotic control and learning with a special focus on the development of autonomous robotic systems for navigation and manipulation.