Towards Verification of Behavioral Software Contracts

Опубликовано 28 июля 2016, 2:06

The past two decades have seen two parallel trends in software development: the increased use of linguistic tools to rigorously ensure the reliability of software, and the rise of higher-order programming languages. A prominent strand within the former are Meyer-style contract systems, originally developed for the Eiffel programming language and now available in a range of languages, including Spec#. Contracts empower programmers to write important invariants of the components they develop and have these down invariants enforced at runtime. Over the past few years, MSR's RiSE group has demonstrated that theorem provers can verify many of these contracts at compile time, supporting programmers as they create modules in their IDEs. As research over the past decade has shown, contracts for higher-order languages pose novel challenges. These contracts are no longer simple boolean predicates on flat values but test objects and functions for infinitary properties. Reasoning about such properties calls for new approaches and technologies, and my talk will present a first solution. The approach extends symbolic execution to use behavioral contracts as symbolic values, thus enabling symbolic approximation of higher-order behavior. This work opens a path toward applying first-order verification techniques to a higher-order setting. This is joint work with Sam Tobin-Hochstadt.