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


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

Skeletal Semantics and Necro

Skeletal Semantics consist of Skel, a meta language designed to describe the semantics of programming languages, and Necro, a set of tools to manipulate said descriptions. Skel, although minimal, can faithfully and formally capture many forms of specification, from inductive rules to complex algorithmic descriptions. Necro includes the generator of OCaml interpreters and Coq formalizations from semantics written in Skel. [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.