[PRL] Practice talk: Friday 4:30, Higher-Order Symbolic Execution via Contracts

[David Van Horn]

I'll be giving a practice talk for OOPSLA this Friday (tomorrow) at 4:30 
and your presence is appreciated.  Thanks!

David

Higher-Order Symbolic Execution via Contracts
Sam Tobin-Hochstadt, David Van Horn

We present a new approach to automated reasoning about higher-order 
programs by extending symbolic execution to use behavioral contracts as 
symbolic values, thus enabling symbolic approximation of higher-order 
behavior.

Our approach is based on the idea of an abstract reduction semantics 
that gives an operational semantics to programs with both concrete and 
symbolic components. Symbolic components are approximated by their 
contract and our semantics gives an operational interpretation of 
contracts-as-values. The result is an executable semantics that soundly 
predicts program behavior, including contract failures, for all possible 
instantiations of symbolic components. We show that our approach scales 
to an expressive language of contracts including arbitrary programs 
embedded as predicates, dependent function contracts, and recursive 
contracts. Supporting this rich language of specifications leads to 
powerful symbolic reasoning using existing program constructs.

We then apply our approach to produce a verifier for contract 
correctness of components, including a sound and computable 
approximation to our semantics that facilitates fully automated contract 
verification. Our implementation is capable of verifying contracts 
expressed in existing programs, and of justifying contract-elimination 
optimizations.

http://arxiv.org/abs/1103.1362