Software

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

Comments are closed.