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

JavaLib is a library to access Java class files from OCaml. It was initially developped by Nicolas Canasse and then extended by the Lande team. [More...]