Soft Contract Verification
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn

TL;DR
This paper introduces soft contract verification, a static analysis method for untyped, higher-order languages that reduces runtime overhead by proving contract correctness using symbolic execution and contract invariants.
Contribution
It presents a novel static verification approach that handles first-class contracts, recursive data, and control-flow refinements in dynamic languages, improving over existing tools.
Findings
Sound symbolic execution approximates dynamic semantics.
Verified programs cannot be blamed.
Competitive performance on standard benchmarks.
Abstract
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. To overcome these issues, we present soft contract verification, which aims to statically prove either complete or partial contract correctness of components, written in an untyped, higher-order language with first-class contracts. Our approach uses higher-order symbolic execution, leveraging contracts as a source of symbolic values including unknown behavioral values, and employs an updatable heap of contract invariants to reason about flow-sensitive facts. We prove the symbolic execution soundly approximates the dynamic semantics and that verified programs can't be blamed. The approach is able to analyze first-class contracts,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
