Basic functions for OCaml codes

Lustre V6 compiler

Verimag's fork of CompCert

Self-stabilizing Algorithms SimulAtor

Tools and libs shared by Verimag/synchronous tools (lustre, lutin, rdbg).

RDBG stands for Reactive programs DeBuGger.

Its a programmable debugger that targets reactive programs for which a rdbg-plugin exists. Currently two plugins exist : one for Lustre, and one for Lutin (nb: both are synchronous programming languages).

Working in a compiler project using java

A tool for generating random task DAGs

A version of CompCert with

extra optimization a backend for the Kalray KVX core

Reproduce the experimental results of an article under submission (at the LITES journal) named :

''Improving WCET Evaluation using Counters and Linear Relation Analysis''

Reproduce experiments done in sasa related articles

A skitz compiler, made to compile mincaml as a University project.

DecentMon: an OCaml Benchmark for Decentralised Monitoring of LTL Formulae

An Ocaml implementation of the Turing Machine Constructions that have been described in many books but never implemented.

Reproduce the experimental results of an article currently under submission

"Assessing Software Abstractions inWCET Analysis of Reactive Programs"

cf http://www-verimag.imag.fr/TR/TR-2018-2.pdf