electrod

Formal analysis for the Electrod formal pivot language
README

Electrod is a model finder inspired by Kodkod. It takes as input a
model expressed in a mixture of relational first-order logic (RFOL)
over bounded domains and linear temporal logic (LTL) over an unbounded
time horizon.

Then Electrod compiles the model to a problem for a solver (currently
the NuSMV and nuXmv tools) to produce example or counter-example traces.

Electrod is mainly meant to be used as a backend for the Electrum Analyzer.

See the file INSTALL.md for building and installation instructions.

Home page

External dependencies

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

Running

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 tool by calling the electrod program.
Type electrod --help to get some help on options.

Copyright and license

(C) 2016-2019 ONERA

electrod is distributed under the terms of the Mozilla Public License v2.0.

See LICENSE.md for more information.

Install
Published
07 Dec 2019
Sources
electrod-0.4.1.tbz
sha256=b0bce9cc7126672feda5a02d5ef0c1131ba54db57654f80c0768c2f8d043cef9
sha512=92cc22f81522435e190039324767b6f69fa0b7d9dbfc3fb5561919823136fe492244dae993caf98633828e0090b67f306eec6270b86a1b2ff8630642130a3081
Dependencies
Reverse Dependencies