Bound Analysis of Imperative Programs with the Size-change Abstraction

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

The size-change abstraction (SCA) is an important program abstraction for termination analysis, which has been successfully implemented in many tools for functional and logic programs. In this talk, I will demonstrate that SCA is also a highly effective abstract domain for the bound analysis of imperative programs. I will introduce the first algorithm for bound computation with SCA and discuss how our methodology solves the technical challenges involved in bound computation. Further I will present two program transformations - pathwise analysis and contextualization - that make our SCA-based analysis precise enough to scale to real world programs. I will demonstrate the effectiveness of our approach by experiments with our tool Loopus on the cBench benchmark.