Static verification of performance properties of programs is an important problem that has attracted great deal of research. However, most existing tools infer best-effort upper bounds and hope that they match users expectations. In this talk, I will present a system for specifying and verifying bounds on resources such as the number of evaluation steps and heap-allocated objects, for functional Scala programs that may rely on lazy evaluation and memoization. In our system, users can specify the desired resource bound as a template with numerical holes in the contracts of functions e.g. as "steps <= ? * size(list) + ?", along with other functional properties necessary for establishing the bounds. The system automatically infers values for the holes that will make the templates hold for all executions of the functions. For example, the property that a function converting a propositional formula f into negation-normal form (NNF) takes time linear in the size of f can be expressed in the post-condition of the function using the predicate "steps <= ? * size(f) + ?", where size is a user-defined function counting the number of nodes in the syntax tree of the formula.
Using our tool, we have verified asymptotically precise bounds of several algorithms and data structures that rely on complex sharing of higher-order functions and memoization. Our benchmarks include balanced search trees like red-black trees and AVL trees, Okasaki’s constant-time queues, deques, lazy data structures based on numerical representations such as lazy binomial heaps, cyclic streams, and dynamic programming algorithms.
Some of the benchmarks have posed serious challenges to automatic as well as manual reasoning.
The system is a part of the Leon verifier and can be tried online at "
http://leondev.epfl.ch" ("Resource bounds" section).
References:
(a) Symbolic Resource Bound Inference For Functional Programs. Ravichandhran Madhavan and Viktor Kuncak. Computer Aided Verification, CAV 2014
(b) Contract-based Resource Verification for Higher-order Functions with Memoization. Ravichandhran Madhavan, Sumith Kulal and Viktor Kuncak. To appear in POPL 2017