Proving Performance Properties of Functional Programs

Опубликовано 31 мая 2017, 22:25

Static verification of performance properties of programs is an important problem that has attracted a lot 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 resources usage bounds of functional programs that use data types, higher-order functions and memoization.

In our system, users can specify the desired resource bound as a template with numerical holes in the contracts of functions along with other correctness 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 inserting into a red-black tree takes time logarithmic in the size of the tree can be expressed in the post-condition of the insert function using the predicate "steps <= ? * log(size(tree)) + ?". Using our tool, we have verified precise bounds of several complex algorithms some of which have posed serious challenges to automatic as well as manual reasoning. Our benchmarks include balanced search trees like red-black trees and AVL trees, Okasaki's persistent, constant-time queues, lazy data structures based on numerical representations such as lazy binomial heaps, cyclic streams, and dynamic programming algorithms. The system is a part of the Leon Verification and Synthesis System and can be tried online at "leondev.epfl.ch" ("Resource bounds" section).

See more on this video at microsoft.com/en-us/research/v...