It is important for many critical software components to be correct and reliable, however verifying that software meets such requirements is difficult, expensive, and error-prone. One approach is to use software contracts as a means to specify and monitor the obligations and guarantees of software components. When the agreements of such contracts are not met during the operation of a program, the program stops and signals a violation and indicates the faulty component. Software contracts have been very important for high-assurance software, since they identify faulty program components, but they offer no guarantees that a component will not fail. The goal of this research project is to investigate approaches to ahead-of-time software verification that can prove the absence of contract failures, thus giving a high level of confidence in the correctness and reliability of critical software components. The research will contribute a new understanding of the interplay between program verification, software contracts, and modern programming languages. Additionally, it will result in the development of tools for verifying software components with contracts. It is expected that by verifying software contracts ahead-of-time, the overhead of monitoring contract agreements during program operation can be eliminated, which will encourage programmers to use contracts far more extensively than they currently do. Such tools can dramatically reduce the difficulty and cost of developing high-assurance software.
There are two paramount technical obstacles that must be overcome to achieve the goals of this project: (1) the expressivity of contracts, while crucial for the construction of reliable components, thwarts static reasoning about programs and incurs significant run-time monitoring costs, (2) the expressivity of higher-order programming languages, a mainstay of modern industrial software construction, thwarts static reasoning about contracts, despite the availability of mature automated tools and techniques. This research project rectifies the situation by providing foundations for modular and compositional automated reasoning about behavioral contracts in a higher-order language. Specifically, the project will provide: (1) a foundational theory in terms of a semantics for reasoning about components via their contracts, which enables automated component-based contract verification; (2) an interactive contract verification environment for exploring, testing, and refining programs and contracts; and (3) an evaluation of our approach and tools in the context of the Racket programming language implementation and standard library, which contains extensive use of contracts.
