Checking Data Structure Properties Orders of Magnitude Faster

Abstract. Executable formal contracts help verify a program at run-time when static verification fails. However, these contracts may be pro-hibitively slow to execute, especially when they describe the transforma-tions of data structures. In fact, often an efficient data structure opera-tion with O(log(n)) running time executes in O(n log(n)) when naturally written specifications are executed at run time. We present a set of techniques that improve the efficiency of run-time checks by orders of magnitude, often recovering the original asymptotic behavior of operations. Our implementation first removes any statically verified parts of checks. Then, it applies a program transformation that changes recursively computed properties into data structure fields, en-suring that properties are evaluated no more than once on a given data structure node. We present evaluation of our techniques on the Leon system for verification of purely functional programs.