![]() This project was for the Modèles et algorithmes des réseaux course at ENS, given by Ana Bušić, Marc Lelarge and Rémi Varloot. This was done as a project for the Foundation of proof systems course of the MPRI, given by Benjamin Werner and Pierre-Yves Strub.ĭistributed multiple voting (2017), with Noémie Fong Implementation and simulations of distributed multiple voting, based on this paper ( DOI). Executable weakest-precondition generator for the While language, written and verified using Coq. Verification of a weakest-precondition generator for the While language in Coq (2017). This was done as a project for the Foundation of proof systems course of the MPRI, given by Benjamin Werner and Pierre-Yves Strub. Specification of Peano and Heyting arithmetic, proof of some basic facts, as well as that Peano arithmetic is Π 0 2- conservative over Heyting arithmetic, verified using Coq. Verification of results on Peano and Heyting arithmeting in Coq (2017). The report (in French) contains some explainations on the invariants used to prove correctness. ![]() ![]() This was done as a project for the Proof of programs ( part 1, part 2) course of the MPRI, given by François Bobot and Jean-Marie Madiot. Implementation and verification of topological sorting using Wh圓. The report (in French) contains some additional information, including the typing rules. It also includes a generational garbage collector, but only the minor collection is implemented, and memory in the major heap is never reclaimed. The language being compiled supports curried functions, algebraic datatypes with deep pattern matching, algebraic effects ( archive) with multishot continuations, and a static type system based on MLsub ( DOI) with type and effect inference, including subtyping. Implementation of a compiler for a small functional language for the Functional programming and type systems course of the MPRI, given by François Pottier, Didier Rémy, Yann Régis-Gianas and Pierre-Évariste Dagand. School projects Compiler for a small functional language (2018). Here are the report and slides for the intership defense, as well as slides for an audience unfamiliar with abstract interpretation, and the paper we published at TACAS 2017 to present the results ( DOI, mirror). ![]() This work was done during my 2016 internship in the Chair of Programming Methodology at ETH Zürich, under the supervision of Caterina Urban. Design and implementation of improved widening operators for the FuncTion tool, an analyser for C programs based on abstract interpretation for deriving sufficient preconditions for termination, guarantee and recurrence properties. Improved widening operators for proving termination by abstract interpretation (2016). Here are the report, the slides for the internship defense and the paper ( DOI, mirror) we published about it after some additional work by Antoine Séré. This work was done during my 2017 internship in the CSL team, under the supervision of Natarajan Shankar. Implementation and verification in PVS of an idealized version of the PVS2C code generator. Verified code generation for the PVS2C code generator (2017). Here are the report, the slides for the internship defense (both in French), and the paper to appear at POPL21 about it. This work was done during my 2018 internship in the Gallium research team under the supervision of Xavier Leroy. Implementation and verification in Coq of the code generation step in the polyhedral model. Projects Work projects Verified code generation for the polyhedral model (2018).
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |