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).