CompCertSSA
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…]
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…]
JSCert
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…]
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…]
