Electrum is a formal specification language mixing relational first-order logic (RFOL) and linear temporal logic (LTL), mainly inspired by Alloy and TLA+.

Electrum Analyzer is a free-software prototype for the analysis of Electrum models: it curently proceeds by translation into SMV models processable by NuSMV and nuXmv (more efficient in practice).

Pre-compiled binaries are currently available in the Files tab. The prototype is also available through opam, the package management system for OCaml. In a shell, type the following to get it:

opam update
opam install electrumAnalyzer

This work has been funded by Onera, ANR/DGA Astrid project Cx and RTRA STAE project Briefcase.