>Bowl of porridge


Porridge is an OCaml library implementing Partial Order Reduction techniques for checking trace equivalence of security protocols.

It has been successfully integrated into two state-of-the-art verifiers DeepSec and Apte, bringing significant speedups.

The tool Porridge, underlying techniques and experimental results are formally described in the following paper:

Quick instructions to install and test Porridge


The code builds with OCaml 4.05.0 or later. It requires the Alcotest library >=0.8.1, and ocamlfind.

You may use opam to get these requirements, using the following commands once you have opam installed and up-to-date:

$ opam switch 4.05.0
$ eval `opam config env`
$ opam install ocamlfind alcotest

Then simply run:

$ make

In more details, make targets include:

$ make lib      # build only the library
$ make test     # test it
$ make porridge # build a utility to play with the lib on predefined examples
$ make doc      # build documentation for "toplevel" modules in doc/


To install/uninstall the library, run $ make install or $ make uninstall. The library will be usable with ocamlfind.

You can also use with opam:

$ opam pin add porridge .

Then $ opam install/uninstall/upgrade porridge can simply be used to install, uninstall, or upgrade the porridge library based on the latest sources.

Once the library is installed, you can install the modified version of DeepSec or Apte that leverages Porridge for reducing the search space.


The src/ subdirectory contains the code. The main modules are:

See doc subdirectory, after running make doc, for more details.

We also use various utility modules, including:

Porridge and its integration in DeepSec and Apte are developed by D. Baelde, S. Delaune and L. Hirschi.

Last update: April 11th 2018.