Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn

			     S É M I N A I R E

                   ______                __    _
                  / ____/___ _____ ___  / /_  (_)_  ______ ___
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                                   En ligne

                             Lundi 14 juin, 10h30

                                --------------
                                Benoît Montagu
                                --------------

                                 Inria Rennes

                      =================================
                      Trace-Based Control-Flow Analysis
                      =================================

I will present some recent advances in control-flow analysis (CFA) for the
untyped lamba-calculus, a classic static analysis for higher-order languages.

First, I will explain how the well-known k-CFA analysis can be obtained in a
simple manner, by abstracting the execution traces of a lambda-term. To this
end, I will introduce a small-step semantics that builds a trace of the
control-flow events (calls, and returns of functions) that are produced by a
program. Using this technical development, the constraint-based formulation of
k-CFA can be proved sound in a modular way, as opposed to the usual method
based on "subject reduction".

Then, building on the previous development, I will introduce a novel
control-flow analysis, called nabla-CFA, that uses a widening operator.
Experiments show that nabla-CFA converges faster in practice compared to
k-CFA. Nabla-CFA also enables the use of domains of unbounded heights, such as
intervals---a new point in the design space of CFAs. I will discuss how
nabla-CFA compares to k-CFA in terms of cost and precision and, if time
permits, sketch some recent developments that solve some of the limitations of
nabla-CFA.

Part of this work will be presented at PLDI'21 at the end of June.