Automata and applications Group

The Automata and applications (A∀) group at LRE concerns itself with automata in various forms and with their applications. The group maintains and develops the Spot library for manipulation of ω-automata and other software. Other research concerns itself with timed automata, weighted automata, automata for concurrency, and SAT solving.

Fields of interest

The A∀ group consists of approximately 13 permanent and several non-permanent staff. Some of our research interests, in roughly lexicographic order:

  • automata learning
  • concurrency theory
  • constraint programming
  • cyber-physical systems
  • games
  • language transformations
  • Lisp
  • LTL & PSL
  • model checking
  • ω-automata
  • parallelism
  • Petri nets
  • pushdown automata
  • quantitative verification
  • reactive synthesis
  • symbolic automata
  • timed automata
  • typesetting


The Automata and applications group hosts the following software projects:

  • Spot: a platform for LTL and ω-automata manipulation
  • Painless: a framework for implementation and evaluation of parallel SAT solvers
  • cosy: a library to exploit symmetries of SAT problems


The group is split over three sites, Paris, Rennes, and Toulouse.





Non-permanent members

Former members

  • Souheib Baarir
  • Sven Dziadek
  • Anissa Kheireddine
  • Nicolas Nalpon
  • Étienne Renault
  • Florian Renkin