package electrod

  1. Overview
  2. No Docs
Formal analysis for the Electrod formal pivot language

Install

Dune Dependency

grayswandyr.github.io Edit opam file Versions (14)

Authors

  1. D
    David Chemouil
  2. J
    Julien Brunel

Maintainers

  1. D
    David Chemouil <david.chemouil+git@onera.fr>

Sources

electrod-0.2.1.tbz
md5=15234055090589329f9e34bd7d5bd80b

Description

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 it compiles the model to a problem for a solver (currently the NuSMV and nuXmv tools) to produce example or counter-example traces.

Electrod is primarily meant to be used as a backend for the Electrum formal method and tool.

Published: 05 Nov 2018

Dependencies (15)

  1. visitors >= "20180513"
  2. stdcompat
  3. sequence >= "0.5"
  4. printbox < "0.6"
  5. ppx_inline_test < "v0.14"
  6. mtime
  7. menhir < "20211128"
  8. logs
  9. hashcons
  10. gen
  11. fmt
  12. containers >= "2.0" & < "3.0"
  13. cmdliner
  14. dune >= "1.4"
  15. ocaml >= "4.04"

Dev Dependencies

None

Used by

None

Conflicts

None