Boris Yakobowski

research and other interests


5 Jun 2015

Improving Static Analyses of C Programs with Conditional Predicates

Joint work with Sandrine Blazy and David Bühler.

In this paper, we present a generic abstract interpretation based framework to enhance the precision of analyses on codes containing multiple successive conditionals. We introduce predicated domains, that preserve and reuse information valid only inside some branches of the code. Our predicates, derived from the conditional statements of the program, postpone the loss of information caused by joins.

The work has been integrated into Frama-C as a new plugin. Experiments on real code show that our approach scales, and improves significantly the precision of the Value Analysis plugin of Frama-C.

This article has been published in the proceedings of FMICS 2014, where it was awarded the best paper award. Here are the pdf and the link at the publisher's website. A journal version is under consideration for publication.

Coq proofs of the results in the journal version: .v file, or as an html page.

15 Jul 2009

xMLF, a Church-style intermediate language for MLF

Didier Rémy and I have written an article completing the MLF "trilogy", entitled A Church-style intermediate language for MLF. We describe an explicit language for a lambda-calculus with (MLF-style) flexible quantification; the language, called xMLF, extends the explicit version of System F with a new form of type applications. Using xMLF, it becomes possible to use MLF in a compiler that uses a typed intermediate language. We describe how to elaborate the results of the (graphical) MLF type inference algorithms into xMLF terms.

The article is currently submitted for publication; a preliminary version is available here. See also those slides (2009-02-09, Gallium seminar, in english), or those of Didier Rémy's talk at IFIP.

19 May 2009

The ` character to the rescue

Created: 8 Oct 2007

I have presented, during the Journées Francophones des Langages Applicatifs 2008, an article entitled Le caractère ` à la rescousse - Factorisation et réutilisation de code grâce aux variants polymorphes ("The ` character to the rescue - Code factorization and reuse using polymorphic variants", but the article is only available in french for the moment). It provides a hopefully gentle introduction to polymorphic variants, a feature of the typing system of OCaml.

Here is the source code of the examples: introduction, section 2, section 3 and section 4.

The abstract and the BibTeX entry can be found on my publications page.

Three different presentations of this work are available (all three are in french)

1 Feb 2009

PhD thesis

Created: 7 Jul 2008

I have defended my PhD «Graphical types and constraints: second-order polymorphism and inference» on December 17th, 2008. The jury was composed of

Pr. Stephanie Weirich University of Pennsylvania
Hugo Herbelin INRIA
Pr. Fritz Henglein University of Copenhagen
Roberto Di Cosmo University Paris 7
Alexandre Miquel University Paris 7, ENS Lyon
Didier Rémy (PhD advisor) INRIA

The final version of the manuscript can be found on TEL, or directly here in color or in black & white. There also exist fully english versions, in color and in black & white. BibTeX entries can be found on my publications page. The slides of the defense are also available.

22 Sep 2008

Graphic type constraints and efficient type inference: from ML to MLF

Created: 17 Jul 2007

This paper, presented at ICFP'08, describes ML type inference in an entirely graphical setting, and shows that MLF type inference is only a very simple generalization of the ML case. Our approach is constraints-based; we give some equivalence rules on constraints, as well as an algorithm to solve them. We also show that type inference for MLF has linear complexity in practice, as in ML.

The full abstract for the paper can be found in my publications page. Compared to the published version, this version corrects some small mistakes in Definitions 9 and 11, and in Figure 17. The long version is available as Part 2 of my PhD dissertation.

Some talks I gave about this work:

9 Apr 2008

Prototype implementation of a MLF typer

Created: 25 Jul 2007

A proof-of-concept prototype implementation of an MLF typer, based on the results presented in our last paper, is online, and has been slightly updated. The source code is now also available.

16 Jan 2007

A graphical presentation of MLF types with a linear-time local unification algorithm - TLDI 2007

Created: 14 Feb 2006

Didier Rémy and I have written a paper on a graph-based presentation of the types of the MLF language. This paper has been presented at the TLDI'07 workshop. The submitted version of the paper (with a few typos corrected) is available, as well as a black and white version, and the slides I presented at the workshop.

Since its publication, we have made some important revisions to this work. A much developed version is available as Part 1 of my PhD dissertation.

The abstract of the paper, as well as a BibTeX entry, can be found in my publications page.

This work is the continuation of what I presented at the APPSEM II Workshop, and entirely supersedes it.

15 Sep 2005

APPSEM Workshop talk

I've presented at the 3rd APPSEM II Workshop a talk about some preliminary results of my thesis. More precisely, they consist in a reformulation of MLF using graphs for the representation of types. This is the corresponding extended abstract.

The slides I've used are here in pdf, or there for Advi users (the Advi version contains more transitions, but needs some manual recentering).

Note that all the content presented in the extended abstract is developped in this article.

28 Sep 2004

PhD Thesis Work

The subject of my PhD Thesis is now online. It is entitled (in french) « Polymorphisme d'ordre omega avec inférence partielle mis en pratique »; I'm going to extend Didier Rémy and Didier Le Botlan's MLF.

13 Sep 2004

Certified compilation in SSA form

I've defended today my Master Thesis, about certified compilation using an intermediate language in SSA form. The report and the slides I've presented are available, in pdf (in french only).

28 Aug 2004

Term enumeration

Created: Apr 2004

Using the resultas of an internship I did in the Ultra Group, Joe Wells and I have written a paper entitled « Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis », which was submitted to LOPSTR'04 (this is the version found in the preliminary proceedings of the conference).

I have presented the paper at LOPSTR'04 in Verona, Italy. The slides I used are here; you need advi to view them.

A final version of the paper is also available. Please note that the preliminary one is slightly more complete, as it includes an appendix not found in the final paper.

Finally, the abstract of the paper can be found in my publications page.

Random photographs