Projects

Extraction of synchronous-reactive models in Lustre from reactive programs written in C. Extracted models can be extended with synchronous observers and verified using model checkers such as Kind2 and GATeL

Extension of the Kind2 synchronous model checker with Statistical Model Checking (SMC)

Formal verification tool for the PsyC real-time language, developed during my PhD. It translates PsyC programs into synchronous models and verifies temporal properties using symbolic model checking.

SAT-based simulator and analysis tool for CCSL logical-clock constraints, implemented in OCaml, with VCD/GtkWave support and generation of synchronous Lustre observers.

A toy SAT solver implemented and formally verified using the Coq proof assistant.

Contribution of initial Netlink support to strace, the Linux system-call tracer, developed in C as part of the Google Summer of Code.