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...]

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...]

FPSE

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...]

Micromega

Micromega is a fast Coq reflexive tactics for linear (and bits of non-linear) arithmetics. [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...]

Nit

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...]