Abstract Reduction Semantics for Modular Higher-Order Contract Verification
The authors contribute a new approach to the modular verification of higher-order programs that leverages behavioral software contracts as a rich source of symbolic values. Their 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 their semantics gives an 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.