TITLES AND ABSTRACTS OF THE INVITED TALKS
Ran Canetti
(IBM T.J. Watson Research Center and MIT, USA), Composable Formal
Security Analysis: Juggling Soundness, Simplicity and Efficiency
Bruno Courcelle
(Labri, Universitè Bordeaux, France), Graph Structure and
Monadic Secondorder Logic: Language Theoretical Aspects
Javier Esparza
(Technische Universität München, Germany), Newtonian
Program Analysis
Abstract:
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. (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
interested in.
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 KnasterTarski'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, wellknown 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.
Muthu Muthukrishnan
(Google, USA), Internet Ad Auctions: Insights and Directions
Peter Winkler
(Dartmouth, USA), Optimality and Greed in Dynamic Allocation
Abstract: Online 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.
