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)
-
odoc
with-doc
-
visitors
>= "20190513"
- stdlib-shims
- stdcompat
- iter
-
printbox
< "0.6"
- ppx_deriving
-
mtime
< "2.0.0"
- menhir
-
mdx
with-test
- logs
- hashcons
- gen
-
fmt
>= "0.8.7"
- containers-data
-
containers
>= "3.0"
- cmdliner
- dune-build-info
-
dune
>= "2.7"
-
ocaml
>= "4.11.0"
Reverse Dependencies
-
None
Conflicts
-
None
Formal analysis for the Electrod formal pivot language
Install
copied = false, 2000)"
:class="{ 'border-gray-700': !copied, 'text-gray-100': !copied, 'focus:ring-orange-500': !copied, 'focus:border-orange-500': !copied, 'border-green-600': copied, 'text-green-600': copied, 'focus:ring-green-500': copied, 'focus:border-green-500': copied }">
Authors
Maintainers
Sources
electrod-1.0.0.tbz
sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58
sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2