Boris Yakobowski

research and other interests
Me

Entries

5 Jun 2015

Improving Static Analyses of C Programs with Conditional Predicates

Category: Research

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

Category: Research

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

Category: Research
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

Category: Research
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

Category: Research
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:

1 Feb 2008

Vallée de Chamonix

Category: Photography

Twelve pictures of the Chamonix Valley, taken in december 2007, are now online.

2 Dec 2007

15 Nov 2007

BNF and neighbourhood

Category: Photography

Six pictures of The Bibliothèque Nationale François Mitterrand, and of its neighbourhood, are now online.

1 Oct 2007

Updated Nice titles

Category: Software
Created: 10 Mar 2007

Back in 2003, Stuart Langridge popularized what became known as “Nice Titles”. In essence they consist in a bit of javascript code that displays fancy hovering boxes on top of links, as can be seen here.

Nice titles have became hugely popular, and many people proposed variants. I will mention those of Dunstan Orchard and Mark Wubben. This entry presents yet another implementation, with some features found only in some of the above versions, and some entirely new. I've also corrected what I believed to be bugs.

What's in this version?

  • The nicetitles follow the mouse.
  • The size of the nicetitles is not fixed. This avoids some overflow problems when their content is too big.
  • The nicetitles do not go outside of the window, and they try moderately hard not to appear on top of the mouse cursor.
  • The nicetitles appear after a little delay (and e.g. ‘sup’ tags inside the text of the anchors do not cause delays).
  • Nicetitles can be used to display image thumbnails. Currently, ‘img’ tags with the ‘thumb’ class automatically receive thumbnails; see the photographs on the right.
  • The code is modular and hides the functions that should not be redefined by other javascript modules.
  • The code is thoroughly tested under various versions of Gecko, Internet Explorer (versions 6 and 7), Opera (versions 8 and 9), Konqueror and Safari 3 (for Windows).

The source code is available, as a plain .js file or pretty-printed. You also need to add inside the file an implementation of the addEvent function that correctly handles the scopes for the ‘this’ keyword. I currently use Justin Diaz's version.

Finally, the css stylesheet I use on this site can be used as an example to format the nicetitles boxes.


I am interested to hear about any problem encountered while using this code. My mail can be found on this page, should you wish to contact me.

Updates:

  • 2007-10: fixed a bug in Safari

8 May 2007

January in Nice

Category: Photography

A gallery of pictures taken during my stay in Nice in January has been uploaded.

18 Jan 2007

Random photographs

Category: Photography

I've put online some very old photos I took in 2005 and 2006: a group of construction workers lifting something heavy (this picture was taken in Tallinn during ICFP 2005), an oriental lamp, and Paris's city hall's square on January 1st.

10 Sep 2006

ICFP Programming Contest 2006 - Untyped raytracers and polymorphic variants

Category: Software

Alain Frisch has created a webpage about our participation to the 2006 ICFP programming contest. This year's problems were quite varied, and my main contribution was to solve the raytracer subproblem.

The raytracer had to be written in a langage where functions are 2D boxes composed of wires. Those wires link atomic boxes that themselves perform operations of construction and deconstruction on completely untyped objects. I wrote an ML solution to the problem (this was in itself non-trivial), and we compiled it into a 2D function using code written by Alain and Nicolas.

The main peculiarity of my solution is that it is typed, even though it dutifully follows the untyped representation of the specification. I used polymorphic variants, which enabled me to define the type (for example) of ray-tracing values or of lists as subtypes of the generic value type.

type value = [
    | `Unit
    | `Pair of value * value
    | `Inl of value
    | `Inr of value ]


type valrt = [ `Inl of u
             | `Inr of [ `Inl of u
                       | `Inr of [`Inl of u]]]

type 'a vlist = [ `Inl of [`Pair of 'a * 'b]
                | `Inr of [`Unit]
                ] as 'b
                

The full solution is available, as a ml file or as a pretty-printed html page. More details on the rest of our submission can be found on our team's page.

28 Oct 2005

Replacing applications by let constructs in OCaml

Category: Software

In ML-based languages, the construction let x = e in e' is equivalent, at execution-time, to (fun x -> e') e. However this property does not hold during type-checking: the let construct permits to generalize the type variables which are free in the environment; this way, more polymorphism can be introduced.

Consequently, it is potentially helpful to replace all applications by let bindings. In OCaml, this can be done automatically by Camlp4 (this patch is intended for OCaml 3.09; otherwise, change _loc to loc).

To compile a cmo usable as a parser by Camlp4, use ocamlc -I +camlp4 -pp "camlp4r pa_extend.cmo q_MLast.cmo" -c pa_o_let_extend.ml. You can create an extended Camlp4 executable by using mkcamlp4 -o $(CAMLP4LET) pa_o.cmo pa_o_let_extend.cmo pr_o.cmo (for a Camlp4 accepting the original syntax as input).

Thanks to Daniel de Rauglaudre and Michel Mauny, who have been instrumental in helping me write this extension.

25 Sep 2004

ICFP Programming Contest 2004

Category: Software
Created: 21 Sep 2004

As we guessed (we were warned in advance that we had won a prize, and the performances of our ants seemed too low to win one of the first two prizes), we have won the Judge's Prize of the ICFP Programming Contest 2004. As expected, we received the prize thanks to the design of our intermediate language (the ultimate goal was to compile ant brains) ; the compiler was mainly due to Xavier Leroy, with additions from Damien Doligez and myself.

A full webpage for our submission is now available, thanks to Yann.

Random photographs

ThumbnailThumbnailThumbnailThumbnailThumbnailThumbnail