Skip to main content

Romain Brenguier

Personal photo - Romain Brenguier

Romain Brenguier

Research Assistant

Leaving date: 28th February 2017

Completed Projects:


I am a research assistant at University of Oxford.Working on the project Towards comprehensive verification of stochastic systems

Until september 2015 I was at ULB, member of the ERC inVEST project

See my dblp profile for a list of publications.


Please see my github profile for a list of projects I contriute to.

  • Praline: Tools for synthesis in multi-agent systems: computes Nash equilibria of concurrent games modelling interactions in a protocol.
  • AbsSynthe: A tool for the synthesis of reactive circuits. It competed in the SyntComp competition and won the first place in the sequential synthesis track in 2014 and in 2015.
  • Speculoos: A set of tools for generating AIGER circuits. Has been used to generate several sets of benchmarks for the SyntComp competition.
  • Reglisse: A tool to generate hardware description (AIGER and Verilog) from safety conditions given by regular languages.


  • Ocaml-cudd: An Ocaml interface to BDD and ADD functions of the CUDD library.
  • Ocaml-aiger: An Ocaml library to read, write and manipulate AIGER files.

Selected Publications

View AllManage publications

Completed Projects