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: 11 Jan 2021

Dependencies (20)

  1. odoc with-doc
  2. visitors >= "20190513"
  3. stdlib-shims
  4. stdcompat
  5. iter
  6. printbox < "0.6"
  7. ppx_deriving
  8. mtime < "2.0.0"
  9. menhir
  10. mdx with-test
  11. logs
  12. hashcons
  13. gen
  14. fmt >= "0.8.7"
  15. containers-data
  16. containers >= "3.0"
  17. cmdliner
  18. dune-build-info
  19. dune >= "2.7"
  20. ocaml >= "4.11.0"

Reverse Dependencies

    None

Conflicts

    None
Formal analysis for the Electrod formal pivot language

Install

Documentation github.com Readme Changelog MPL-2.0 License Edit opam file

Authors

  1. D
    David Chemouil
  2. J
    Julien Brunel

Maintainers

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

Sources

electrod-1.0.0.tbz
sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58
sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2