Professor Rajeev Alur, University of Pennsylvania
Professor Orna Grumberg, Technion
Professor Peter Druschel, Max Planck Institute

Contact Person
Dr Reza SHOKRI, NUS Presidential Young Professor, School of Computing

  07 Jan 2020 Tuesday, 10:00 AM to 05:00 PM

 SR1, COM1-02-06

This is a distinguished talk as part of the NUS Computer Science Research Week 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).

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.

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.