Making Objects Count: A Shape Analysis Framework for Proving Polynomial Time Termination

Опубликовано 13 июня 2016, 20:23

We present a novel technique for verifying that (recursive) heap manipulating programs terminate in polynomial time. We achieve this by defining an unorthodox ranking function that tracks the number of loop iterations using logical counters distributed across heap objects. If every object counter is bounded, then the program belongs to large class of interesting programs whose running time is O(n k ), where n is the size of the input heap and k is the maximal loop-nesting depth. We soundly determine whether such a bound exists by generating a constraint system in the (decidable) quantifier-free fragment of Presburger arithmetic out of an abstraction of the program's transition relation. The latter can be computed by any shape analysis algorithm that enjoys certain natural properties. We have implemented a prototype analysis and successfully applied it to prove polynomial-time termination of a suite of benchmarks, including (looping and recursive) list manipulating programs, looping list-sorting programs, and looping programs that manipulate trees and graphs. This is joint work with Dr. Noam Rinetzky (Tel-Aviv University) and Boris Dogadov (Tel-Aviv University).