2011.12.19

Speaker:
David Van Horn
Northeastern University

Title:
Verification via Abstract Reduction Semantics

Time and place:
21/12/2011 in Turing 014 at 15:00

Abstract:
In this talk, I will describe a new approach to the modular
verification of higher-order programs that leverages behavioral
software contracts as a rich source of symbolic values. Our approach
is based on the idea of an abstract reduction semantics that gives
meaning to programs with missing or opaque components. Such components
are approximated by their contract and our semantics gives a
non-deterministic operational interpretation of contracts-as-values.
The result is a executable semantics that soundly approximates all
possible instantiations of opaque components, including contract
failures. It enables automated reasoning tools that can verify the
contract correctness of components for all possible contexts. We show
that our approach scales to an expressive language of contracts
including arbitrary programs embedded as predicates, dependent
function contracts, and recursive contracts. We argue that handling
such a feature-rich language of specifications leads to powerful
symbolic reasoning that utilizes existing program assertions. Finally,
we derive a sound and computable approximation to our semantics that
facilitates fully automated contract verification.

Joint work with Sam Tobin-Hochstadt