CompCertSSA is built on top of the C CompCert verified compiler, by adding a SSA-based middle-end (conversion to SSA, SSA-based optimizations, destruction of SSA). [More…]


FPSE is a symbolic execution tool for C/C++/Java programs, based on Constraint Programming technology. Its applications include automatic test data generation and constraint-based testing. [More…]

Javalib / Sawja

Javalib is a library to access Java class files from OCaml. It was initially developped by Nicolas Canasse and then extended by the Celtique team. Sawja is a library developped on top of Javalib to represent complete programs. [More…]


The JSCert project aims to really understand JavaScript. JSCert itself is a mechanised specification of JavaScript, written in the Coq proof assistant, which closely follows the ECMAScript 5nglish standard. JSRef is a reference interpreter for JavaScript in OCaml, which has been proved correct with respect to JSCert and tested with the Test 262 test suite. [More…]


Nit, the Nullability Inference Tool, infers nullness properties of variables and can prove that a program is NullPointerException free. It allows to find suitable nullability annotations for fields, method parameters, return values and local variables. It works at the bytecode level (on .class files or .jar files) so it can be used on programs where the source is not available. While this can look strange for a programmer, this tool can also be used by other static analyses to improve their precision. [More…]

Object initialization type checker

This type checker allows to check that objects accessed in Java programs are completely initialized. This allows to enforce security properties whithout heavy code modifications. [More…]

SPAN: a Security Protocol Animator

SPAN is a tool to help protocol designers in debugging HLPSL (High-Level Protocol Specification Language) specifications. It allows to animate them, i.e. interactively produce Message Sequence Charts (MSC for short) which can be seen as an “Alice et Bob” trace from an HLPSL specification. [More…]

Timbuk: a Tree Automata Library

Timbuk is a library of Ocaml functions for manipulating tree automata. More precisely Timbuk deals with finite bottom-up tree automata (deterministic or not). [More…]

Comments are closed