Technische Universitat Muenchen
3pm Thursday, 31st of March, 2009
Room 4.31/4.33, Informatics Forum
In this talk I'll look at a sequential program as a system of equations of the form X_1 = f_1(X_1, ..., X_n) ... X_n = f_n(X_1, ..., X_n) where the f_i's are polynomials, and sum and product correspond to choice and sequential composition. I'll argue that static program analysis is the art of solving these equations over different interpretations, depending on the information one is interested in.
After 40 years of research on static analysis we have not produced much theory on *generic* methods for solving these equations, i.e., on methods that work for *any* interpretation. The ones around are based on Knaster-Tarski's and Kleene's theorems. Unfortunately, these methods rarely terminate for infinite domains, and in metric interpretations their convergence is often hopelessly slow. Can't we do better?
I'll show that Newton's method, well-known from numerical mathematics, can be generalized to (almost) arbitrary interpretations, and that this generalization provides a unified view of many results of language theory, as well as a bridge between qualitative and quantitative program analysis.
This is joint work with Stefan Kiefer and Michael Luttenberger.