ICSE 2020 Plenary Sessions

• Keynote Plenary Sessions
  • Nancy Leveson
  • Peter O’Hearn
  • Chan-Mo Park
• Most Influential Paper from ICSE N-10
  • Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari
• 2020 Harlan Mills Award
  • Nachiappan Naggapan
• 2020 SIGSOFT Outstanding Research Award
  • Mike Ernst

Keynote Plenary Sessions

Dr. Nancy Leveson Professor of Aeronautics and Astronautics MIT	Dr. Peter O'Hearn Research Scientist at Facebook and Professor at University College London	Dr. Chan-Mo Park POSTECH Former President / Chancellor Pyongyang University of Science and Technology (PUST)

Nancy Leveson

Everything You “Know” About Software and Safety is Probably Wrong. For much of its existence, software engineering has not had to deal directly with safety. Software is an abstraction and abstractions do not directly harm anyone or anything: it does not explode, catch on fire, or exude toxins. It can, of course, indirectly cause harm by providing unsafe control over physical processes that are directly dangerous. But until relatively recently, software was used to control dangerous physical processes only in limited and constrained circumstances. That genie has been let out of the bottle and nearly every dangerous system is now controlled by software. In this presentation, I will describe what needs to be done to limit the damage done by software and the new practices that are required to deal with the problem.

Bio. Dr. Nancy Leveson has worked in the field of system safety for 30 years. Currently she is Professor of Aeronautics and Astronautics and also Professor of Engineering Systems at MIT. She is an elected member of the National Academy of Engineering (NAE) and has received many awards such as the ACM Allen Newell Award for outstanding computer science research, the AIAA Information Systems Award for “developing the field of software safety and for promoting responsible software and system engineering practices where life and property are at stake,” and the ACM Sigsoft Outstanding Research Award. She has published over 200 research papers and is author of a book, Safeware: System Safety and Computers, published by Addison-Wesley and recently translated into Japanese and a new book Engineering a Safer World published by MIT Press in January 2012.

Peter O’Hearn

Formal Reasoning and the Hacker Way

This talk is about the unexpected learnings when a theoretical computer scientist was suddenly submerged into a fast-moving industrial software engineering practice.

I’ll recount the clash of cultures I encountered when, after 25 years in academia, I moved to Facebook with the acquisition of a program verification startup, Monoidics.

Traditionally calm and cool formal reasoning came in contact with a heated software development methodology based on rapid modification of large codebases (thousands of modifications per day on 10s MLOC). To my surprise, we found that static formal reasoning could survive and even thrive when we used techniques allowing it to adapt it to the company’s “hacker way” engineering culture, rather than the other way around. I’ll also describe how interactions with software engineers caused me to question some of the assumptions I brought from academic static analysis, and how I’ve come out the other side with new science spurred by that experience (most recently, incorrectness logic). Overall, I hope to convey that having theory and engineering playing off one another in a tight feedback loop is possible, even advantageous, when practicing static analysis in industry at present.

Bio. Peter O’Hearn is a Research Scientist at Facebook and a Professor at University College London. Peter has done research in the broad areas of programming languages and verification for over 25 years, having held academic positions at Syracuse University, Queen Mary University of London, and University College London, before joining Facebook in 2013 with the acquisition of the verification startup Monoidics. With John Reynolds Peter devised separation logic, a theory which opened up new practical possibilities for program proof, including the technology which led to the Infer program analyzer developed by Peter’s team at Facebook. Infer runs internally on Facebook’s code bases, detecting over 100,000 bugs which have been fixed by Facebook’s developers in the past five years. Infer is also used in production at number of other companies, including Amazon, Mozilla, Spotify and Marks and Spencer. Peter is a Fellow of the Royal Society, a Fellow of the Royal Academy of Engineering and he has received a number of awards for his work including the 2016 Godel Prize, the 2016 CAV Award and the 2011 and 2019 POPL MIP Awards. Peter received an honorary doctorate from Dalhousie University in 2018.

Chan-Mo Park

ICT Manpower Development and Software Technology in the DPRK. The government of the Democratic People’s Republic of Korea (DPRK, also referred to by many as “North Korea”) realized the importance of Information and Computing Technology (ICT) and began to establish a master plan for ICT adoption after Kim Il Sung toured eight countries in Eastern Europe in 1984. Kim determined that electronics-related high technology was key to national economic development, and technical cooperation contracts were signed with many of the countries he visited. Moreover, DPRK students were sent to those countries to learn modern technologies. In 1988, a three-year plan for the promotion of science and technology began, and the government began to provide massive funding for information science and industry. In addition, through the International Cooperation Bureau of the State Commission of Science and Technology, the DPRK has been seeking help from UN organizations such as the United Nations Development Program and the United Nations Industrial Development Organization. Also, the DPRK signed an MoU with the International Institute for Software Technology of United Nations University on a joint effort for software development. The DPRK has been stressing software sectors more than hardware sectors due to its poor economic situation and various restrictions (such as those imposed by the Wassenaar Agreement, COCOM, and EAR) on the importation of advanced equipment. The software industry does not require a large amount of capital but instead requires good human brains and creativity. In general, young people in the DPRK are very strong in mathematics and basic sciences. In this presentation, the general education system in the DPRK will be briefly described, and this will be followed by a detailed discussion of several aspects of ICT education in the DPRK, including education in secondary schools for gifted students, the establishment of computer technology universities, and ICT education at prestigious universities and research institutions including KISU(Kim Il Sung University), KUT(Kim-Chaek University of Technology), PUST(Pyongyang University of Science and Technology), KCC(Korea Computer Center) and PIC(Pyongyang Informatics Center). The level of software technology in the DPRK is nearly on a par with that of Western countries. The Silver Star Go game developed in 1997 won the first prize in the global computer Go game competition held in Japan in 1998. Since then, the DPRK has won first prize several years in a row. The DPRK government initiated many programs to encourage and improve the DPRK’s software capability. Some of the software products developed in earlier days will be presented, together with those displayed at the DPRK Computer Software Seminar being held in Beijing, China in April, 2002. After the historic meeting of Kim Dae-jung and Kim Jong Il in June 2000, inter-Korean collaborations in ICT, in particular those involving technology, had become quite active until the South Korean government halted collaborations on May 24, 2010. Some examples of inter-Korean projects will be described. Finally, a brief introduction to Pyongyang University of Science and Technology and its role in nurturing skilled graduates with global mindsets, in order to lead the DPRK into the era of the 4th Industrial Revolution, will be presented.

Bio. Dr. Chan-Mo Park was the 4th President of Pohang University of Science & Technology (POSTECH). After retiring from POSTECH in 2007 Prof. Park served as a Special Advisor on S & T to the President of Republic of Korea (ROK) before he assumed a Chancellor position with Pyongyang University of Science & Technology (PUST), a unique private and international university in DPRK since October, 2010. Prof. Park received his B.S. degree from Seoul National University and M.S. and Ph.D. degrees from University of Maryland, College Park. He earned an Honorary Doctor of Letters degree from the University of Maryland University College in 2001 in recognition of his scholarly achievements and distinguished service.
Dr. Park’s experience includes professorships in Computer Science both in U.S.A. and Korea. His research interests are Computer Graphics, Virtual Reality, System Simulation and Science Diplomacy. For the past several years, he has been involved with research activities concerning IT development in DPRK including a joint research with Pyongyang Informatics Centre (PIC) for 7 years. Dr. Park was decorated by ROK with the National Order of Camellia in 1986 for his contributions to the advancement of S & T in Korea and received the Teacher of the Year Award from The Catholic University of America in 1987. In June, 2005 he was decorated by ROK with the Blue Stripes Order of Service Merit for his contributions on IT development in Korea and collaborations with DPRK. Prof. Park also received the International Alumnus Award from the University of Maryland, College Park in April, 2009 for providing significant leadership to another country’s educational, cultural, social and economic development. In November, 2018 Chancellor Park received the Dosan Education Award from Dosan Academy in Seoul, Korea for his contribution to the Advancement of Science and Technology in Korea, Manpower development and Inter-Korean Collaboration on Information Technology.

We are pleased to announce this year’s this year’s recipient of the ICSE 2020 Most Influential Paper Award from ICSE 2010:

• Oracle-Guided Component-Based Program Synthesis
  Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari
  https://dl.acm.org/citation.cfm?id=1806833

“By bringing together the notion of an oracle providing input/output examples with the reduction of synthesis to two kinds of search problems — those aiming at producing oracle-consistent programs and those producing distinguishing inputs to further elaborate the candidate program — ‘Oracle-guided component-based program synthesis’ has made a significant impact in Software Engineering and beyond, inspiring subsequent work not only on program synthesis and learning, but also on automated program repair, controller synthesis, and interpretable artificial intelligence.”
– Sebastian Uchitel, co-Chair, MIP Committee

A Decade of Oracle-Guided Program Synthesis: Progress, Challenges, and Opportunities

Program Synthesis is concerned with the fascinating goal of generating a program to meet a specification that can be given in one of many forms. The field has evolved over the years, but it is in the last decade that it has truly exploded with new techniques and applications. In this talk, we place our paper from ICSE 2010, titled “Oracle-guided component-based synthesis” in this journey of program synthesis. We describe the results in the paper, and their impact on some key trends in modern program synthesis, namely counterexample-guided inductive synthesis, programming by examples, and domain-specific languages for synthesis, as well as theoretical and practical connections with machine learning. We highlight follow-up work on synthesis partly influenced by this paper from academia and across industries ranging from software and hardware to logistics and aerospace. We identify successes, failures, and the key challenges remaining to the broader deployment of automated synthesis techniques. We hope our experience will inspire researchers and students pursuing the goal of automated synthesis.

Bios:
Susmit Jha is a Principal Computer Scientist at SRI International, leading the research on building trustworthy, resilient, and interpretable neurosymbolic Artificial Intelligence. He is a primary investigator on several U.S. Government research programs including DARPA Assured Autonomy, DARPA Intent-based Design of Adaptive Software, DARPA Symbiotic Design of Cyberphysical Systems, IARPA Trojans in AI, Army Research Laboratory’s Internet of Battlefield Things CRA, and National Science Foundation’s projects on Duality-based Synthesis and Self-improving Cyberphysical Systems. Before joining SRI, he was a Staff Scientist at United Technologies Research Center (UTRC) from 2014 to 2016, and a Research Scientist at Intel from 2012 to 2014. Dr. Jha’s research on automated synthesis at UTRC and Intel impacted aerospace and semiconductor products, reaching millions of people. The SoC Converged Architecture product division at Intel awarded him a Division Recognition Award for his impact on 14nm SoCs. He has published 60+ peer-reviewed publications at top-tier venues in machine learning and formal methods. He obtained his B.Tech. in Computer Science from IIT Kharagpur in 2006 and was awarded TCS Gold Medal. He received his M.S. and Ph.D. in Electrical Engineering and Computer Science from UC Berkeley in 2011 and was awarded the Leon O. Chua award. The paper on “Oracle-Guided Component-Based Program Synthesis” was a component contribution of Dr. Jha’s Ph.D. thesis.

Sanjit A. Seshia is a Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in formal methods for dependable and secure computing, with a current focus on the areas of cyber-physical systems, computer security, machine learning, and robotics. He has made pioneering contributions to the areas of satisfiability modulo theories (SMT), SMT-based verification, and inductive program synthesis. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, and the IEEE Technical Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award. He is a Fellow of the IEEE.

Ashish Tiwari received his B.Tech degree in Computer Science from the Indian Institute of Technology, Kanpur in 1995, and his Ph.D. in Computer Science from the State University of New York at Stony Brook in 2000. He is currently a member of the Prose team at Microsoft. Prior to that, he was a Staff Scientist at SRI International. He has worked in the areas of program analysis, synthesis, automated deduction, and hybrid systems.

Sumit Gulwani is a Computer Scientist seeking connections: between ideas, between research & practice, and with people with varied roles. He is the inventor of many intent-understanding, programming-by-example, and programming-by-natural-language technologies including the popular Flash Fill feature in Excel used by hundreds of millions of people. He founded and currently leads the PROSE research and engineering team at Microsoft that develops APIs for program synthesis and incorporates them into various products. He has published 125+ peer-reviewed papers in top-tier conferences and journals across multiple computer science areas, delivered 50+ keynotes and invited talks at various forums, and authored 50+ patent applications (granted and pending). He was awarded the ACM SIGPLAN Robin Milner Young Researcher Award in 2014 for his pioneering contributions to end-user programming and intelligent tutoring systems. He obtained his PhD in Computer Science from UC-Berkeley, and was awarded the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in Computer Science and Engineering from IIT Kanpur, and was awarded the President’s Gold Medal.

Events