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

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(nk), 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).

Speaker Details

Roman Manevich is an assistant Professor at Ben-Gurion University of the Negev. His research interests include static analysis and verification of sequential and parallel programs, especially ones involving dynamic memory allocation. He is also interested in synthesizing parallel programs from high-level languages. He obtained his B.Sc., M.Sc., and Ph.D. in computer science from Tel-Aviv University where he was involved in the development of the TVLA system for 3-valued shape analysis. He has recently been involved in developing program synthesis techniques for parallel graph programs from implicitly parallel high-level languages (publications appearing in OOPSLA’12 and PLDI’15).

Series:
Microsoft Research Talks
Date:
Speakers:
Roman Manevich
Affiliation:
Ben-Gurion University Of the Negev

    • Portrait of Jeff Running

      Jeff Running

Series: Microsoft Research Talks