A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
, Technische Universität Wien
Date: Wednesday, October 30, 2013
Time: 2:30 PM to 3:30 PM Note: all times are in the Eastern Time Zone
Host: Rishabh Singh, MIT CSAIL
Contact: Rishabh Singh, email@example.com
Speaker URL: None
TALK: Wednesday 10-30-2013 A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
We present the first scalable bound analysis that achieves amortized complexity analysis. In contrast to earlier work, our bound
analysis is not based on general purpose reasoners such as abstract interpreters, software model checkers or computer algebra tools. Rather,
we derive bounds directly from abstract program models, which we obtain from programs by comparatively simple invariant generation and
symbolic execution techniques. As a result, we obtain an analysis that is
more predictable and more scalable than earlier approaches. Our experiments demonstrate that our analysis is fast and at the same time able to
compute bounds for challenging loops in a large real-world benchmark.
Technically, our approach is based on lossy vector addition systems (VASS).
Our bound analysis first computes a lexicographic ranking function that
proves the termination of a VASS, and then derives a bound from this
ranking function. Our methodology achieves amortized analysis based on
a new insight how lexicographic ranking functions can be used for bound
Florian Zuleger is an assistant professor at TU Vienna. He obtained his PhD from TU Vienna under the supervision of Helmut Veith. He is interested in the static and dynamic analysis of imperative programs. His current focus is on termination and bound analysis and on the verification of heap-manipulating programs.
Created by Rishabh Singh at Monday, October 28, 2013 at 11:03 AM.