Behavioral software contracts are a widely used mechanism for governing the flow of values between components. However, run-time monitoring and enforcement of contracts imposes significant overhead and delays discovery of faulty components to run-time.

In this talk, I will present our work on soft contract verification, which overcomes the above issues by proving contract correctness or producing a counterexample.

The approach is able to analyze first-class contracts, recursive data structures, unknown functions, and control-flow-sensitive refinements of values, which are all idiomatic in dynamic languages. It makes effective use of an off-the-shelf solver to decide problems without heavy encodings.  Our theoretical results include soundness and relative completeness.  The approach is competitive with a wide range of existing tools---including type systems, flow analyzers, and model checkers---on their own benchmarks.

Joint work with Phúc C. Nguyen (UMD) and Sam Tobin-Hochstadt (IU)

See also:

Relatively complete counterexamples for higher-order programs, Phúc C. Nguyen and David Van Horn, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015. 

Soft Contract Verification, Phúc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn, Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, 2014.