Scaling up Abstract Interpretation: Efficient and Precise Static Analyses for Large Programs

idea of approximation. It can be used both to verify and optimize
programs. Applying this theory to large and complex programs presents
a number of theoretical and practical challenges, that must be tackled
to obtain the full power of abstract interpretation in practice. All
features of real languages must be analyzed. New analyses, that scale
up and that yield a good tradeoff between cost and precision, must be
designed. My talk will present my previous work and my projects in
this area.

On the one hand, I have designed fast and precise escape analyses,
that have been applied to stack allocation for ML and Java and to
synchronization elimination for Java. I have fully implemented these
analyses in compilers. On the other hand, I have also designed and
implemented a cryptographic protocol verifier, that can prove secrecy
properties of protocols, without limiting the number of sessions of
the analyzed protocol. This verifier is efficient enough to handle
complex protocols.

My projects for the research group aim at designing new analyses that
also scale up. First, the work on cryptographic protocols would be
continued, to verify other properties and to analyze implementations
of protocols instead of specifications. Second, new analyses would be
designed for verifying mobile code, in particular the Java platform
and Java software. At last, the verification of critical software will
be a key objective, since an error in such software can have very
serious consequences.