Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization

We present a new approach for specifying and verifying resource utilization of functional programs that use lazy evaluation and memoization. Our approach verifies asymptotically tight bounds of complex programs that rely on deep sharing and aliasing of lazy heap references, as well as algorithms that use memoization extensively. Our approach can also find counter-examples for incorrect specifications or implementations. We demonstrate the effectiveness of the approach by verifying the resource bounds of several complex benchmarks, some of which have never been formally verified before. Examples include Okasaki's real-time queues, deques, lazy data structures based on numerical representations such as lazy binomial heaps, catenable queues, dynamic programming algorithms like weighted scheduling, and packrat parsing.

Related material