Abstraction and Automation for Reasoning about Complex Software

现代软件开发是一项复杂而杂乱的业务。要求很可能是不完整的。新的开发使用复杂的现有库、工具和组件，这些都可能失败。多个开发团队按照不同的计划进行，这使得很难确保他们的构件将按预期的那样“相互交谈”。每次进行更改时，都需要执行昂贵的质量保证，以确保软件仍能正常运行。这些问题变得更加可怕，因为许多公司，特别是在汽车、电子、航空航天和国防领域，需要维护功能相似但不相同的软件产品变体系列(例如，支持不同类型的客户和/或软件平台)。*我相信，上述许多问题可以通过可工业扩展的自动化推理和分析工具来帮助，这些工具使用户能够回答关于其制品的基本问题。例如，他们可以确定提议的更改的影响，询问关于他们设计的“如果”问题，确定不同的功能是否将交互，检查组件的所需属性是否在任何环境中保持，等等。创建这样的工具需要正式验证和软件工程方面的专业知识，因为许多挑战在于为SE从业者提高分析工具的可用性，在“正确的”抽象级别执行分析，在开发生命周期的早期启用分析(在尚未获得完整信息的情况下)，重复使用产品变体之间的分析结果，等等。*本项目的目标是开发精确的、有效且可扩展的自动化技术，用于解决各种复杂的软件工程问题。重点将放在实现对具有不完整信息的构件的分析、处理产品线和分析重用。我打算利用我对模型检查器和静态分析器等验证工具的深入了解，并努力建立正确的抽象来促进推理。该项目的成功将大大扩大自动化推理和分析在实践中的适用范围。**

Modern software development is a complex and messy business. Requirements are likely incomplete. New development uses complex existing libraries, tools and components that can fail. Multiple development teams proceed on different schedules, making it difficult to assure that their artifacts will "talk to each other" as intended. Every time a change is made, expensive quality assurance needs to be performed to ensure that software still does what it was supposed to. Such problems are made even more dire because many companies, especially in automotive, electronics, aerospace and defense domains, need to maintain families of software product variants with similar yet not identical functionality (e.g., supporting different types of customers and/or software platforms).***   I believe that many of the above problems can be aided by the availability of industrially scalable automated reasoning and analysis tools that enable users to answer essential questions about their artifacts. For example, they can determine the impact of a proposed change, ask "what if" questions about their designs, determine whether the different features are going to interact, check whether desired properties of a component would hold in any environment, etc. Creating such tools requires expertise both in formal verification and in software engineering, as many of the challenges are in improving usability of the analysis tools for SE practitioners, performing analysis at the "right" level of abstraction, enabling analysis earlier in the development lifecycle where complete information is not yet available, reusing results of analysis between product variants, etc.***   The goal of this project is to develop precise, effective and scalable automated techniques to solve a variety of complex software engineering problems. The emphasis will be on enabling analysis of artifacts with incomplete information, handling product lines, and analysis reuse. I intend to leverage my in-depth knowledge of verification tools such as model-checkers and static analyzers as well as strive to establish the right abstractions to facilitate reasoning. Success of this project will significantly expand the scope of applicability of automated reasoning and analysis in practice.**