On Safety, Assurance and Reliability: A Software Engineering Perspective
Marsha Chechik, University of Toronto, Canada
AI-assisted Programming: Applications, User experiences, and Neuro-symbolic Techniques
Sumit Gulwani, Microsoft
Marsha Chechik, University of Toronto
From financial services platforms to social networks to vehicle control, software has come to mediate many activities of daily life. Governing bodies and standards organizations have responded to this trend by creating regulations and standards to address issues such as safety, security and privacy. In this environment, the compliance of software development to standards and regulations has emerged as a key requirement. Compliance claims and arguments are often captured in assurance cases, with linked evidence of compliance. Evidence can come from test cases, verification proofs, human judgement, or a combination of these. That is, we try to build (safety-critical) systems carefully according to well justified methods and articulate these justifications in an assurance case that is ultimately judged by a human.
Building safety arguments for traditional software systems is difficult — they are lengthy and expensive to maintain, especially as software undergoes change. Safety is also notoriously noncompositional — each subsystem might be safe but together they may create unsafe behaviors. It is also easy to miss cases, which in the simplest case would mean developing an argument for when a condition is true but missing arguing for a false condition. Furthermore, many ML-based systems are becoming safety-critical. For example, recent Tesla self-driving cars misclassified emergency vehicles and caused multiple crashes. ML-based systems typically do not have precisely specified and machine-verifiable requirements. While some safety requirements can be stated clearly: “the system should detect all pedestrians at a crossing”, these requirements are for the entire system, making them too high-level for safety analysis of individual components. Thus, systems with ML components (MLCs) add a significant layer of complexity for safety assurance.
I argue that safety assurance should be an integral part of building safe and reliable software systems, but this process needs support from advanced software engineering and software analysis. In this talk, I outline a few approaches for development of principled, tool-supported methodologies for creating and managing assurance arguments. I then describe some of the recent work on specifying and verifying reliability requirements for machine-learned components in safety-critical domains.
Marsha Chechik is Professor in the Department of Computer Science (where she was a former Chair in 2019-22), and Acting Dean in the Faculty of Information at the University of Toronto. She received her Ph.D. from the University of Maryland. Prof. Chechik’s research interests are in the application of formal methods to improve the quality of software. She has authored over 200 papers in formal methods, software specification and verification, computer safety and security and requirements engineering. Marsha Chechik is Program Chair of the 2023 International Conference on Formal Methods (FM’23). She has been Program Committee Co-Chair of the 2021 International Conference on Foundations of Software Engineering (ESEC/FSE’21), 2018 International Conference in Software Engineering (ICSE’18), 2016 International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16), the 2016 Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE16), the 2014 International Conference on Automated Software Engineering (ASE’14), the 2008 International Conference on Concurrency Theory (CONCUR’08), the 2008 International Conference on Computer Science and Software Engineering (CASCON’08), and the 2009 International Conference on Formal Aspects of Software Engineering (FASE’09). She is a Distinguished Member of ACM, a Vice Chair of ACM SIGSOFT, and holds a Bell University Chair in Software Engineering.
Sumit Gulwani, Microsoft
AI can enhance programming experiences for a diverse set of programmers: from professional developers and data scientists (proficient programmers) who need help in software engineering and data wrangling, all the way to spreadsheet users (low-code programmers) who need help in authoring formulas, and students (novice programmers) who seek hints when stuck with their programming homework. To communicate their need to AI, users can express their intent explicitly—as input-output examples or natural-language specification—or implicitly—where they encounter a bug (and expect AI to suggest a fix), or simply allow AI to observe their last few lines of code or edits (to have it suggest the next steps).
The task of synthesizing an intended program snippet from the user’s intent is both a search and a ranking problem. Search is required to discover candidate programs that correspond to the (often ambiguous) intent, and ranking is required to pick the best program from multiple plausible alternatives. This creates a fertile playground for combining symbolic-reasoning techniques, which model the semantics of programming operators, and machine-learning techniques, which can model human preferences in programming. Recent advances in large language models like Codex offer further promise to advance such neuro-symbolic techniques.
Finally, a few critical requirements in AI-assisted programming are usability, precision, and trust; and they create opportunities for innovative user experiences and interactivity paradigms. In this talk, I will explain these concepts using some existing successes, including the Flash Fill feature in Excel, Data Connectors in PowerQuery, and IntelliCode/CoPilot in Visual Studio. I will also describe several new opportunities in AI-assisted programming, which can drive the next set of foundational neuro-symbolic advances.
Sumit Gulwani is a computer scientist connecting ideas, people, and research & practice. He invented the popular Flash Fill feature in Excel, which has now also found its place in middle-school computing textbooks. He leads the PROSE research and engineering team at Microsoft that develops APIs for program synthesis and has incorporated them into various Microsoft products including Visual Studio, Office, Notebooks, PowerQuery, PowerApps, PowerAutomate, Powershell, and SQL. He is a sponsor of storytelling trainings and initiatives within Microsoft. He has started a novel research fellowship program in India, a remote apprenticeship model to scale up impact while nurturing globally diverse talent and growing research leaders. He has co-authored 11 award-winning papers (including 3 test-of-time awards from ICSE and POPL) amongst 140+ research publications across multiple computer science areas and delivered 60+ keynotes/invited talks. He was awarded the Max Planck-Humboldt medal in 2021 and the ACM SIGPLAN Robin Milner Young Researcher Award in 2014 for his pioneering contributions to program synthesis 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.
Mik Kersten, Tasktop Technologies; Gail C. Murphy, University of British Columbia
The creation of techniques, languages and tools to support building software from modular parts has enabled the development and evolution of large complex software systems. For many years, the focus of modularity was on the structure of the software system. The thinking was that the right modularity would enable software teams involved in different pieces of the system to work as independently as possible. As a community, we learned over the years that a system has no one optimal modularity, and in fact, the work that is undertaken to add new features or fix defects often crosscuts the modularity of the software. The research we conducted on task contexts and Mylyn over fifteen years ago recognized that capturing the activity performed on development tasks provided a means to make explicit emergent modularity for a system. With Mylyn, we explored how the activity of one developer could enable the surfacing of emergent modularity to help a developer perform tasks on a software system. Through stewardship of the Mylyn open source project and the creation of Tasktop Technologies, we brought these ideas into use in industry. Over the past decade, through interactions with practicing developers and their organizations, we have learned more about how modularity emerges at the individual developer, team, and organizational levels. Tasktop’s products moved accordingly from supporting the activity of individual developers to supporting the streams of value teams within an organization produce. In this talk, we will discuss how following the flow of tasks within software development supports value stream management and outline open research questions about the socio-technical aspects of developing complex software systems.
Mik Kersten is the chief technology officer at Planview. Mik co-founded Tasktop Technologies (recently acquired by Planview) and is the best-selling author of “Project To Product: How to Survive and Thrive in the Age of Digital Disruption with the Flow Framework®“. Mik’s experiences working with some of the largest digital transformations in the world has led him to identify the critical gap between business leaders and technologists, resulting in his creation of the Flow Framework® to connect strategy to delivery. He started his career as a Research Scientist at Xerox PARC where he built the first aspect-oriented development environment. He then pioneered the integration of development environments with Agile and DevOps tools while working on his Computer Science PhD at the University of British Columbia. Founding Tasktop out of that research, Mik has written over one million lines of open-source code that are still in use today and has brought seven successful open-source and commercial products to market.
Gail C. Murphy is a Professor of Computer Science and Vice-President Research and Innovation at the University of British Columbia (UBC). Her research interests are in improving the productivity of software developers and knowledge workers by giving them tools to identify, manage and co-ordinate the information that really matters for their work. She is a Fellow of the Royal Society of Canada, a Fellow of the ACM and a recipient of such awards as the IEEE Harlan J. Mills Award, a University of Washington Computer Science & Engineering Alumni Achievement Award, an NSERC E.W.R. Stacie Memorial Fellowship and the AITO Dahl-Nygaard Junior Prize.
Zhi Jin, Peking University, China
Programming languages are artificial and highly restricted languages. But source code is there to tell computers as well as programmers what to do, as an act of communication. Despite its weird syntax and is riddled with different delimiters, the good news is that the very large corpus of open-source code is available. That makes it reasonable to apply machine learning techniques to source code to enable the source code analytics.
Despite there are plenty of deep learning frameworks in the field of NLP, source code analytics has different features. In addition to the conventional way of coding, understanding the meaning of code involves many perspectives. The source code representation could be the token sequence, the API call sequence, the data dependency graph, and the control flow graph, as well as the program hierarchy, etc. This tutorial will tell the long, ongoing, and fruitful journey on exploiting the potential power of deep learning techniques in source code analytics. It will highlight that how code representation models can be utilized to support software engineers to perform different tasks that require proficient programming knowledge. The exploratory work show that code does imply the learnable knowledge, more precisely the learnable tacit knowledge. Although such knowledge is not easily transferrable between humans, it can be transferred between the automated programming tasks. A vision for future research will be stated for source code analytics.
Zhi Jin is professor of computer science at Peking University. She is currently the deputy director of Key Lab of High Confidence Software Technologies (PKU), Ministry of Education. Her main research interest is AI for SE, with a long-term focus on domain knowledge-led requirements engineering. She has published over 200 scientific articles in refereed international journals, such as IEEE T-KDE, T-SE, ACM T-OSEM, and T-CPS, and high rank conferences, such as ICSE, FSE, ASE and RE. She has co-authored five books and has held more than 30 approved invention patents. She is four times recipient of ACM SIGSOFT Distinguished Paper Awards. Prof. Jin serves as an Associate Editor of IEEE Transactions on Software Engineering, IEEE Transactions on Reliability, and ACM Transactions on Autonomous and Adaptive Systems, and serves on the Editorial Board of Requirements Engineering Journal and Empirical Software Engineering. She was the director of CCF (China Computer Federation) Technical Committee of Software Engineering (2016-2019) and currently the director of CCF Technical Committee of System Software (2020-2023). She is member of ACM, senior member of the IEEE, Fellow of CCF.
Andreas Zeller, CISPA Helmholtz Center for Information Security
Much of our research requires building tools to evaluate and demonstrate new approaches. Yet, tool building can take large amounts of time and resources. And it brings risks: The original idea might not work; rendering all efforts futile. And after the student in charge has left, the tool becomes a maintenance problem.
In this tutorial, I present tools and techniques for the quick creation of prototypes for academic research. Building prototypes in and for Python is at least ten times faster than traditional engineering in and for C or Java; it thus frees lots of time for creating and refining approaches. Using Jupyter Notebooks to code and run experiments saves rationales, settings, examples, and results in self-contained documents that can be read and reused easily by other students and researchers. Once the basics of the new approach are settled (and only then!) can one go and port the new approach to “traditional” languages – or move on to the next challenge.
You don’t believe me? Watch me illustrate this approach by building a symbolic fuzzer (think KLEE) for Python from scratch, live coding the capturing and solving of path conditions in less than 20 minutes. From there, we will determine what it is that makes languages like Python and tools like Jupyter Notebooks so suitable for academic prototyping, and the consequences this has (or should have) for organizing our research.
Andreas Zeller is faculty at the CISPA Helmholtz Center for Information Security and a professor of Software Engineering at Saarland University, both in Saarbrücken, Germany. His research on automated debugging, mining software archives, specification mining, and security testing has won several awards for its impact in academia and industry. Zeller is an ACM Fellow, an IFIP Fellow, an ERC Advanced Grant Awardee, and holds an ACM SIGSOFT Outstanding Research Award.
Mon 14 Nov
08:30 - 09:00
09:00 - 10:30
|AI-Assisted Programming: Applications, User Experiences, and Neuro-Symbolic Techniques (Keynote)|
Sumit Gulwani MicrosoftDOI
10:30 - 11:00
12:30 - 14:00
14:00 - 15:30
Andreas Zeller CISPA Helmholtz Center for Information SecurityDOI Pre-print
Tue 15 Nov
08:00 - 09:15
09:15 - 10:15
|Automated concolic testing of smartphone apps|
10:15 - 10:45
12:30 - 14:00
16:00 - 17:30
Transportation to Banquet from 16:30Social
Wed 16 Nov
08:00 - 09:00
09:00 - 10:30
|Task Modularity and the Emergence of Software Value Streams (Impact Award Paper Keynote)|
10:30 - 11:00
14:00 - 15:30
|Multi-perspective representation learning for source code analytics|
Zhi Jin Peking UniversityDOI
16:00 - 17:30
|On Safety, Assurance, and Reliability: A Software Engineering Perspective (Keynote)|
Marsha Chechik University of TorontoDOI