CAREER: A Formal, Integrated Analysis Framework for Contract-based Reasoning of Strong Properties of Open Systems

本研究旨在开发一种形式化、集成化的分析框架，该框架基于多种分析技术的协同组合，如符号执行、模型检测、静态分析、约束求解和定理证明，用于对开放系统(其计算结构不完整)的行为进行推理。该框架为现代软件系统的质量保证提供了一种全面的方法，以获得强大的行为特性，包括合同检查、辅助代码检查和理解以及自动测试用例生成。提供这种框架的关键技术挑战是分析的可扩展性和对大量使用动态创建的堆对象、高级编程构造和抽象(例如，设计模式)、库和软件框架的软件组件的深层语义属性的模块化推理的支持。该项目为开放式面向对象系统的自动形式化分析的长期研究奠定了基础，该分析从过去几年各种分析技术的重大进步中汲取了优势。除了关于强功能属性的推理之外，该方法还可以支持用于未来调查的一系列软件质量保证技术，例如分析并发性、安全信息流和系统事件排序(例如，用于检查应用程序编程接口的协议一致性)。

This research aims to develop a formal, integrated analysis framework based on a synergistic combination of various analysis techniques such as symbolic execution, model checking, static analysis, constraint solving, and theorem proving for reasoning about behaviors of open systems (whose computational structures are incomplete). The framework enables a holistic approach to quality-assurance of modern software systems for strong behavioral properties including contract checking, assisting code inspection and understanding, and automatic test case generation. Key technical challenges in providing such framework are scalability of the analysis and support for modular reasoning about deep semantic properties of software components that heavily use dynamically created heap objects, high-level programming constructs and abstractions (e.g., design patterns), libraries, and software frameworks. This project lays the foundation for a long-term investigation of an automatic formal analysis for open object-oriented systems that draws its strengths from significant advancements of various analysis techniques over the past several years. In addition to reasoning about strong functional properties, the approach can support a spectrum of software quality-assurance techniques for future investigations such as analyzing concurrency aspects, secure information-flow, and system event orderings (e.g., useful for checking protocol conformance of application programming interfaces).