Research

Current work

I am currently doing an internship in the Celtique research team, with Thomas Jensen and Alan Schmitt. I am working on automatically extracting analyser from skeletal semantics.

Skeletal semantics are a way to specify the semantics of programming language at a fine-grained level, taking the primitive operations of the language as granted, similarly to what the main evaluation function of an interpreter would be once the primitives are defined. From these, it is possible to automatically extract an interpreter, or analysers such as abstract interpreters. I am currently working on extracting analysers giving interesting results on programs with non-static control flow, for languages that contain first-class functions, objects, or function pointers.

Previous work

Verified code generation for the polyhedral model

I did an internship from March to July 2018 in the Gallium research team, supervised by Xavier Leroy. During this internship, I worked on verifying the code generation step in the polyhedral model.

The goal of polyhedral compilation is to optimise loop nests and imperfect loop nests. It is traditionally separated in three steps: nested loops identification, reordering, and code generation. The first step transforms the original program into a representation where each instruction corresponds to the integer points of a polyhedron where it should be executed, with dependencies between some iterations, that mean they must be executed in some order. The second step is reordering, which modifies the original polyhedron into another with the same points, but preserving dependencies. The last and the one I worked on verifying is code generation, where this intermediate representation, after reordering, is transformed back into a traditional loop nest.

I wrote a code generator that does this last step in Coq, with Verimag's Verified Polyhedra Library to handle some polyhedral operations. The code generator handles code generation for perfect and imperfect loop nests (one or more than one polyhedra in its source language), and is fully verified using Coq. Its code can be found here. If you want to read more about it, you can read the report or slides for the internship defense (both in French).

Verified code generation for the PVS2C code generator

From March to July 2017, I was in the Computer Science Laboratory at SRI International, for an internship under the supervision of Natarajan Shankar. During that time, I worked on verifying the PVS2C code generator in PVS.

I did not work on verifying the whole PVS2C generator: indeed, it is written in Lisp, which PVS can not verify, and to the best of my knowledge, there is (or at least, was at that time) no formal semantics of PVS in PVS. Instead, I worked on verifying the code generation from an intermediate language in A-normal form to an imperative C-like language, most notably including the verification of reference counting and using destructive updates when possible.

The resulting code can be found here. The proof still is incomplete in some places, due to a combination of bugs of PVS either making the proof of some subgoals needlessly complicated, not asking to prove some subgoals before some fixes in PVS, and associating proofs with the wrong subgoals when rerunning proofs. Nevertheless, the proof is mostly complete, with only a few subgoals remaining that should be simple but tedious to prove, and it also allowed to spot the bugs of PVS in the first place. In case you want to read more about it, you can get the report or the slides for the internship defense.

Improved widening operators for proving termination by abstract interpretation

I spent seven weeks in June and July 2016 at Chair of Programming Methodology at ETH Zürich, for an internship supervised by Caterina Urban. I worked on improving the widening operators used in FuncTion, an analyser based on abstract interpretation that derives sufficient preconditions for termination, guarantee and recurrence properties of C programs.

FuncTion works by inferring ranking functions at each program point, that give an upper bound to the number of program steps needed before termination. As usual for abstract interpretation, termination of the analysis depends on the widening operators being used, which are heuristical in nature. Thus, they are often one of the main sources of precision or imprecision of the analysis. I improved the existing operators taking inspiration from this paper on precise widening operators for the domain of convex polyhedra.

The code of FuncTion, with includes my improvements, can be found here. If you want to know more about these improved widening operators, you can read my internship report, the slides for the defense, slides for an audience unfamiliar with abstract interpretation, or the paper we published about them (DOI, mirror).

Publications

Nathanaël Courant, Caterina Urban - Precise Widening Operators for Proving Termination by Abstract Interpretation.
TACAS 2017. (DOI, mirror)