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.