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

[David Van Horn]

Sorry, but due to tight travel constraints I wasn't able to get my 
slides in good enough shape to not waste people's time so I've decided 
to cancel this practice talk.

Thanks anyway,
David


On 10/18/12 12:35 PM, David Van Horn wrote:
> 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
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>