Software
OCaml Ecosystem
ocamlformat
Ocamlformat is an auto-formatter for OCaml, meaning it make the code prettier without changing its semantics. It is quite opinionated but also offers a lot of customizations. I have been the main maintainer of ocamlformat since 2018, in charge of fixing bugs, improving the user experience and customization, and drawing the roadmap. It has become the de facto formatter of the OCaml platform.
ocamlformat-preview
Ocamlformat-preview is a one-webpage preview of ocamlformat options in the browser. It serves as a showcase for ocamlformat's options and preset profiles and their impact on the formatted code. It is obtained by compiling ocamlformat with js_of_ocaml. It may lag behind the ocamlformat releases but gives a good idea of ocamlformat's features.
I also help maintain and improve a few more projects of the OCaml ecosystem: mdx, dune-release, odoc, odoc-parser, voodoo and the ocaml.org website.
Frama-C Plugins
Frama-C is a platform to analyze C software. As part of my PhD — that explored combining static and dynamic analyses for the software verification of C programs — I developed a few plugins for Frama-C.
StaDy
StaDy stands for Static and Dynamic verification of C programs. It leverages automated testing directed by code specification to help diagnose proof failures. More details can be found in the related research papers.
Mutation
Mutation is a plugin that generates mutant programs, i.e. program that are obtained by syntactically modifying the source program (either its code or its ACSL specification). It has been used to generate thousands of mutant programs to validate the StaDy approach and compare it against benchmarks.
Inline
Inline is another plugin that has been developed as part of the StaDy approach. As hinted by its name, it inlines the ACSL predicates and functions contained in the ACSL specification as a way to handle aliases. This allows to make StaDy work on complex specifications involving aliases that would otherwise require a more complex analysis.