PV4 Electrum Analyzer (sometimes called 'Electrum')checks assertions and LTL properties in Electrum models with bounded or unbounded model checking

Model checker for Electrum specifications

Application domain/field

Type of tool

Model checker

Expected input


Electrum language


Electrum is an extension of Alloy that enriches its relational logic with LTL operators. The Electrum Analyzer can do bounded model checking (encoded into SAT) and unbounded model checking (encoding into SMV) There are two main commands to analyse Electrum models: There is a visualiser to inspect the results of the run and check commands.


License: Apache License 2.0
LTL Model checking


Related papers

https://doi.org/10.1145/3238147.3240475 (ASE '18)

Last publication date

3 September 2018

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.