Soft Contract Verification for Higher-Order Stateful Programs

Watch a 26-minute conference presentation from POPL 2018 exploring an innovative approach to static contract verification for higher-order stateful programs in Racket. Learn how researchers from the University of Maryland and Indiana University developed a method to verify software contracts ahead of runtime, achieving verification of 99.94% of checks across pure and stateful benchmarks. Discover solutions to the challenges of analyzing stateful higher-order functions in a modular way, including handling escaped closures to opaque contexts and managing arbitrarily expressive contracts. Understand the implementation of higher-order symbolic execution techniques and their formal proof of soundness through behavioral approximation. The presentation covers groundbreaking work that addresses the full complexity of untyped dynamic programming with higher-order functions, modularity, and statefulness in the mature Racket programming environment.