ReaTK is the Reactive System Verification and Synthesis ToolKit. It provides the ReaVer tool dedicated to the static verification of logico-numerical programs by abstract interpretation, and the ReaX tool performing discrete controller synthesis for such programs.

The controller synthesis tool ReaX was initially developed by Nicolas Berthier and Hervé Marchand from the SUMO Team at INRIA Rennes — Bretagne Atlantique. ReaX is a fork of the ReaVer tool originally implemented by Peter Schrammel.

This page is about the ReaX tool and its usage. Documentation about ReaVer is available here.


The recommended way for installing ReaTK is to use the OCaml Package Manager (OPAM). See for further instructions.


The project is distributed under the terms of the GNU General Public License. Its source code is hosted here.

Further Documentation

User Manual

The user manual gives some example executions of ReaX. It also describes the Controllable-Nbac language in which input systems (ASTSs) can be specified and outputs are generated.

Related Publications


Nicolas Berthier and Hervé Marchand. Discrete controller synthesis for infinite state systems with ReaX. In 12th Int. Workshop on Discrete Event Systems, WODES '14, May 2014. [ DOI ]

Nicolas Berthier and Hervé Marchand. Deadlock-Free Discrete Controller Synthesis for Infinite State Systems. In 54th IEEE Conference on Decision and Control, CDC '15, pages 1000--10007, December 2015. [ DOI ]


  • This project was supported by the French ANR project Ctrl-Green, funded by ANR INFRA and MINALOGIC.
  • The visual presentation of this page is highly based on Solarized CSS.

Author: Nicolas Berthier

Created: 2016-11-30 Wed 11:50