TITLES AND ABSTRACTS OF THE INVITED TALKS
(IBM T.J. Watson Research Center and MIT, USA), Composable Formal
Security Analysis: Juggling Soundness, Simplicity and Efficiency
(Labri, Universitè Bordeaux, France), Graph Structure and
Monadic Second-order Logic: Language Theoretical Aspects
(Technische Universität München, Germany), Newtonian
In this talk I'll look at a sequential program as a system of
equations of the form
X1 = f1(X1, ..., Xn)
Xn = fn(X1, ..., Xn)
where the fi's are polynomials, and sum and product
correspond to choice and sequential composition. (If you're familiar
with process algebras, this should ring a bell.) I'll argue that
static program analysis is the art of solving these equations over
different interpretations, depending on the information one is
40 years of research on static analysis 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 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.
Joint work with Stefan Kiefer and Michael Luttenberger.
(Google, USA), Internet Ad Auctions: Insights and Directions
(Dartmouth, USA), Optimality and Greed in Dynamic Allocation
Abstract: On-line problems arise often in industry,
but even in simple cases it seems impossible to prove that a given
algorithm is optimal without assuming some precise input distribution.
Rather than settle for a competitive ratio result, we offer a method
for proving optimality in dynamic allocation problems which relies on
the assumption that "it's right to be greedy." The method is applied
to two problems which arose at Lucent Technologies.