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

Subscribers:
344,000
Published on ● Video Link: https://www.youtube.com/watch?v=luy5r6pu4_s



Duration: 1:08:13
34 views
0


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).




Other Videos By Microsoft Research


2016-06-24Towards Understandable Neural Networks for High Level AI Tasks - Part 6
2016-06-24Symposium: Algorithms Among Us - Panel "Human-level AI – if, how, and when?"
2016-06-24KrishiPustak: A social networking system for low-literate farmers
2016-06-22NSF Interdisciplinary Workshop on Statistical NLP and Software Engineering - Session 7
2016-06-22Studio99 Presents: The 2015 Stranger Genius Nominees Show and Discuss Their Work
2016-06-22The Linear Algebraic Structure of Word Meanings
2016-06-22Single-shot error correction with the gauge color code
2016-06-22Panel: Progress in AI: Myths, Realities, and Aspirations
2016-06-22Studio99 Presents: Michael Gough and "Drawing as Literacy."
2016-06-22Comics and Stuff: An Introduction
2016-06-22Making Objects Count: A Shape Analysis Framework for Proving Polynomial Time Termination
2016-06-22Green Security Games
2016-06-22Panel 4: Publishing Content: The Article of the Future
2016-06-22Improving Urban Public Education: Lessons from Charter Schools
2016-06-22Coloring the Universe: An Insider's Look at Making Spectacular Images of Space
2016-06-22NSF Interdisciplinary Workshop on Statistical NLP and Software Engineering - Session 3
2016-06-22Theory and Experiments on the Spontaneous Evolution of Culture
2016-06-22NSF Interdisciplinary Workshop on Statistical NLP and Software Engineering - Session 2
2016-06-22Panel 3: Measuring Content: Evaluation, Metrics and Measuring Impact
2016-06-22NSF Interdisciplinary Workshop on Statistical NLP and Software Engineering - Session 8
2016-06-22NSF Interdisciplinary Workshop on Statistical NLP and Software Engineering - Session 5



Tags:
microsoft research
program languages and software engineering