[Pl-seminar] 10/19: David Van Horn, "Verification via Abstract Reduction Semantics"

[Aaron Turon]

NEU Programming Languages Seminar presents

David Van Horn
Northeastern University

Wednesday, 10/19

11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Verification via Abstract Reduction Semantics

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.

My talk will focus on current work in progress and emphasize future
directions.  There are interesting avenues for new work in testing,
model checking, and theorem proving that we hope to explore.  We are
actively seeking potential collaborators.

Joint work with Sam Tobin-Hochstadt