A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis

Speaker: Florian Zuleger , 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

Public: Yes

Location: G449

Event Type:

Room Description:

Host: Rishabh Singh, MIT CSAIL

Contact: Rishabh Singh, rishabh@csail.mit.edu

Relevant URL:

Speaker URL: None

Speaker Photo:
None

Reminders to: pl@lists.csail.mit.edu

Reminder Subject: 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
analysis.

Bio:
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.

Research Areas:

Impact Areas:

See other events that are part of the PL/SE Seminar Series 2013/2014.

Created by Rishabh Singh at Monday, October 28, 2013 at 11:03 AM.