Electrod is a model finder for first-order linear temporal logic with relations, transitive closure and partial domains.

As of now, Electrod relies on NuSMV or nuXmv (default), so you must at least install one of them.

Electrod is primarily aimed at being called by external, more abstract tools, such as the Electrum Analyzer. However, it can also be run as a standalone program.

This prototype program is maide available under the Mozilla Pulic License 2.0.
Releases are mainly available through OPAM (opam install electrod) or can be downloaded from the Github mirror page.

Latest news

First public release of Electrod
Electrod is now available publically!
Added by David Chemouil over 3 years ago

View all news


Manager : David Chemouil

Développeur : Alcino Cunha, David Chemouil, Julien Brunel, Nuno Macedo

Invite: electro guest