This page describes the Ecdar tool architecture as of spring 2022.

Overview of the Architecture

The general design intent of having two verification engines, is that it should make the whole platform more reliable.


The intention of j-Ecdar is to be a form of reference implementation, where no effort is put into optimizing the code for speed, but rather for

  • Correctness
  • Readability


The intention of the Reveaal engine is to get a verification engine that is fast and parallelizable. Both over multiple cores, but also in the long run over multiple machines. The design goals for Reveaal are

  • Correctness
  • Speed
  • Remove dependency to UDBM

Ecdar GUI

The intention of the GUI is be quick and usable to create and edit models. It should provide visual feedback on the verification.

Test framework

Automated test of the two engines. This component is vital in order allow to obtain the ability to actually refactor code in the engines with confidence.

  • Hand designed test cases with known results
  • Conformance testing between the two engines
  • Automated performance testing