Projects

Implementation of the methodology proposed in my doctoral thesis: a formal verification tool for the PsyC language based on SAT and BDD model-checkers. The project is implemented mainly in OCaml and makes extensive use of the synchronous language Lustre, in particular as an intermediate representation.

CLOCK (Copilot of Logical Operational Constraint Kernels) is an implementation of a CCSL simulator based on a SAT solver with several heuristics. The project is implemented in OCaml and is compatible with the VCD format and the GtkWave tool. It is also possible to generate synchronous observers in Lustre.

CoqSAT is an attempt to make a highly simple SAT solver but proven using Coq.

Design and implementation of a digital circuit simulator accelerated by a graphics processing unit (GPU). The tool generates scheduled gate-level clusters synchronized with time barriers. It is implemented in Python, C++ with GPU kernels using OpenCL. This project was my end-of-studies engineering project.

Implementation of the initial Netlink support in the strace utility, the Linux system tracer. This project, implemented in C, was funded by the Google Summer of Code (GSoC) program.