Towards Verification of Behavioral Software Contracts

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.

Speaker Bios

David Van Horn is a Research Assistant Professor in the Programming Research Lab at Northeastern University. He received his PhD in 2009 from Brandeis University and from 2009 to 2011 he was a CRA Computing Innovation Fellow at Northeastern.

Séries:
Microsoft Research Talks
Date:
Haut-parleurs:
David Van Horn
Affiliation:
Northeastern University

Taille: Microsoft Research Talks