From dff0d58ccc6fad6c99eb443f5343d2e244e09263 Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Mon, 23 Jun 2025 14:05:05 -0600 Subject: [PATCH] rebuild after many tool additions --- .gitea/index.html | 110 + .gitea/index.xml | 25 + .gitea/issue_template/add_tool/index.html | 138 + .gitea/issue_template/fix_tool/index.html | 138 + about/index.html | 2 +- applications/hybrid-systems/index.html | 130 + applications/hybrid-systems/index.xml | 19 + applications/index.html | 108 + applications/index.xml | 42 + applications/model-checker/index.html | 255 + applications/model-checker/index.xml | 210 + applications/model-generator/index.html | 131 + applications/model-generator/index.xml | 19 + applications/modeling-framework/index.html | 130 + applications/modeling-framework/index.xml | 19 + applications/modeling-language/index.html | 147 + applications/modeling-language/index.xml | 33 + applications/parameter-synthesizer/index.html | 130 + applications/parameter-synthesizer/index.xml | 19 + .../probabilistic-program-prover/index.html | 131 + .../probabilistic-program-prover/index.xml | 19 + applications/smt-solver/index.html | 2 +- applications/smt-solver/index.xml | 2 +- applications/theorem-prover/index.html | 18 + applications/theorem-prover/index.xml | 14 + developers/-leslie-lamport/index.html | 130 + developers/-leslie-lamport/index.xml | 19 + developers/aalborg-university/index.html | 147 + developers/aalborg-university/index.xml | 33 + developers/bell-labs/index.html | 131 + developers/bell-labs/index.xml | 19 + .../disi-university-of-trento/index.html | 2 +- .../disi-university-of-trento/index.xml | 2 +- .../index.html | 8 + .../index.xml | 7 + .../federal-university-of-amazonas/index.html | 130 + .../federal-university-of-amazonas/index.xml | 19 + .../fondazione-bruno-kessler/index.html | 19 +- developers/fondazione-bruno-kessler/index.xml | 16 +- developers/index.html | 432 ++ developers/index.xml | 168 + developers/inria-rocquencourt/index.html | 130 + developers/inria-rocquencourt/index.xml | 19 + developers/iscas/index.html | 130 + developers/iscas/index.xml | 19 + developers/jonathan-nadal/index.html | 131 + developers/jonathan-nadal/index.xml | 19 + developers/laas-cnrs/index.html | 138 + developers/laas-cnrs/index.xml | 26 + developers/lean-fro/index.html | 131 + developers/lean-fro/index.xml | 19 + .../index.html | 131 + .../index.xml | 19 + developers/matthew-fernandez/index.html | 140 + developers/matthew-fernandez/index.xml | 26 + developers/rwth-aachen/index.html | 17 + developers/rwth-aachen/index.xml | 14 + developers/saarland-university/index.html | 130 + developers/saarland-university/index.xml | 19 + .../index.html | 130 + .../universidad-nacional-de-cordoba/index.xml | 19 + .../universite-sorbonne-paris-nord/index.html | 130 + .../universite-sorbonne-paris-nord/index.xml | 19 + developers/university-of-bristol/index.html | 130 + developers/university-of-bristol/index.xml | 19 + developers/university-of-iowa/index.html | 9 + developers/university-of-iowa/index.xml | 7 + .../university-of-manchester/index.html | 130 + developers/university-of-manchester/index.xml | 19 + developers/university-of-nantes/index.html | 131 + developers/university-of-nantes/index.xml | 19 + .../university-of-southampton/index.html | 130 + .../university-of-southampton/index.xml | 19 + .../university-of-stellenbosch/index.html | 130 + .../university-of-stellenbosch/index.xml | 19 + developers/university-of-twente/index.html | 147 + developers/university-of-twente/index.xml | 33 + developers/uppsala-universitet/index.html | 138 + developers/uppsala-universitet/index.xml | 26 + developers/uppsala-university/index.html | 140 + developers/uppsala-university/index.xml | 26 + developers/verimag/index.html | 130 + developers/verimag/index.xml | 19 + developers/vertics/index.html | 130 + developers/vertics/index.xml | 19 + index.html | 348 +- index.xml | 263 +- inputs/heyvl/index.html | 131 + inputs/heyvl/index.xml | 19 + inputs/index.html | 18 + inputs/index.xml | 7 + interfaces/cli/index.html | 11 +- interfaces/cli/index.xml | 9 +- interfaces/index.html | 18 + interfaces/index.xml | 7 + interfaces/vscode/index.html | 131 + interfaces/vscode/index.xml | 19 + licenses/agpl-v3/index.html | 130 + licenses/agpl-v3/index.xml | 19 + licenses/all-rights-reserved/index.html | 35 +- licenses/all-rights-reserved/index.xml | 30 +- licenses/apache-2.0/index.html | 59 + licenses/apache-2.0/index.xml | 49 + licenses/bsd-3-clause/index.html | 130 + licenses/bsd-3-clause/index.xml | 19 + licenses/bsd-4-clause/index.html | 130 + licenses/bsd-4-clause/index.xml | 19 + licenses/bsd/index.html | 51 + licenses/bsd/index.xml | 42 + licenses/bsl/index.html | 139 + licenses/bsl/index.xml | 26 + licenses/gpl/index.html | 131 + licenses/gpl/index.xml | 19 + licenses/gplv2/index.html | 17 + licenses/gplv2/index.xml | 14 + licenses/gplv3/index.html | 32 + licenses/gplv3/index.xml | 28 + licenses/index.html | 162 + licenses/index.xml | 63 + licenses/isc/index.html | 131 + licenses/isc/index.xml | 19 + licenses/lgpl/index.html | 131 + licenses/lgpl/index.xml | 19 + licenses/mit/index.html | 75 + licenses/mit/index.xml | 63 + licenses/open-source-3.0/index.html | 139 + licenses/open-source-3.0/index.xml | 26 + licenses/unilicense/index.html | 140 + licenses/unilicense/index.xml | 26 + maintenance/actively-maintained/index.html | 258 +- maintenance/actively-maintained/index.xml | 212 +- maintenance/not-maintained/index.html | 57 + maintenance/not-maintained/index.xml | 49 + sitemap.xml | 243 + taxonomies/index.html | 731 +++ techniques/car/index.html | 131 + techniques/car/index.xml | 19 + techniques/index.html | 36 + techniques/index.xml | 14 + techniques/pdr/index.html | 131 + techniques/pdr/index.xml | 19 + tools/index.html | 4300 ++++++++++++++++- tools/mc/blast/index.html | 336 ++ tools/mc/cadp/index.html | 311 ++ tools/mc/cgaal/index.html | 267 + tools/mc/concuerror/index.html | 299 ++ tools/mc/cpachecker/index.html | 311 ++ tools/mc/dscheck/index.html | 297 ++ tools/mc/eldarica/index.html | 297 ++ tools/mc/esbmc/index.html | 435 ++ tools/mc/geyser/index.html | 314 ++ tools/mc/imitator/index.html | 299 ++ tools/mc/imspin/index.html | 267 + tools/mc/index.html | 3698 ++++++++++++++ tools/mc/index.xml | 224 + tools/mc/intrepyd/index.html | 287 ++ tools/mc/kind2/index.html | 299 ++ tools/mc/ltsa/index.html | 257 + tools/mc/ltsmin/index.html | 299 ++ tools/mc/mcltlrs/index.html | 255 + tools/mc/mcrl2/index.html | 299 ++ tools/mc/mercury/index.html | 334 ++ tools/mc/munta/index.html | 287 ++ tools/mc/nusmv/index.html | 297 ++ tools/mc/nuxmv/index.html | 309 ++ tools/mc/pnmc/index.html | 267 + tools/mc/pypl/index.html | 331 ++ tools/mc/romeo/index.html | 297 ++ tools/mc/rumur/index.html | 297 ++ tools/mc/sally/index.html | 2 +- tools/mc/smpt/index.html | 297 ++ tools/mc/spaceex/index.html | 297 ++ tools/mc/spin/index.html | 299 ++ tools/mc/stateright/index.html | 299 ++ tools/mc/tapaal/index.html | 333 ++ tools/mc/timesolver/index.html | 257 + tools/mc/uppaal/index.html | 326 ++ tools/mod/index.html | 548 +++ tools/mod/index.xml | 33 + tools/mod/jani/index.html | 367 ++ tools/mod/momba/index.html | 316 ++ tools/mod/tlaplus/index.html | 331 ++ tools/prob/caesar/index.html | 376 ++ tools/prob/index.html | 122 + tools/prob/index.xml | 7 + tools/sat-smt/index.html | 131 + tools/sat-smt/index.xml | 9 +- tools/sat-smt/lean/index.html | 316 ++ tools/sat-smt/mathsat/index.html | 4 +- 189 files changed, 31636 insertions(+), 197 deletions(-) create mode 100644 .gitea/index.html create mode 100644 .gitea/index.xml create mode 100644 .gitea/issue_template/add_tool/index.html create mode 100644 .gitea/issue_template/fix_tool/index.html create mode 100644 applications/hybrid-systems/index.html create mode 100644 applications/hybrid-systems/index.xml create mode 100644 applications/model-generator/index.html create mode 100644 applications/model-generator/index.xml create mode 100644 applications/modeling-framework/index.html create mode 100644 applications/modeling-framework/index.xml create mode 100644 applications/modeling-language/index.html create mode 100644 applications/modeling-language/index.xml create mode 100644 applications/parameter-synthesizer/index.html create mode 100644 applications/parameter-synthesizer/index.xml create mode 100644 applications/probabilistic-program-prover/index.html create mode 100644 applications/probabilistic-program-prover/index.xml create mode 100644 developers/-leslie-lamport/index.html create mode 100644 developers/-leslie-lamport/index.xml create mode 100644 developers/aalborg-university/index.html create mode 100644 developers/aalborg-university/index.xml create mode 100644 developers/bell-labs/index.html create mode 100644 developers/bell-labs/index.xml create mode 100644 developers/federal-university-of-amazonas/index.html create mode 100644 developers/federal-university-of-amazonas/index.xml create mode 100644 developers/inria-rocquencourt/index.html create mode 100644 developers/inria-rocquencourt/index.xml create mode 100644 developers/iscas/index.html create mode 100644 developers/iscas/index.xml create mode 100644 developers/jonathan-nadal/index.html create mode 100644 developers/jonathan-nadal/index.xml create mode 100644 developers/laas-cnrs/index.html create mode 100644 developers/laas-cnrs/index.xml create mode 100644 developers/lean-fro/index.html create mode 100644 developers/lean-fro/index.xml create mode 100644 developers/ludwig-maximilians-universität-münchen/index.html create mode 100644 developers/ludwig-maximilians-universität-münchen/index.xml create mode 100644 developers/matthew-fernandez/index.html create mode 100644 developers/matthew-fernandez/index.xml create mode 100644 developers/saarland-university/index.html create mode 100644 developers/saarland-university/index.xml create mode 100644 developers/universidad-nacional-de-cordoba/index.html create mode 100644 developers/universidad-nacional-de-cordoba/index.xml create mode 100644 developers/universite-sorbonne-paris-nord/index.html create mode 100644 developers/universite-sorbonne-paris-nord/index.xml create mode 100644 developers/university-of-bristol/index.html create mode 100644 developers/university-of-bristol/index.xml create mode 100644 developers/university-of-manchester/index.html create mode 100644 developers/university-of-manchester/index.xml create mode 100644 developers/university-of-nantes/index.html create mode 100644 developers/university-of-nantes/index.xml create mode 100644 developers/university-of-southampton/index.html create mode 100644 developers/university-of-southampton/index.xml create mode 100644 developers/university-of-stellenbosch/index.html create mode 100644 developers/university-of-stellenbosch/index.xml create mode 100644 developers/university-of-twente/index.html create mode 100644 developers/university-of-twente/index.xml create mode 100644 developers/uppsala-universitet/index.html create mode 100644 developers/uppsala-universitet/index.xml create mode 100644 developers/uppsala-university/index.html create mode 100644 developers/uppsala-university/index.xml create mode 100644 developers/verimag/index.html create mode 100644 developers/verimag/index.xml create mode 100644 developers/vertics/index.html create mode 100644 developers/vertics/index.xml create mode 100644 inputs/heyvl/index.html create mode 100644 inputs/heyvl/index.xml create mode 100644 interfaces/vscode/index.html create mode 100644 interfaces/vscode/index.xml create mode 100644 licenses/agpl-v3/index.html create mode 100644 licenses/agpl-v3/index.xml create mode 100644 licenses/bsd-3-clause/index.html create mode 100644 licenses/bsd-3-clause/index.xml create mode 100644 licenses/bsd-4-clause/index.html create mode 100644 licenses/bsd-4-clause/index.xml create mode 100644 licenses/bsl/index.html create mode 100644 licenses/bsl/index.xml create mode 100644 licenses/gpl/index.html create mode 100644 licenses/gpl/index.xml create mode 100644 licenses/isc/index.html create mode 100644 licenses/isc/index.xml create mode 100644 licenses/lgpl/index.html create mode 100644 licenses/lgpl/index.xml create mode 100644 licenses/open-source-3.0/index.html create mode 100644 licenses/open-source-3.0/index.xml create mode 100644 licenses/unilicense/index.html create mode 100644 licenses/unilicense/index.xml create mode 100644 techniques/car/index.html create mode 100644 techniques/car/index.xml create mode 100644 techniques/pdr/index.html create mode 100644 techniques/pdr/index.xml create mode 100644 tools/mc/blast/index.html create mode 100644 tools/mc/cadp/index.html create mode 100644 tools/mc/cgaal/index.html create mode 100644 tools/mc/concuerror/index.html create mode 100644 tools/mc/cpachecker/index.html create mode 100644 tools/mc/dscheck/index.html create mode 100644 tools/mc/eldarica/index.html create mode 100644 tools/mc/esbmc/index.html create mode 100644 tools/mc/geyser/index.html create mode 100644 tools/mc/imitator/index.html create mode 100644 tools/mc/imspin/index.html create mode 100644 tools/mc/intrepyd/index.html create mode 100644 tools/mc/kind2/index.html create mode 100644 tools/mc/ltsa/index.html create mode 100644 tools/mc/ltsmin/index.html create mode 100644 tools/mc/mcltlrs/index.html create mode 100644 tools/mc/mcrl2/index.html create mode 100644 tools/mc/mercury/index.html create mode 100644 tools/mc/munta/index.html create mode 100644 tools/mc/nusmv/index.html create mode 100644 tools/mc/nuxmv/index.html create mode 100644 tools/mc/pnmc/index.html create mode 100644 tools/mc/pypl/index.html create mode 100644 tools/mc/romeo/index.html create mode 100644 tools/mc/rumur/index.html create mode 100644 tools/mc/smpt/index.html create mode 100644 tools/mc/spaceex/index.html create mode 100644 tools/mc/spin/index.html create mode 100644 tools/mc/stateright/index.html create mode 100644 tools/mc/tapaal/index.html create mode 100644 tools/mc/timesolver/index.html create mode 100644 tools/mc/uppaal/index.html create mode 100644 tools/mod/index.html create mode 100644 tools/mod/index.xml create mode 100644 tools/mod/jani/index.html create mode 100644 tools/mod/momba/index.html create mode 100644 tools/mod/tlaplus/index.html create mode 100644 tools/prob/caesar/index.html create mode 100644 tools/sat-smt/lean/index.html diff --git a/.gitea/index.html b/.gitea/index.html new file mode 100644 index 0000000..efb0d66 --- /dev/null +++ b/.gitea/index.html @@ -0,0 +1,110 @@ + + + + + + + + +.Gitea | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

.Gitea

+ +
+ +
+

[ADD]

+

Fill in as little or as much information as you like, but more information increases my ability to …

+
+ +
+

[FIX]

+

Fill in as little or as much information as you like, but more information increases my ability to …

+
+ +
+ +
+ + + diff --git a/.gitea/index.xml b/.gitea/index.xml new file mode 100644 index 0000000..388ee18 --- /dev/null +++ b/.gitea/index.xml @@ -0,0 +1,25 @@ + + + + .Gitea on Formal Methods Tools + http://localhost:1313/.gitea/ + Recent content in .Gitea on Formal Methods Tools + Hugo + en-us + + + [ADD] + http://localhost:1313/.gitea/issue_template/add_tool/ + Mon, 01 Jan 0001 00:00:00 +0000 + http://localhost:1313/.gitea/issue_template/add_tool/ + <p>Fill in as little or as much information as you like, but more information increases my ability to add your tool effectively.</p> <p>Tool Name:</p> <p>Actively maintained? yes/no</p> <p>Tool Links: (add as many as you need) - <a href="" >Homepage</a> - <a href="" >Source Code</a> - <a href="" >Online Playground</a></p> <p>Applications: (think SMT Solver, Theorem Prover, Probabilistic Model Checker, etc.) -</p> <p>Developers: (institutions or individuals) -</p> <p>Licenses: -</p> <p>Input Formats: (think SMTLIB2, DIMACS, etc.) -</p> <p>Interfaces: (think CLI, GUI, Online, Python Bindings, etc.) -</p> + + + [FIX] + http://localhost:1313/.gitea/issue_template/fix_tool/ + Mon, 01 Jan 0001 00:00:00 +0000 + http://localhost:1313/.gitea/issue_template/fix_tool/ + <p>Fill in as little or as much information as you like, but more information increases my ability to add your tool effectively.</p> <p>Tool Name:</p> <p>Actively maintained? yes/no</p> <p>Tool Links: (add as many as you need) - <a href="" >Homepage</a> - <a href="" >Source Code</a> - <a href="" >Online Playground</a></p> <p>Applications: (think SMT Solver, Theorem Prover, Probabilistic Model Checker, etc.) -</p> <p>Developers: (institutions or individuals) -</p> <p>Licenses: -</p> <p>Input Formats: (think SMTLIB2, DIMACS, etc.) -</p> <p>Interfaces: (think CLI, GUI, Online, Python Bindings, etc.) -</p> + + + diff --git a/.gitea/issue_template/add_tool/index.html b/.gitea/issue_template/add_tool/index.html new file mode 100644 index 0000000..0c35de0 --- /dev/null +++ b/.gitea/issue_template/add_tool/index.html @@ -0,0 +1,138 @@ + + + + + + + + +[ADD] | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ + + + +
+

Fill in as little or as much information as you like, but more information increases my ability to add your tool effectively.

+

Tool Name:

+

Actively maintained? yes/no

+

Tool Links: (add as many as you need) +- Homepage +- Source Code +- Online Playground

+

Applications: (think SMT Solver, Theorem Prover, Probabilistic Model Checker, etc.) +-

+

Developers: (institutions or individuals) +-

+

Licenses: +-

+

Input Formats: (think SMTLIB2, DIMACS, etc.) +-

+

Interfaces: (think CLI, GUI, Online, Python Bindings, etc.) +-

+

Publications: (a DOI or URL is sufficient) +-

+

Additional Details or Description:

+ +
+ +
+ + +
+ + +
+ + + diff --git a/.gitea/issue_template/fix_tool/index.html b/.gitea/issue_template/fix_tool/index.html new file mode 100644 index 0000000..0ba4184 --- /dev/null +++ b/.gitea/issue_template/fix_tool/index.html @@ -0,0 +1,138 @@ + + + + + + + + +[FIX] | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ + + + +
+

Fill in as little or as much information as you like, but more information increases my ability to add your tool effectively.

+

Tool Name:

+

Actively maintained? yes/no

+

Tool Links: (add as many as you need) +- Homepage +- Source Code +- Online Playground

+

Applications: (think SMT Solver, Theorem Prover, Probabilistic Model Checker, etc.) +-

+

Developers: (institutions or individuals) +-

+

Licenses: +-

+

Input Formats: (think SMTLIB2, DIMACS, etc.) +-

+

Interfaces: (think CLI, GUI, Online, Python Bindings, etc.) +-

+

Publications: (a DOI or URL is sufficient) +-

+

Additional Details or Description:

+ +
+ +
+ + +
+ + +
+ + + diff --git a/about/index.html b/about/index.html index e935be7..322f71f 100644 --- a/about/index.html +++ b/about/index.html @@ -92,7 +92,7 @@
-

The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. Our goal is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.

+

The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. The goal of this website is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.

Key Objectives

diff --git a/developers/index.xml b/developers/index.xml index a3cc10a..dca84e2 100644 --- a/developers/index.xml +++ b/developers/index.xml @@ -8,6 +8,20 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + Leslie Lamport + https://fmtools.fyi/developers/-leslie-lamport/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/-leslie-lamport/ + + + + Aalborg University + https://fmtools.fyi/developers/aalborg-university/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/aalborg-university/ + + Albert-Ludwigs-Universität https://fmtools.fyi/developers/albert-ludwigs-universit%C3%A4t/ @@ -15,6 +29,13 @@ https://fmtools.fyi/developers/albert-ludwigs-universit%C3%A4t/ + + Bell Labs + https://fmtools.fyi/developers/bell-labs/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/bell-labs/ + + CEA https://fmtools.fyi/developers/cea/ @@ -43,6 +64,13 @@ https://fmtools.fyi/developers/eindhoven-university-of-technology/ + + Federal University of Amazonas + https://fmtools.fyi/developers/federal-university-of-amazonas/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/federal-university-of-amazonas/ + + Fondazione Bruno Kessler https://fmtools.fyi/developers/fondazione-bruno-kessler/ @@ -64,6 +92,20 @@ https://fmtools.fyi/developers/inria-rh%C3%B4ne-alpes/ + + INRIA Rocquencourt + https://fmtools.fyi/developers/inria-rocquencourt/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/inria-rocquencourt/ + + + + ISCAS + https://fmtools.fyi/developers/iscas/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/iscas/ + + Johannes Kepler Universität Linz https://fmtools.fyi/developers/johannes-kepler-universit%C3%A4t-linz/ @@ -71,6 +113,20 @@ https://fmtools.fyi/developers/johannes-kepler-universit%C3%A4t-linz/ + + Jonathan Nadal + https://fmtools.fyi/developers/jonathan-nadal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/jonathan-nadal/ + + + + LAAS-CNRS + https://fmtools.fyi/developers/laas-cnrs/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/laas-cnrs/ + + Laurent Simon https://fmtools.fyi/developers/laurent-simon/ @@ -78,6 +134,13 @@ https://fmtools.fyi/developers/laurent-simon/ + + Lean FRO + https://fmtools.fyi/developers/lean-fro/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/lean-fro/ + + LORIA https://fmtools.fyi/developers/loria/ @@ -85,6 +148,13 @@ https://fmtools.fyi/developers/loria/ + + Ludwig-Maximilians-Universität München + https://fmtools.fyi/developers/ludwig-maximilians-universit%C3%A4t-m%C3%BCnchen/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/ludwig-maximilians-universit%C3%A4t-m%C3%BCnchen/ + + Masaryk University https://fmtools.fyi/developers/masaryk-university/ @@ -92,6 +162,13 @@ https://fmtools.fyi/developers/masaryk-university/ + + Matthew Fernandez + https://fmtools.fyi/developers/matthew-fernandez/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/matthew-fernandez/ + + Microsoft Research https://fmtools.fyi/developers/microsoft-research/ @@ -141,6 +218,13 @@ https://fmtools.fyi/developers/rwth-aachen/ + + Saarland University + https://fmtools.fyi/developers/saarland-university/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/saarland-university/ + + SRI International https://fmtools.fyi/developers/sri-international/ @@ -169,6 +253,27 @@ https://fmtools.fyi/developers/uliege/ + + Universidad Nacional De Cordoba + https://fmtools.fyi/developers/universidad-nacional-de-cordoba/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/universidad-nacional-de-cordoba/ + + + + Universite Sorbonne Paris Nord + https://fmtools.fyi/developers/universite-sorbonne-paris-nord/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/universite-sorbonne-paris-nord/ + + + + University of Bristol + https://fmtools.fyi/developers/university-of-bristol/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/university-of-bristol/ + + University of Freiburg https://fmtools.fyi/developers/university-of-freiburg/ @@ -197,6 +302,41 @@ https://fmtools.fyi/developers/university-of-lugano/ + + University of Manchester + https://fmtools.fyi/developers/university-of-manchester/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/university-of-manchester/ + + + + University of Nantes + https://fmtools.fyi/developers/university-of-nantes/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/university-of-nantes/ + + + + University of Southampton + https://fmtools.fyi/developers/university-of-southampton/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/university-of-southampton/ + + + + University of Stellenbosch + https://fmtools.fyi/developers/university-of-stellenbosch/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/university-of-stellenbosch/ + + + + University of Twente + https://fmtools.fyi/developers/university-of-twente/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/university-of-twente/ + + University of Virginia https://fmtools.fyi/developers/university-of-virginia/ @@ -204,6 +344,20 @@ https://fmtools.fyi/developers/university-of-virginia/ + + Uppsala Universitet + https://fmtools.fyi/developers/uppsala-universitet/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/uppsala-universitet/ + + + + Uppsala University + https://fmtools.fyi/developers/uppsala-university/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/uppsala-university/ + + Utah State University https://fmtools.fyi/developers/utah-state-university/ @@ -211,5 +365,19 @@ https://fmtools.fyi/developers/utah-state-university/ + + Verimag + https://fmtools.fyi/developers/verimag/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/verimag/ + + + + Vertics + https://fmtools.fyi/developers/vertics/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/developers/vertics/ + + diff --git a/developers/inria-rocquencourt/index.html b/developers/inria-rocquencourt/index.html new file mode 100644 index 0000000..2682742 --- /dev/null +++ b/developers/inria-rocquencourt/index.html @@ -0,0 +1,130 @@ + + + + + + + + +INRIA Rocquencourt | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + INRIA Rocquencourt + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
CADP [ Closed-Source Tool ]  CADP (“Construction and Analysis of Distributed …
+ +
+ + + diff --git a/developers/inria-rocquencourt/index.xml b/developers/inria-rocquencourt/index.xml new file mode 100644 index 0000000..8785f2d --- /dev/null +++ b/developers/inria-rocquencourt/index.xml @@ -0,0 +1,19 @@ + + + + INRIA Rocquencourt on Formal Methods Tools + https://fmtools.fyi/developers/inria-rocquencourt/ + Recent content in INRIA Rocquencourt on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + CADP + https://fmtools.fyi/tools/mc/cadp/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cadp/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CADP (&ldquo;Construction and Analysis of Distributed Processes&rdquo;, formerly known as &ldquo;CAESAR/ALDEBARAN Development Package&rdquo;) is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.</p> + + + diff --git a/developers/iscas/index.html b/developers/iscas/index.html new file mode 100644 index 0000000..0d8c205 --- /dev/null +++ b/developers/iscas/index.html @@ -0,0 +1,130 @@ + + + + + + + + +ISCAS | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + ISCAS + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
JANIThe JANI specification defines the jani-model model interchange format and the jani-interaction tool …
+ +
+ + + diff --git a/developers/iscas/index.xml b/developers/iscas/index.xml new file mode 100644 index 0000000..2cf8da2 --- /dev/null +++ b/developers/iscas/index.xml @@ -0,0 +1,19 @@ + + + + ISCAS on Formal Methods Tools + https://fmtools.fyi/developers/iscas/ + Recent content in ISCAS on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + JANI + https://fmtools.fyi/tools/mod/jani/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/jani/ + <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p> + + + diff --git a/developers/jonathan-nadal/index.html b/developers/jonathan-nadal/index.html new file mode 100644 index 0000000..a22f40e --- /dev/null +++ b/developers/jonathan-nadal/index.html @@ -0,0 +1,131 @@ + + + + + + + + +Jonathan Nadal | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Jonathan Nadal + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
staterightstateright is a Rust library for model checking systems, with an emphasis on distributed systems. +
+ +
+ + + diff --git a/developers/jonathan-nadal/index.xml b/developers/jonathan-nadal/index.xml new file mode 100644 index 0000000..6d4e73a --- /dev/null +++ b/developers/jonathan-nadal/index.xml @@ -0,0 +1,19 @@ + + + + Jonathan Nadal on Formal Methods Tools + https://fmtools.fyi/developers/jonathan-nadal/ + Recent content in Jonathan Nadal on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + stateright + https://fmtools.fyi/tools/mc/stateright/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/stateright/ + <p><code>stateright</code> is a Rust library for model checking systems, with an emphasis on distributed systems.</p> + + + diff --git a/developers/laas-cnrs/index.html b/developers/laas-cnrs/index.html new file mode 100644 index 0000000..cdb16a4 --- /dev/null +++ b/developers/laas-cnrs/index.html @@ -0,0 +1,138 @@ + + + + + + + + +LAAS-CNRS | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + LAAS-CNRS + +

+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ToolDescription
Mercury [ Not Maintained Since 2020 ] Mercury is a Model Checker developed for multicore, multiprocessors …
SM(P/)TSMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes …
+ +
+ + + diff --git a/developers/laas-cnrs/index.xml b/developers/laas-cnrs/index.xml new file mode 100644 index 0000000..afcc1fd --- /dev/null +++ b/developers/laas-cnrs/index.xml @@ -0,0 +1,26 @@ + + + + LAAS-CNRS on Formal Methods Tools + https://fmtools.fyi/developers/laas-cnrs/ + Recent content in LAAS-CNRS on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Mercury + https://fmtools.fyi/tools/mc/mercury/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mercury/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.</p> + + + SM(P/)T + https://fmtools.fyi/tools/mc/smpt/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/smpt/ + <p>SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).</p> + + + diff --git a/developers/lean-fro/index.html b/developers/lean-fro/index.html new file mode 100644 index 0000000..740a074 --- /dev/null +++ b/developers/lean-fro/index.html @@ -0,0 +1,131 @@ + + + + + + + + +Lean FRO | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Lean FRO + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
LEANcvc5 is an automatic theorem prover for SMT problems. +
+ +
+ + + diff --git a/developers/lean-fro/index.xml b/developers/lean-fro/index.xml new file mode 100644 index 0000000..4ca6c70 --- /dev/null +++ b/developers/lean-fro/index.xml @@ -0,0 +1,19 @@ + + + + Lean FRO on Formal Methods Tools + https://fmtools.fyi/developers/lean-fro/ + Recent content in Lean FRO on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + LEAN + https://fmtools.fyi/tools/sat-smt/lean/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/sat-smt/lean/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + + + diff --git a/developers/ludwig-maximilians-universität-münchen/index.html b/developers/ludwig-maximilians-universität-münchen/index.html new file mode 100644 index 0000000..d49d53f --- /dev/null +++ b/developers/ludwig-maximilians-universität-münchen/index.html @@ -0,0 +1,131 @@ + + + + + + + + +Ludwig-Maximilians-Universität München | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Ludwig-Maximilians-Universität München + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
CPAchecker [ Closed-Source Tool ]  CPAchecker is a tool for configurable software verification. +
+ +
+ + + diff --git a/developers/ludwig-maximilians-universität-münchen/index.xml b/developers/ludwig-maximilians-universität-münchen/index.xml new file mode 100644 index 0000000..b27e762 --- /dev/null +++ b/developers/ludwig-maximilians-universität-münchen/index.xml @@ -0,0 +1,19 @@ + + + + Ludwig-Maximilians-Universität München on Formal Methods Tools + https://fmtools.fyi/developers/ludwig-maximilians-universit%C3%A4t-m%C3%BCnchen/ + Recent content in Ludwig-Maximilians-Universität München on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + CPAchecker + https://fmtools.fyi/tools/mc/cpachecker/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cpachecker/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CPAchecker is a tool for configurable software verification.</p> + + + diff --git a/developers/matthew-fernandez/index.html b/developers/matthew-fernandez/index.html new file mode 100644 index 0000000..8b074f6 --- /dev/null +++ b/developers/matthew-fernandez/index.html @@ -0,0 +1,140 @@ + + + + + + + + +Matthew Fernandez | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Matthew Fernandez + +

+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ToolDescription
pyPLpyPL is a naive model generator, model checker and theorem prover. +
RumurRumur is a model checker. +
+ +
+ + + diff --git a/developers/matthew-fernandez/index.xml b/developers/matthew-fernandez/index.xml new file mode 100644 index 0000000..e95f450 --- /dev/null +++ b/developers/matthew-fernandez/index.xml @@ -0,0 +1,26 @@ + + + + Matthew Fernandez on Formal Methods Tools + https://fmtools.fyi/developers/matthew-fernandez/ + Recent content in Matthew Fernandez on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + pyPL + https://fmtools.fyi/tools/mc/pypl/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/pypl/ + <p>pyPL is a naive model generator, model checker and theorem prover.</p> + + + Rumur + https://fmtools.fyi/tools/mc/rumur/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/rumur/ + <p>Rumur is a model checker.</p> + + + diff --git a/developers/rwth-aachen/index.html b/developers/rwth-aachen/index.html index 55433cc..f1d1d85 100644 --- a/developers/rwth-aachen/index.html +++ b/developers/rwth-aachen/index.html @@ -107,12 +107,29 @@ + + Caesar + Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + + + + + + COMICS COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for … + + + + JANI + The JANI specification defines the jani-model model interchange format and the jani-interaction tool … + + + diff --git a/developers/rwth-aachen/index.xml b/developers/rwth-aachen/index.xml index d65129f..152c366 100644 --- a/developers/rwth-aachen/index.xml +++ b/developers/rwth-aachen/index.xml @@ -8,6 +8,13 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + Caesar + https://fmtools.fyi/tools/prob/caesar/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/prob/caesar/ + <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> + COMICS https://fmtools.fyi/tools/prob/comics/ @@ -15,6 +22,13 @@ https://fmtools.fyi/tools/prob/comics/ <p>COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).</p> + + JANI + https://fmtools.fyi/tools/mod/jani/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/jani/ + <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p> + SMT-RAT https://fmtools.fyi/tools/sat-smt/smt-rat/ diff --git a/developers/saarland-university/index.html b/developers/saarland-university/index.html new file mode 100644 index 0000000..4d17149 --- /dev/null +++ b/developers/saarland-university/index.html @@ -0,0 +1,130 @@ + + + + + + + + +Saarland University | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Saarland University + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
MombaMomba is a Python framework for dealing with quantitative models centered around the JANI-model …
+ +
+ + + diff --git a/developers/saarland-university/index.xml b/developers/saarland-university/index.xml new file mode 100644 index 0000000..df89f89 --- /dev/null +++ b/developers/saarland-university/index.xml @@ -0,0 +1,19 @@ + + + + Saarland University on Formal Methods Tools + https://fmtools.fyi/developers/saarland-university/ + Recent content in Saarland University on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Momba + https://fmtools.fyi/tools/mod/momba/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/momba/ + <p>Momba is a Python framework for dealing with quantitative models centered around the <a href="../jani" >JANI-model</a> interchange format.</p> + + + diff --git a/developers/universidad-nacional-de-cordoba/index.html b/developers/universidad-nacional-de-cordoba/index.html new file mode 100644 index 0000000..53d8352 --- /dev/null +++ b/developers/universidad-nacional-de-cordoba/index.html @@ -0,0 +1,130 @@ + + + + + + + + +Universidad Nacional De Cordoba | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Universidad Nacional De Cordoba + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
JANIThe JANI specification defines the jani-model model interchange format and the jani-interaction tool …
+ +
+ + + diff --git a/developers/universidad-nacional-de-cordoba/index.xml b/developers/universidad-nacional-de-cordoba/index.xml new file mode 100644 index 0000000..86dd68d --- /dev/null +++ b/developers/universidad-nacional-de-cordoba/index.xml @@ -0,0 +1,19 @@ + + + + Universidad Nacional De Cordoba on Formal Methods Tools + https://fmtools.fyi/developers/universidad-nacional-de-cordoba/ + Recent content in Universidad Nacional De Cordoba on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + JANI + https://fmtools.fyi/tools/mod/jani/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/jani/ + <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p> + + + diff --git a/developers/universite-sorbonne-paris-nord/index.html b/developers/universite-sorbonne-paris-nord/index.html new file mode 100644 index 0000000..e229950 --- /dev/null +++ b/developers/universite-sorbonne-paris-nord/index.html @@ -0,0 +1,130 @@ + + + + + + + + +Universite Sorbonne Paris Nord | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Universite Sorbonne Paris Nord + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
IMITATORIMITATOR is a parametric timed model checker taking as input extensions of parametric timed …
+ +
+ + + diff --git a/developers/universite-sorbonne-paris-nord/index.xml b/developers/universite-sorbonne-paris-nord/index.xml new file mode 100644 index 0000000..b70e6fa --- /dev/null +++ b/developers/universite-sorbonne-paris-nord/index.xml @@ -0,0 +1,19 @@ + + + + Universite Sorbonne Paris Nord on Formal Methods Tools + https://fmtools.fyi/developers/universite-sorbonne-paris-nord/ + Recent content in Universite Sorbonne Paris Nord on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + IMITATOR + https://fmtools.fyi/tools/mc/imitator/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/imitator/ + <p>IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.</p> + + + diff --git a/developers/university-of-bristol/index.html b/developers/university-of-bristol/index.html new file mode 100644 index 0000000..33712a4 --- /dev/null +++ b/developers/university-of-bristol/index.html @@ -0,0 +1,130 @@ + + + + + + + + +University of Bristol | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + University of Bristol + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
ESBMCESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying …
+ +
+ + + diff --git a/developers/university-of-bristol/index.xml b/developers/university-of-bristol/index.xml new file mode 100644 index 0000000..cc3be9b --- /dev/null +++ b/developers/university-of-bristol/index.xml @@ -0,0 +1,19 @@ + + + + University of Bristol on Formal Methods Tools + https://fmtools.fyi/developers/university-of-bristol/ + Recent content in University of Bristol on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + diff --git a/developers/university-of-iowa/index.html b/developers/university-of-iowa/index.html index e7fa865..3c72a12 100644 --- a/developers/university-of-iowa/index.html +++ b/developers/university-of-iowa/index.html @@ -122,6 +122,15 @@ + + + + Kind 2 + Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems. + + + + diff --git a/developers/university-of-iowa/index.xml b/developers/university-of-iowa/index.xml index f78e1b5..a4a5cea 100644 --- a/developers/university-of-iowa/index.xml +++ b/developers/university-of-iowa/index.xml @@ -22,5 +22,12 @@ https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p>
+ + Kind 2 + https://fmtools.fyi/tools/mc/kind2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/kind2/ + <p>Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.</p> + diff --git a/developers/university-of-manchester/index.html b/developers/university-of-manchester/index.html new file mode 100644 index 0000000..47a3fde --- /dev/null +++ b/developers/university-of-manchester/index.html @@ -0,0 +1,130 @@ + + + + + + + + +University of Manchester | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + University of Manchester + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
ESBMCESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying …
+ +
+ + + diff --git a/developers/university-of-manchester/index.xml b/developers/university-of-manchester/index.xml new file mode 100644 index 0000000..96fa9d0 --- /dev/null +++ b/developers/university-of-manchester/index.xml @@ -0,0 +1,19 @@ + + + + University of Manchester on Formal Methods Tools + https://fmtools.fyi/developers/university-of-manchester/ + Recent content in University of Manchester on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + diff --git a/developers/university-of-nantes/index.html b/developers/university-of-nantes/index.html new file mode 100644 index 0000000..16e6fa1 --- /dev/null +++ b/developers/university-of-nantes/index.html @@ -0,0 +1,131 @@ + + + + + + + + +University of Nantes | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + University of Nantes + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
RoméoRomeo allows the modelling of complex systems using extensions of time Petri nets. +
+ +
+ + + diff --git a/developers/university-of-nantes/index.xml b/developers/university-of-nantes/index.xml new file mode 100644 index 0000000..cc5778e --- /dev/null +++ b/developers/university-of-nantes/index.xml @@ -0,0 +1,19 @@ + + + + University of Nantes on Formal Methods Tools + https://fmtools.fyi/developers/university-of-nantes/ + Recent content in University of Nantes on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Roméo + https://fmtools.fyi/tools/mc/romeo/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/romeo/ + <p>Romeo allows the modelling of complex systems using extensions of time Petri nets.</p> + + + diff --git a/developers/university-of-southampton/index.html b/developers/university-of-southampton/index.html new file mode 100644 index 0000000..f01c285 --- /dev/null +++ b/developers/university-of-southampton/index.html @@ -0,0 +1,130 @@ + + + + + + + + +University of Southampton | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + University of Southampton + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
ESBMCESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying …
+ +
+ + + diff --git a/developers/university-of-southampton/index.xml b/developers/university-of-southampton/index.xml new file mode 100644 index 0000000..222f54d --- /dev/null +++ b/developers/university-of-southampton/index.xml @@ -0,0 +1,19 @@ + + + + University of Southampton on Formal Methods Tools + https://fmtools.fyi/developers/university-of-southampton/ + Recent content in University of Southampton on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + diff --git a/developers/university-of-stellenbosch/index.html b/developers/university-of-stellenbosch/index.html new file mode 100644 index 0000000..422d514 --- /dev/null +++ b/developers/university-of-stellenbosch/index.html @@ -0,0 +1,130 @@ + + + + + + + + +University of Stellenbosch | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + University of Stellenbosch + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
ESBMCESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying …
+ +
+ + + diff --git a/developers/university-of-stellenbosch/index.xml b/developers/university-of-stellenbosch/index.xml new file mode 100644 index 0000000..379d1a5 --- /dev/null +++ b/developers/university-of-stellenbosch/index.xml @@ -0,0 +1,19 @@ + + + + University of Stellenbosch on Formal Methods Tools + https://fmtools.fyi/developers/university-of-stellenbosch/ + Recent content in University of Stellenbosch on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + diff --git a/developers/university-of-twente/index.html b/developers/university-of-twente/index.html new file mode 100644 index 0000000..4775b9e --- /dev/null +++ b/developers/university-of-twente/index.html @@ -0,0 +1,147 @@ + + + + + + + + +University of Twente | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + University of Twente + +

+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ToolDescription
DSCheckDSCheck is an experimental model checker for testing concurrent OCaml programs. +
JANIThe JANI specification defines the jani-model model interchange format and the jani-interaction tool …
LTSminLTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the …
+ +
+ + + diff --git a/developers/university-of-twente/index.xml b/developers/university-of-twente/index.xml new file mode 100644 index 0000000..daa195f --- /dev/null +++ b/developers/university-of-twente/index.xml @@ -0,0 +1,33 @@ + + + + University of Twente on Formal Methods Tools + https://fmtools.fyi/developers/university-of-twente/ + Recent content in University of Twente on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + DSCheck + https://fmtools.fyi/tools/mc/dscheck/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/dscheck/ + <p>DSCheck is an experimental model checker for testing concurrent OCaml programs.</p> + + + JANI + https://fmtools.fyi/tools/mod/jani/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/jani/ + <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p> + + + LTSmin + https://fmtools.fyi/tools/mc/ltsmin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/ltsmin/ + <p>LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.</p> + + + diff --git a/developers/uppsala-universitet/index.html b/developers/uppsala-universitet/index.html new file mode 100644 index 0000000..900ccdf --- /dev/null +++ b/developers/uppsala-universitet/index.html @@ -0,0 +1,138 @@ + + + + + + + + +Uppsala Universitet | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Uppsala Universitet + +

+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ToolDescription
BLAST [ Not Maintained Since 2012 ] BLAST (Berkeley Lazy Abstraction Software verification Tool) is a …
Uppaal [ Closed-Source Tool ]  Uppaal is an integrated tool environment for modeling, validation and …
+ +
+ + + diff --git a/developers/uppsala-universitet/index.xml b/developers/uppsala-universitet/index.xml new file mode 100644 index 0000000..9ce0652 --- /dev/null +++ b/developers/uppsala-universitet/index.xml @@ -0,0 +1,26 @@ + + + + Uppsala Universitet on Formal Methods Tools + https://fmtools.fyi/developers/uppsala-universitet/ + Recent content in Uppsala Universitet on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + BLAST + https://fmtools.fyi/tools/mc/blast/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/blast/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2012</span> <span style="display:none">]</span> </div> BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.</p> + + + Uppaal + https://fmtools.fyi/tools/mc/uppaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/uppaal/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).</p> + + + diff --git a/developers/uppsala-university/index.html b/developers/uppsala-university/index.html new file mode 100644 index 0000000..a0f4842 --- /dev/null +++ b/developers/uppsala-university/index.html @@ -0,0 +1,140 @@ + + + + + + + + +Uppsala University | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Uppsala University + +

+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ToolDescription
ConcuerrorConcuerror is a stateless model checking tool for Erlang programs. +
EldaricaEldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs. +
+ +
+ + + diff --git a/developers/uppsala-university/index.xml b/developers/uppsala-university/index.xml new file mode 100644 index 0000000..7b953df --- /dev/null +++ b/developers/uppsala-university/index.xml @@ -0,0 +1,26 @@ + + + + Uppsala University on Formal Methods Tools + https://fmtools.fyi/developers/uppsala-university/ + Recent content in Uppsala University on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Concuerror + https://fmtools.fyi/tools/mc/concuerror/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/concuerror/ + <p>Concuerror is a stateless model checking tool for Erlang programs.</p> + + + Eldarica + https://fmtools.fyi/tools/mc/eldarica/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/eldarica/ + <p>Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.</p> + + + diff --git a/developers/verimag/index.html b/developers/verimag/index.html new file mode 100644 index 0000000..c7f1352 --- /dev/null +++ b/developers/verimag/index.html @@ -0,0 +1,130 @@ + + + + + + + + +Verimag | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Verimag + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
SpaceExThe SpaceEx tool platform is designed to facilitate the implementation of algorithms related to …
+ +
+ + + diff --git a/developers/verimag/index.xml b/developers/verimag/index.xml new file mode 100644 index 0000000..62a43f1 --- /dev/null +++ b/developers/verimag/index.xml @@ -0,0 +1,19 @@ + + + + Verimag on Formal Methods Tools + https://fmtools.fyi/developers/verimag/ + Recent content in Verimag on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + SpaceEx + https://fmtools.fyi/tools/mc/spaceex/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/spaceex/ + <p>The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.</p> + + + diff --git a/developers/vertics/index.html b/developers/vertics/index.html new file mode 100644 index 0000000..07b1978 --- /dev/null +++ b/developers/vertics/index.html @@ -0,0 +1,130 @@ + + + + + + + + +Vertics | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Vertics + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
Mercury [ Not Maintained Since 2020 ] Mercury is a Model Checker developed for multicore, multiprocessors …
+ +
+ + + diff --git a/developers/vertics/index.xml b/developers/vertics/index.xml new file mode 100644 index 0000000..184eef7 --- /dev/null +++ b/developers/vertics/index.xml @@ -0,0 +1,19 @@ + + + + Vertics on Formal Methods Tools + https://fmtools.fyi/developers/vertics/ + Recent content in Vertics on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Mercury + https://fmtools.fyi/tools/mc/mercury/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mercury/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.</p> + + + diff --git a/index.html b/index.html index 3809683..36db92d 100644 --- a/index.html +++ b/index.html @@ -122,171 +122,37 @@ Contribute

- PRISM + Colibri - Probabilistic Model Checker + SMT Solver

-

PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that …

- PRISM -
- -
-

- STAMINA - - Probabilistic Model Checker - -

-

A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces …

- STAMINA -
- -
-

- E - - Theorem Prover - -

-

E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with …

- E -
- -
-

- CaDiCaL - - SAT Solver - -

-

CaDiCaL is a simplified satisfiability solver. +

Colibri is an SMT solver.

- CaDiCaL + Colibri

- dReal + Sally - SMT Solver + Model Checker

-

[ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems …

- dReal -
- -
-

- SMTInterpol - - Interpolating SMT Solver - -

-

SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. -APIs and …

- SMTInterpol -
- -
-

- Alt-Ergo - - SMT Solver - -

-

Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools …

- Alt-Ergo -
- -
-

- cvc5 - - Theorem Prover - -

-

cvc5 is an automatic theorem prover for SMT problems. +

Sally is a model checker for infinite state systems described as transition systems.

- cvc5 + Sally

- Q3B + CADP - SMT Solver + Model Checker

-

[ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which …

- Q3B -
- -
-

- OpenSMT - - SMT Solver - -

-

OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making …

- OpenSMT -
- -
-

- COMICS - - DTMC Counterexample Generator - -

-

COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for …

- COMICS -
- -
-

- veriT - - SMT Solver - -

-

veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …

- veriT -
- -
-

- ParaFROST - - SMT Solver - -

-

ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA …

- ParaFROST -
- -
-

- MathSAT - - SMT Solver - -

-

[ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help …

- MathSAT -
- -
-

- Vampire - - Theorem Prover - -

-

Vampire is a theorem prover. -

- Vampire +

[ Closed-Source Tool ]  CADP (“Construction and Analysis of Distributed …

+ CADP
@@ -314,38 +180,170 @@ APIs and …

- Colibri - - SMT Solver - -

-

Colibri is an SMT solver. -

- Colibri -
- -
-

- Riss - - SAT Tool Collection - -

-

[ Not Maintained Since 2017 ] Riss is a SAT solving tool collection. -

- Riss -
- -
-

- Z3 + cvc4 Theorem Prover

-

Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. -APIs and Bindings This …

- Z3 +

[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded …

+ cvc4 +
+ +
+

+ LTSmin + + Model Checker + +

+

LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the …

+ LTSmin +
+ +
+

+ Intrepyd + + Model Checker + +

+

[ Not Maintained Since 2021 ] Intrepyd is a python module that provides a simulator and a model …

+ Intrepyd +
+ +
+

+ veriT + + SMT Solver + +

+

veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …

+ veriT +
+ +
+

+ DSCheck + + Model Checker + +

+

DSCheck is an experimental model checker for testing concurrent OCaml programs. +

+ DSCheck +
+ +
+

+ Geyser + + Model Checker + +

+

Geyser is a simple symbolic model checker for propositional transition system systems. +

+ Geyser +
+ +
+

+ STAMINA + + Probabilistic Model Checker + +

+

A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces …

+ STAMINA +
+ +
+

+ E + + Theorem Prover + +

+

E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with …

+ E +
+ +
+

+ Bitwuzla + + SMT Solver + +

+

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …

+ Bitwuzla +
+ +
+

+ SM(P/)T + + Satisfiability Modulo Petri Net + +

+

SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes …

+ SM(P/)T +
+ +
+

+ CPAchecker + + Model Checker + +

+

[ Closed-Source Tool ]  CPAchecker is a tool for configurable software verification. +

+ CPAchecker +
+ +
+

+ Q3B + + SMT Solver + +

+

[ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which …

+ Q3B +
+ +
+

+ JANI + + Quantitative Modeling Specification + +

+

The JANI specification defines the jani-model model interchange format and the jani-interaction tool …

+ JANI +
+ +
+

+ CGAAL + + Model Checker + +

+

CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game …

+ CGAAL +
+ +
+

+ BLAST + + Model Checker + +

+

[ Not Maintained Since 2012 ] BLAST (Berkeley Lazy Abstraction Software verification Tool) is a …

+ BLAST
@@ -363,7 +361,7 @@ APIs and Bindings This …

Made with ♥ using Hugo
- Built + Built diff --git a/index.xml b/index.xml index 4e2761b..d53cd99 100644 --- a/index.xml +++ b/index.xml @@ -13,7 +13,7 @@ https://fmtools.fyi/about/ Sat, 07 Jun 2025 00:00:00 +0000 https://fmtools.fyi/about/ - <p>The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. Our goal is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.</p> <h2 id="key-objectives">Key Objectives</h2> <ul> <li>Provide a comprehensive list of tools for formal methods.</li> <li>Group tools by rich metadata to support collaboration and boost tools&rsquo; strengths.</li> <li>Foster a collaborative community for tool development and support.</li> </ul> <h2 id="whos-behind-this">Who&rsquo;s Behind This?</h2> <p>Howdy. My name is Landon Taylor. I sometimes go by mossBiscuits. This is one of my hobby projects. I have a passion for formal methods. When I started learning about verification, there was a sharp barrier to entry due partially to the sprawl of content online. I wanted to solve this problem, so I have been chipping away at this website for a while now.</p> + <p>The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. The goal of this website is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.</p> <h2 id="key-objectives">Key Objectives</h2> <ul> <li>Provide a comprehensive list of tools for formal methods.</li> <li>Group tools by rich metadata to support collaboration and boost tools&rsquo; strengths.</li> <li>Foster a collaborative community for tool development and support.</li> </ul> <h2 id="whos-behind-this">Who&rsquo;s Behind This?</h2> <p>Howdy. My name is Landon Taylor. I sometimes go by mossBiscuits. This is one of my hobby projects. I have a passion for formal methods. When I started learning about verification, there was a sharp barrier to entry due partially to the sprawl of content online. I wanted to solve this problem, so I have been chipping away at this website for a while now.</p> Alt-Ergo @@ -29,6 +29,13 @@ https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations.</p> + + BLAST + https://fmtools.fyi/tools/mc/blast/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/blast/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2012</span> <span style="display:none">]</span> </div> BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.</p> + Boolector https://fmtools.fyi/tools/sat-smt/boolector/ @@ -43,6 +50,27 @@ https://fmtools.fyi/tools/sat-smt/cadical/ <p>CaDiCaL is a simplified satisfiability solver.</p> + + CADP + https://fmtools.fyi/tools/mc/cadp/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cadp/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CADP (&ldquo;Construction and Analysis of Distributed Processes&rdquo;, formerly known as &ldquo;CAESAR/ALDEBARAN Development Package&rdquo;) is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.</p> + + + Caesar + https://fmtools.fyi/tools/prob/caesar/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/prob/caesar/ + <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> + + + CGAAL + https://fmtools.fyi/tools/mc/cgaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cgaal/ + <p>CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).</p> + Colibri https://fmtools.fyi/tools/sat-smt/colibri/ @@ -57,6 +85,13 @@ https://fmtools.fyi/tools/prob/comics/ <p>COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).</p> + + Concuerror + https://fmtools.fyi/tools/mc/concuerror/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/concuerror/ + <p>Concuerror is a stateless model checking tool for Erlang programs.</p> + Contribute https://fmtools.fyi/contribute/ @@ -64,6 +99,13 @@ https://fmtools.fyi/contribute/ <p>Instructions coming soon. Please see <a href="https://gitmoss.fyi/fmtools/content/wiki/Contribute" target="_blank" >https://gitmoss.fyi/fmtools/content/wiki/Contribute</a> for temporary instructions.</p> <h2 id="quick-links">Quick Links</h2> <ul> <li>Request addding a tool: <a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2fadd_tool.md" target="_blank" >Submit Git Issue</a></li> <li>Request fixing a tool: <a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md" target="_blank" >Submit Git Issue</a></li> </ul> + + CPAchecker + https://fmtools.fyi/tools/mc/cpachecker/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cpachecker/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CPAchecker is a tool for configurable software verification.</p> + CryptoMiniSat https://fmtools.fyi/tools/sat-smt/cryptominisat/ @@ -92,6 +134,13 @@ https://fmtools.fyi/tools/sat-smt/dreal/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.</p> + + DSCheck + https://fmtools.fyi/tools/mc/dscheck/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/dscheck/ + <p>DSCheck is an experimental model checker for testing concurrent OCaml programs.</p> + E https://fmtools.fyi/tools/sat-smt/e/ @@ -99,6 +148,27 @@ https://fmtools.fyi/tools/sat-smt/e/ <p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.</p> + + Eldarica + https://fmtools.fyi/tools/mc/eldarica/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/eldarica/ + <p>Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.</p> + + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + Geyser + https://fmtools.fyi/tools/mc/geyser/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/geyser/ + <p>Geyser is a simple symbolic model checker for propositional transition system systems.</p> + Glucose https://fmtools.fyi/tools/sat-smt/glucose/ @@ -106,6 +176,48 @@ https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> + + IMITATOR + https://fmtools.fyi/tools/mc/imitator/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/imitator/ + <p>IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.</p> + + + ImSpin + https://fmtools.fyi/tools/mc/imspin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/imspin/ + <p>ImSpin is a frontend for the <a href="../spin" >SPIN</a> model checker, providing an environment for users engaged in model checking tasks.</p> + + + Intrepyd + https://fmtools.fyi/tools/mc/intrepyd/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/intrepyd/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> Intrepyd is a python module that provides a simulator and a model checker in form of a rich API, to allow the rapid prototyping of formal methods algorithms for the rigorous analysis of circuits, specifications, models.</p> + + + JANI + https://fmtools.fyi/tools/mod/jani/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/jani/ + <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p> + + + Kind 2 + https://fmtools.fyi/tools/mc/kind2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/kind2/ + <p>Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.</p> + + + LEAN + https://fmtools.fyi/tools/sat-smt/lean/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/sat-smt/lean/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + Lingeling https://fmtools.fyi/tools/sat-smt/lingeling/ @@ -113,12 +225,47 @@ https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> + + LTSA + https://fmtools.fyi/tools/mc/ltsa/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/ltsa/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2018</span> <span style="display:none">]</span> </div> LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour.</p> + + + LTSmin + https://fmtools.fyi/tools/mc/ltsmin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/ltsmin/ + <p>LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.</p> + MathSAT https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 https://fmtools.fyi/tools/sat-smt/mathsat/ - <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).</p> + + + mcltl-rs + https://fmtools.fyi/tools/mc/mcltlrs/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mcltlrs/ + <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> <p>mcltl-rs is an experimental model checker for LTL written in Rust.</p> + + + mCRL2 + https://fmtools.fyi/tools/mc/mcrl2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mcrl2/ + <p>mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.</p> + + + Mercury + https://fmtools.fyi/tools/mc/mercury/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mercury/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.</p> MiniSat @@ -134,6 +281,34 @@ https://fmtools.fyi/license/ <p>MIT License</p> <p>Copyright (c) 2025 Landon Taylor.</p> <p>Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the &ldquo;Software&rdquo;), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:</p> + + Momba + https://fmtools.fyi/tools/mod/momba/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/momba/ + <p>Momba is a Python framework for dealing with quantitative models centered around the <a href="../jani" >JANI-model</a> interchange format.</p> + + + MUNTA + https://fmtools.fyi/tools/mc/munta/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/munta/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata</p> + + + NuSMV + https://fmtools.fyi/tools/mc/nusmv/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/nusmv/ + <p>NuSMV is a symbolic model checker.</p> + + + NuXMV + https://fmtools.fyi/tools/mc/nuxmv/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/nuxmv/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.</p> + OpenSMT https://fmtools.fyi/tools/sat-smt/opensmt/ @@ -148,6 +323,13 @@ https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> + + Pnmc + https://fmtools.fyi/tools/mc/pnmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/pnmc/ + <p>Pnmc is a symbolic model checker for Petri nets.</p> + PRISM https://fmtools.fyi/tools/prob/prism/ @@ -162,6 +344,13 @@ https://fmtools.fyi/privacy/ <p>This website does not collect or track any personal data from visitors. No cookies, personalized analytics, or tracking scripts are used. No ads are shown on this website, and there is no money to be made from this project.</p> <p>If you choose to contribute content (including emails, issues, and pull requests), any information you voluntarily provide may be stored as part of the website&rsquo;s content and source code. Only the data you explicitly submit will be saved, and data is not sold by the website&rsquo;s owner. Due to the public nature of its disclosure, this information is not considered private and may be used by the general public as allowed by respective laws and policies. Your privacy is respected, and no unnecessary data is collected or shared.</p> + + pyPL + https://fmtools.fyi/tools/mc/pypl/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/pypl/ + <p>pyPL is a naive model generator, model checker and theorem prover.</p> + Q3B https://fmtools.fyi/tools/sat-smt/q3b/ @@ -176,6 +365,20 @@ https://fmtools.fyi/tools/sat-smt/riss/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span> <span style="display:none">]</span> </div> Riss is a SAT solving tool collection.</p> + + Roméo + https://fmtools.fyi/tools/mc/romeo/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/romeo/ + <p>Romeo allows the modelling of complex systems using extensions of time Petri nets.</p> + + + Rumur + https://fmtools.fyi/tools/mc/rumur/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/rumur/ + <p>Rumur is a model checker.</p> + Sally https://fmtools.fyi/tools/mc/sally/ @@ -183,6 +386,13 @@ https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> + + SM(P/)T + https://fmtools.fyi/tools/mc/smpt/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/smpt/ + <p>SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).</p> + SMT-RAT https://fmtools.fyi/tools/sat-smt/smt-rat/ @@ -197,6 +407,20 @@ https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> + + SpaceEx + https://fmtools.fyi/tools/mc/spaceex/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/spaceex/ + <p>The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.</p> + + + Spin + https://fmtools.fyi/tools/mc/spin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/spin/ + <p>Spin is a model checker for multi-threaded software.</p> + STAMINA https://fmtools.fyi/tools/prob/stamina/ @@ -204,6 +428,13 @@ https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> + + stateright + https://fmtools.fyi/tools/mc/stateright/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/stateright/ + <p><code>stateright</code> is a Rust library for model checking systems, with an emphasis on distributed systems.</p> + Storm https://fmtools.fyi/tools/prob/storm/ @@ -218,6 +449,34 @@ https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> + + TAPAAL + https://fmtools.fyi/tools/mc/tapaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/tapaal/ + <p>TAPAAL is a tool for verification of timed-arc petri nets</p> + + + TimeSolver + https://fmtools.fyi/tools/mc/timesolver/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/timesolver/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2019</span> <span style="display:none">]</span> </div> TimeSolver is a Model Checker for timed automata that uses pes (predicate equation systems).</p> + + + TLA+ + https://fmtools.fyi/tools/mod/tlaplus/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/tlaplus/ + <p>TLA+ is a high-level language for modeling programs and systems&ndash;especially concurrent and distributed ones.</p> + + + Uppaal + https://fmtools.fyi/tools/mc/uppaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/uppaal/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).</p> + Vampire https://fmtools.fyi/tools/sat-smt/vampire/ diff --git a/inputs/heyvl/index.html b/inputs/heyvl/index.html new file mode 100644 index 0000000..d2f86e4 --- /dev/null +++ b/inputs/heyvl/index.html @@ -0,0 +1,131 @@ + + + + + + + + +HeyVL | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + HeyVL + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
CaesarStorm is a tool for the analysis of systems involving random or probabilistic phenomena. +
+ +
+ + + diff --git a/inputs/heyvl/index.xml b/inputs/heyvl/index.xml new file mode 100644 index 0000000..975f112 --- /dev/null +++ b/inputs/heyvl/index.xml @@ -0,0 +1,19 @@ + + + + HeyVL on Formal Methods Tools + https://fmtools.fyi/inputs/heyvl/ + Recent content in HeyVL on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Caesar + https://fmtools.fyi/tools/prob/caesar/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/prob/caesar/ + <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> + + + diff --git a/inputs/index.html b/inputs/index.html index 39086c4..ed2274b 100644 --- a/inputs/index.html +++ b/inputs/index.html @@ -186,6 +186,24 @@ + + HeyVL + + + + + + + + + + + + https://fmtools.fyi/inputs/greatspn/
+ + HeyVL + https://fmtools.fyi/inputs/heyvl/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/inputs/heyvl/ + + JANI https://fmtools.fyi/inputs/jani/ diff --git a/interfaces/cli/index.html b/interfaces/cli/index.html index 72a9f2a..e87d6a8 100644 --- a/interfaces/cli/index.html +++ b/interfaces/cli/index.html @@ -138,6 +138,15 @@ + + + + Caesar + Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + + + + @@ -211,7 +220,7 @@ APIs and Bindings This tool is available through the following … MathSAT - [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … + [ Closed-Source Tool ]  MathSAT is an SMT solver supporting a wide range of theories … diff --git a/interfaces/cli/index.xml b/interfaces/cli/index.xml index 520824a..a545497 100644 --- a/interfaces/cli/index.xml +++ b/interfaces/cli/index.xml @@ -36,6 +36,13 @@ https://fmtools.fyi/tools/sat-smt/cadical/ <p>CaDiCaL is a simplified satisfiability solver.</p> + + Caesar + https://fmtools.fyi/tools/prob/caesar/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/prob/caesar/ + <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> + Colibri https://fmtools.fyi/tools/sat-smt/colibri/ @@ -97,7 +104,7 @@ https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 https://fmtools.fyi/tools/sat-smt/mathsat/ - <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).</p> MiniSat diff --git a/interfaces/index.html b/interfaces/index.html index 9d008b4..f805f87 100644 --- a/interfaces/index.html +++ b/interfaces/index.html @@ -231,6 +231,24 @@ + + + + + + + + + + + VSCode + + + diff --git a/interfaces/index.xml b/interfaces/index.xml index 04224f0..29846fb 100644 --- a/interfaces/index.xml +++ b/interfaces/index.xml @@ -64,5 +64,12 @@ https://fmtools.fyi/interfaces/rust/ + + VSCode + https://fmtools.fyi/interfaces/vscode/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/interfaces/vscode/ + + diff --git a/interfaces/vscode/index.html b/interfaces/vscode/index.html new file mode 100644 index 0000000..f32939c --- /dev/null +++ b/interfaces/vscode/index.html @@ -0,0 +1,131 @@ + + + + + + + + +VSCode | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + VSCode + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
CaesarStorm is a tool for the analysis of systems involving random or probabilistic phenomena. +
+ +
+ + + diff --git a/interfaces/vscode/index.xml b/interfaces/vscode/index.xml new file mode 100644 index 0000000..7da654f --- /dev/null +++ b/interfaces/vscode/index.xml @@ -0,0 +1,19 @@ + + + + VSCode on Formal Methods Tools + https://fmtools.fyi/interfaces/vscode/ + Recent content in VSCode on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Caesar + https://fmtools.fyi/tools/prob/caesar/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/prob/caesar/ + <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> + + + diff --git a/licenses/agpl-v3/index.html b/licenses/agpl-v3/index.html new file mode 100644 index 0000000..77d9da7 --- /dev/null +++ b/licenses/agpl-v3/index.html @@ -0,0 +1,130 @@ + + + + + + + + +AGPL-V3 | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + AGPL-V3 + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
CGAALCGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game …
+ +
+ + + diff --git a/licenses/agpl-v3/index.xml b/licenses/agpl-v3/index.xml new file mode 100644 index 0000000..87b4971 --- /dev/null +++ b/licenses/agpl-v3/index.xml @@ -0,0 +1,19 @@ + + + + AGPL-V3 on Formal Methods Tools + https://fmtools.fyi/licenses/agpl-v3/ + Recent content in AGPL-V3 on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + CGAAL + https://fmtools.fyi/tools/mc/cgaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cgaal/ + <p>CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).</p> + + + diff --git a/licenses/all-rights-reserved/index.html b/licenses/all-rights-reserved/index.html index 5cf017b..705ceac 100644 --- a/licenses/all-rights-reserved/index.html +++ b/licenses/all-rights-reserved/index.html @@ -107,9 +107,42 @@ + + CADP + [ Closed-Source Tool ]  CADP (“Construction and Analysis of Distributed … + + + + + MathSAT - [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … + [ Closed-Source Tool ]  MathSAT is an SMT solver supporting a wide range of theories … + + + + + + + NuXMV + [ Closed-Source Tool ]  nuXmv is a symbolic model checker for the analysis of synchronous … + + + + + + + Spin + Spin is a model checker for multi-threaded software. + + + + + + + + Uppaal + [ Closed-Source Tool ]  Uppaal is an integrated tool environment for modeling, validation and … diff --git a/licenses/all-rights-reserved/index.xml b/licenses/all-rights-reserved/index.xml index 2f55737..a75cafd 100644 --- a/licenses/all-rights-reserved/index.xml +++ b/licenses/all-rights-reserved/index.xml @@ -8,12 +8,40 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + CADP + https://fmtools.fyi/tools/mc/cadp/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cadp/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CADP (&ldquo;Construction and Analysis of Distributed Processes&rdquo;, formerly known as &ldquo;CAESAR/ALDEBARAN Development Package&rdquo;) is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.</p> + MathSAT https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 https://fmtools.fyi/tools/sat-smt/mathsat/ - <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).</p> + + + NuXMV + https://fmtools.fyi/tools/mc/nuxmv/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/nuxmv/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.</p> + + + Spin + https://fmtools.fyi/tools/mc/spin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/spin/ + <p>Spin is a model checker for multi-threaded software.</p> + + + Uppaal + https://fmtools.fyi/tools/mc/uppaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/uppaal/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).</p> diff --git a/licenses/apache-2.0/index.html b/licenses/apache-2.0/index.html index 4a713ba..1c61b81 100644 --- a/licenses/apache-2.0/index.html +++ b/licenses/apache-2.0/index.html @@ -107,12 +107,71 @@ + + BLAST + [ Not Maintained Since 2012 ] BLAST (Berkeley Lazy Abstraction Software verification Tool) is a … + + + + + + + CPAchecker + [ Closed-Source Tool ]  CPAchecker is a tool for configurable software verification. + + + + + + dReal [ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems … + + + + ESBMC + ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying … + + + + + + + JANI + The JANI specification defines the jani-model model interchange format and the jani-interaction tool … + + + + + + + Kind 2 + Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems. + + + + + + + + LEAN + cvc5 is an automatic theorem prover for SMT problems. + + + + + + + + Momba + Momba is a Python framework for dealing with quantitative models centered around the JANI-model … + + + diff --git a/licenses/apache-2.0/index.xml b/licenses/apache-2.0/index.xml index 17a5f4c..c646bbd 100644 --- a/licenses/apache-2.0/index.xml +++ b/licenses/apache-2.0/index.xml @@ -8,6 +8,20 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + BLAST + https://fmtools.fyi/tools/mc/blast/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/blast/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2012</span> <span style="display:none">]</span> </div> BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.</p> + + + CPAchecker + https://fmtools.fyi/tools/mc/cpachecker/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cpachecker/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CPAchecker is a tool for configurable software verification.</p> + dReal https://fmtools.fyi/tools/sat-smt/dreal/ @@ -15,5 +29,40 @@ https://fmtools.fyi/tools/sat-smt/dreal/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.</p> + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + JANI + https://fmtools.fyi/tools/mod/jani/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/jani/ + <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p> + + + Kind 2 + https://fmtools.fyi/tools/mc/kind2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/kind2/ + <p>Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.</p> + + + LEAN + https://fmtools.fyi/tools/sat-smt/lean/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/sat-smt/lean/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + + + Momba + https://fmtools.fyi/tools/mod/momba/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/momba/ + <p>Momba is a Python framework for dealing with quantitative models centered around the <a href="../jani" >JANI-model</a> interchange format.</p> + diff --git a/licenses/bsd-3-clause/index.html b/licenses/bsd-3-clause/index.html new file mode 100644 index 0000000..78b8c12 --- /dev/null +++ b/licenses/bsd-3-clause/index.html @@ -0,0 +1,130 @@ + + + + + + + + +BSD 3-Clause | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + BSD 3-Clause + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
ESBMCESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying …
+ +
+ + + diff --git a/licenses/bsd-3-clause/index.xml b/licenses/bsd-3-clause/index.xml new file mode 100644 index 0000000..93af869 --- /dev/null +++ b/licenses/bsd-3-clause/index.xml @@ -0,0 +1,19 @@ + + + + BSD 3-Clause on Formal Methods Tools + https://fmtools.fyi/licenses/bsd-3-clause/ + Recent content in BSD 3-Clause on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + diff --git a/licenses/bsd-4-clause/index.html b/licenses/bsd-4-clause/index.html new file mode 100644 index 0000000..f45f37f --- /dev/null +++ b/licenses/bsd-4-clause/index.html @@ -0,0 +1,130 @@ + + + + + + + + +BSD 4-Clause | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + BSD 4-Clause + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
ESBMCESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying …
+ +
+ + + diff --git a/licenses/bsd-4-clause/index.xml b/licenses/bsd-4-clause/index.xml new file mode 100644 index 0000000..6a40f2e --- /dev/null +++ b/licenses/bsd-4-clause/index.xml @@ -0,0 +1,19 @@ + + + + BSD 4-Clause on Formal Methods Tools + https://fmtools.fyi/licenses/bsd-4-clause/ + Recent content in BSD 4-Clause on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + diff --git a/licenses/bsd/index.html b/licenses/bsd/index.html index 01b7f79..24385a6 100644 --- a/licenses/bsd/index.html +++ b/licenses/bsd/index.html @@ -107,6 +107,15 @@ + + Concuerror + Concuerror is a stateless model checking tool for Erlang programs. + + + + + + cvc4 [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … @@ -122,6 +131,48 @@ + + + + Intrepyd + [ Not Maintained Since 2021 ] Intrepyd is a python module that provides a simulator and a model … + + + + + + + LTSmin + LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the … + + + + + + + Pnmc + Pnmc is a symbolic model checker for Petri nets. + + + + + + + + TAPAAL + TAPAAL is a tool for verification of timed-arc petri nets + + + + + + + + TLA+ + TLA+ is a high-level language for modeling programs and systems–especially concurrent and … + + + diff --git a/licenses/bsd/index.xml b/licenses/bsd/index.xml index d0dbd93..031d8b6 100644 --- a/licenses/bsd/index.xml +++ b/licenses/bsd/index.xml @@ -8,6 +8,13 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + Concuerror + https://fmtools.fyi/tools/mc/concuerror/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/concuerror/ + <p>Concuerror is a stateless model checking tool for Erlang programs.</p> + cvc4 https://fmtools.fyi/tools/sat-smt/cvc4/ @@ -22,6 +29,41 @@ https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> + + Intrepyd + https://fmtools.fyi/tools/mc/intrepyd/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/intrepyd/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> Intrepyd is a python module that provides a simulator and a model checker in form of a rich API, to allow the rapid prototyping of formal methods algorithms for the rigorous analysis of circuits, specifications, models.</p> + + + LTSmin + https://fmtools.fyi/tools/mc/ltsmin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/ltsmin/ + <p>LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.</p> + + + Pnmc + https://fmtools.fyi/tools/mc/pnmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/pnmc/ + <p>Pnmc is a symbolic model checker for Petri nets.</p> + + + TAPAAL + https://fmtools.fyi/tools/mc/tapaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/tapaal/ + <p>TAPAAL is a tool for verification of timed-arc petri nets</p> + + + TLA+ + https://fmtools.fyi/tools/mod/tlaplus/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/tlaplus/ + <p>TLA+ is a high-level language for modeling programs and systems&ndash;especially concurrent and distributed ones.</p> + Vampire https://fmtools.fyi/tools/sat-smt/vampire/ diff --git a/licenses/bsl/index.html b/licenses/bsl/index.html new file mode 100644 index 0000000..fd5f85d --- /dev/null +++ b/licenses/bsl/index.html @@ -0,0 +1,139 @@ + + + + + + + + +BSL | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + BSL + +

+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ToolDescription
EldaricaEldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs. +
mCRL2mCRL2 is a formal specification language with an associated toolset. The toolset can be used for …
+ +
+ + + diff --git a/licenses/bsl/index.xml b/licenses/bsl/index.xml new file mode 100644 index 0000000..d472b74 --- /dev/null +++ b/licenses/bsl/index.xml @@ -0,0 +1,26 @@ + + + + BSL on Formal Methods Tools + https://fmtools.fyi/licenses/bsl/ + Recent content in BSL on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Eldarica + https://fmtools.fyi/tools/mc/eldarica/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/eldarica/ + <p>Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.</p> + + + mCRL2 + https://fmtools.fyi/tools/mc/mcrl2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mcrl2/ + <p>mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.</p> + + + diff --git a/licenses/gpl/index.html b/licenses/gpl/index.html new file mode 100644 index 0000000..2399404 --- /dev/null +++ b/licenses/gpl/index.html @@ -0,0 +1,131 @@ + + + + + + + + +GPL | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + GPL + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
RoméoRomeo allows the modelling of complex systems using extensions of time Petri nets. +
+ +
+ + + diff --git a/licenses/gpl/index.xml b/licenses/gpl/index.xml new file mode 100644 index 0000000..039afb5 --- /dev/null +++ b/licenses/gpl/index.xml @@ -0,0 +1,19 @@ + + + + GPL on Formal Methods Tools + https://fmtools.fyi/licenses/gpl/ + Recent content in GPL on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Roméo + https://fmtools.fyi/tools/mc/romeo/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/romeo/ + <p>Romeo allows the modelling of complex systems using extensions of time Petri nets.</p> + + + diff --git a/licenses/gplv2/index.html b/licenses/gplv2/index.html index 171804d..80881c8 100644 --- a/licenses/gplv2/index.html +++ b/licenses/gplv2/index.html @@ -139,6 +139,23 @@ APIs and Bindings This tool is available through the following … + + + + TAPAAL + TAPAAL is a tool for verification of timed-arc petri nets + + + + + + + + TLA+ + TLA+ is a high-level language for modeling programs and systems–especially concurrent and … + + + diff --git a/licenses/gplv2/index.xml b/licenses/gplv2/index.xml index 007e6bb..2907cd5 100644 --- a/licenses/gplv2/index.xml +++ b/licenses/gplv2/index.xml @@ -36,5 +36,19 @@ https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p>
+ + TAPAAL + https://fmtools.fyi/tools/mc/tapaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/tapaal/ + <p>TAPAAL is a tool for verification of timed-arc petri nets</p> + + + TLA+ + https://fmtools.fyi/tools/mod/tlaplus/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/tlaplus/ + <p>TLA+ is a high-level language for modeling programs and systems&ndash;especially concurrent and distributed ones.</p> + diff --git a/licenses/gplv3/index.html b/licenses/gplv3/index.html index 193450f..c46c5a4 100644 --- a/licenses/gplv3/index.html +++ b/licenses/gplv3/index.html @@ -107,6 +107,22 @@ + + ESBMC + ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying … + + + + + + + IMITATOR + IMITATOR is a parametric timed model checker taking as input extensions of parametric timed … + + + + + OpenSMT OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making … @@ -121,6 +137,14 @@ + + + + SM(P/)T + SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes … + + + @@ -130,6 +154,14 @@ APIs and … + + + + SpaceEx + The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to … + + + diff --git a/licenses/gplv3/index.xml b/licenses/gplv3/index.xml index d73c207..88bd94b 100644 --- a/licenses/gplv3/index.xml +++ b/licenses/gplv3/index.xml @@ -8,6 +8,20 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + IMITATOR + https://fmtools.fyi/tools/mc/imitator/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/imitator/ + <p>IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.</p> + OpenSMT https://fmtools.fyi/tools/sat-smt/opensmt/ @@ -22,6 +36,13 @@ https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> + + SM(P/)T + https://fmtools.fyi/tools/mc/smpt/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/smpt/ + <p>SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).</p> + SMTInterpol https://fmtools.fyi/tools/sat-smt/smtinterpol/ @@ -29,6 +50,13 @@ https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> + + SpaceEx + https://fmtools.fyi/tools/mc/spaceex/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/spaceex/ + <p>The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.</p> + STAMINA https://fmtools.fyi/tools/prob/stamina/ diff --git a/licenses/index.html b/licenses/index.html index 1041565..cad49c6 100644 --- a/licenses/index.html +++ b/licenses/index.html @@ -96,6 +96,24 @@ + + AGPL-V3 + + + + + + + + + + + + + BSD 3-Clause + + + + + + + + + + + + + + BSD 4-Clause + + + + + + + + + + + + + + BSL + + + + + + + + + + + + + + GPL + + + + + + + + + + + + + ISC + + + + + + + + + + + + + + LGPL + + + + + + + + + + + + + + + + + + + + + + + Open Source 3.0 + + + + + + + + + + + + + + Unilicense + + + diff --git a/licenses/index.xml b/licenses/index.xml index 9415c20..f2d5d31 100644 --- a/licenses/index.xml +++ b/licenses/index.xml @@ -8,6 +8,13 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + AGPL-V3 + https://fmtools.fyi/licenses/agpl-v3/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/licenses/agpl-v3/ + + All Rights Reserved https://fmtools.fyi/licenses/all-rights-reserved/ @@ -29,6 +36,34 @@ https://fmtools.fyi/licenses/bsd/ + + BSD 3-Clause + https://fmtools.fyi/licenses/bsd-3-clause/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/licenses/bsd-3-clause/ + + + + BSD 4-Clause + https://fmtools.fyi/licenses/bsd-4-clause/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/licenses/bsd-4-clause/ + + + + BSL + https://fmtools.fyi/licenses/bsl/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/licenses/bsl/ + + + + GPL + https://fmtools.fyi/licenses/gpl/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/licenses/gpl/ + + GPLv2 https://fmtools.fyi/licenses/gplv2/ @@ -43,6 +78,20 @@ https://fmtools.fyi/licenses/gplv3/ + + ISC + https://fmtools.fyi/licenses/isc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/licenses/isc/ + + + + LGPL + https://fmtools.fyi/licenses/lgpl/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/licenses/lgpl/ + + LGPLv2 https://fmtools.fyi/licenses/lgplv2/ @@ -64,5 +113,19 @@ https://fmtools.fyi/licenses/ocamlpro-non-commercial/ + + Open Source 3.0 + https://fmtools.fyi/licenses/open-source-3.0/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/licenses/open-source-3.0/ + + + + Unilicense + https://fmtools.fyi/licenses/unilicense/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/licenses/unilicense/ + + diff --git a/licenses/isc/index.html b/licenses/isc/index.html new file mode 100644 index 0000000..f74cb5e --- /dev/null +++ b/licenses/isc/index.html @@ -0,0 +1,131 @@ + + + + + + + + +ISC | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + ISC + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
DSCheckDSCheck is an experimental model checker for testing concurrent OCaml programs. +
+ +
+ + + diff --git a/licenses/isc/index.xml b/licenses/isc/index.xml new file mode 100644 index 0000000..7aa8fe3 --- /dev/null +++ b/licenses/isc/index.xml @@ -0,0 +1,19 @@ + + + + ISC on Formal Methods Tools + https://fmtools.fyi/licenses/isc/ + Recent content in ISC on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + DSCheck + https://fmtools.fyi/tools/mc/dscheck/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/dscheck/ + <p>DSCheck is an experimental model checker for testing concurrent OCaml programs.</p> + + + diff --git a/licenses/lgpl/index.html b/licenses/lgpl/index.html new file mode 100644 index 0000000..7ee31de --- /dev/null +++ b/licenses/lgpl/index.html @@ -0,0 +1,131 @@ + + + + + + + + +LGPL | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + LGPL + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
NuSMVNuSMV is a symbolic model checker. +
+ +
+ + + diff --git a/licenses/lgpl/index.xml b/licenses/lgpl/index.xml new file mode 100644 index 0000000..926ddd9 --- /dev/null +++ b/licenses/lgpl/index.xml @@ -0,0 +1,19 @@ + + + + LGPL on Formal Methods Tools + https://fmtools.fyi/licenses/lgpl/ + Recent content in LGPL on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + NuSMV + https://fmtools.fyi/tools/mc/nusmv/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/nusmv/ + <p>NuSMV is a symbolic model checker.</p> + + + diff --git a/licenses/mit/index.html b/licenses/mit/index.html index 0433897..2393447 100644 --- a/licenses/mit/index.html +++ b/licenses/mit/index.html @@ -130,6 +130,15 @@ + + + + Caesar + Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + + + + @@ -148,6 +157,23 @@ APIs and Bindings This tool is available through the following … + + + + ESBMC + ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying … + + + + + + + Geyser + Geyser is a simple symbolic model checker for propositional transition system systems. + + + + @@ -157,6 +183,22 @@ APIs and Bindings This tool is available through the following … + + + + ImSpin + ImSpin is a frontend for the SPIN model checker, providing an environment for users engaged in model … + + + + + + + JANI + The JANI specification defines the jani-model model interchange format and the jani-interaction tool … + + + @@ -166,6 +208,14 @@ APIs and Bindings This tool is available through the following … + + + + Mercury + [ Not Maintained Since 2020 ] Mercury is a Model Checker developed for multicore, multiprocessors … + + + @@ -174,6 +224,22 @@ APIs and Bindings This tool is available through the following … + + + + Momba + Momba is a Python framework for dealing with quantitative models centered around the JANI-model … + + + + + + + MUNTA + [ Not Maintained Since 2020 ] MUNTA is a model checker for the popular realtime systems modeling … + + + @@ -199,6 +265,15 @@ APIs and Bindings This tool is available through the … + + + + stateright + stateright is a Rust library for model checking systems, with an emphasis on distributed systems. + + + + diff --git a/licenses/mit/index.xml b/licenses/mit/index.xml index b337f06..bcaca02 100644 --- a/licenses/mit/index.xml +++ b/licenses/mit/index.xml @@ -29,6 +29,13 @@ https://fmtools.fyi/tools/sat-smt/cadical/ <p>CaDiCaL is a simplified satisfiability solver.</p>
+ + Caesar + https://fmtools.fyi/tools/prob/caesar/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/prob/caesar/ + <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> + Colibri https://fmtools.fyi/tools/sat-smt/colibri/ @@ -43,6 +50,20 @@ https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + Geyser + https://fmtools.fyi/tools/mc/geyser/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/geyser/ + <p>Geyser is a simple symbolic model checker for propositional transition system systems.</p> + Glucose https://fmtools.fyi/tools/sat-smt/glucose/ @@ -50,6 +71,20 @@ https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> + + ImSpin + https://fmtools.fyi/tools/mc/imspin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/imspin/ + <p>ImSpin is a frontend for the <a href="../spin" >SPIN</a> model checker, providing an environment for users engaged in model checking tasks.</p> + + + JANI + https://fmtools.fyi/tools/mod/jani/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/jani/ + <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p> + Lingeling https://fmtools.fyi/tools/sat-smt/lingeling/ @@ -57,6 +92,13 @@ https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> + + Mercury + https://fmtools.fyi/tools/mc/mercury/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mercury/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.</p> + MiniSat https://fmtools.fyi/tools/sat-smt/minisat/ @@ -64,6 +106,20 @@ https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> + + Momba + https://fmtools.fyi/tools/mod/momba/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/momba/ + <p>Momba is a Python framework for dealing with quantitative models centered around the <a href="../jani" >JANI-model</a> interchange format.</p> + + + MUNTA + https://fmtools.fyi/tools/mc/munta/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/munta/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata</p> + Q3B https://fmtools.fyi/tools/sat-smt/q3b/ @@ -85,6 +141,13 @@ https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> + + stateright + https://fmtools.fyi/tools/mc/stateright/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/stateright/ + <p><code>stateright</code> is a Rust library for model checking systems, with an emphasis on distributed systems.</p> + STP https://fmtools.fyi/tools/sat-smt/stp/ diff --git a/licenses/open-source-3.0/index.html b/licenses/open-source-3.0/index.html new file mode 100644 index 0000000..f645866 --- /dev/null +++ b/licenses/open-source-3.0/index.html @@ -0,0 +1,139 @@ + + + + + + + + +Open Source 3.0 | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Open Source 3.0 + +

+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ToolDescription
TAPAALTAPAAL is a tool for verification of timed-arc petri nets +
TLA+TLA+ is a high-level language for modeling programs and systems–especially concurrent and …
+ +
+ + + diff --git a/licenses/open-source-3.0/index.xml b/licenses/open-source-3.0/index.xml new file mode 100644 index 0000000..0e03cb1 --- /dev/null +++ b/licenses/open-source-3.0/index.xml @@ -0,0 +1,26 @@ + + + + Open Source 3.0 on Formal Methods Tools + https://fmtools.fyi/licenses/open-source-3.0/ + Recent content in Open Source 3.0 on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + TAPAAL + https://fmtools.fyi/tools/mc/tapaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/tapaal/ + <p>TAPAAL is a tool for verification of timed-arc petri nets</p> + + + TLA+ + https://fmtools.fyi/tools/mod/tlaplus/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/tlaplus/ + <p>TLA+ is a high-level language for modeling programs and systems&ndash;especially concurrent and distributed ones.</p> + + + diff --git a/licenses/unilicense/index.html b/licenses/unilicense/index.html new file mode 100644 index 0000000..7e10268 --- /dev/null +++ b/licenses/unilicense/index.html @@ -0,0 +1,140 @@ + + + + + + + + +Unilicense | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + Unilicense + +

+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ToolDescription
pyPLpyPL is a naive model generator, model checker and theorem prover. +
RumurRumur is a model checker. +
+ +
+ + + diff --git a/licenses/unilicense/index.xml b/licenses/unilicense/index.xml new file mode 100644 index 0000000..b45b254 --- /dev/null +++ b/licenses/unilicense/index.xml @@ -0,0 +1,26 @@ + + + + Unilicense on Formal Methods Tools + https://fmtools.fyi/licenses/unilicense/ + Recent content in Unilicense on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + pyPL + https://fmtools.fyi/tools/mc/pypl/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/pypl/ + <p>pyPL is a naive model generator, model checker and theorem prover.</p> + + + Rumur + https://fmtools.fyi/tools/mc/rumur/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/rumur/ + <p>Rumur is a model checker.</p> + + + diff --git a/maintenance/actively-maintained/index.html b/maintenance/actively-maintained/index.html index 853d701..ec40f1c 100644 --- a/maintenance/actively-maintained/index.html +++ b/maintenance/actively-maintained/index.html @@ -130,6 +130,31 @@ + + + + CADP + [ Closed-Source Tool ]  CADP (“Construction and Analysis of Distributed … + + + + + + + Caesar + Storm is a tool for the analysis of systems involving random or probabilistic phenomena. + + + + + + + + CGAAL + CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game … + + + @@ -139,6 +164,24 @@ + + + + Concuerror + Concuerror is a stateless model checking tool for Erlang programs. + + + + + + + + CPAchecker + [ Closed-Source Tool ]  CPAchecker is a tool for configurable software verification. + + + + @@ -157,6 +200,15 @@ APIs and Bindings This tool is available through the following … + + + + DSCheck + DSCheck is an experimental model checker for testing concurrent OCaml programs. + + + + @@ -165,6 +217,32 @@ APIs and Bindings This tool is available through the following … + + + + Eldarica + Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs. + + + + + + + + ESBMC + ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying … + + + + + + + Geyser + Geyser is a simple symbolic model checker for propositional transition system systems. + + + + @@ -174,6 +252,48 @@ APIs and Bindings This tool is available through the following … + + + + IMITATOR + IMITATOR is a parametric timed model checker taking as input extensions of parametric timed … + + + + + + + ImSpin + ImSpin is a frontend for the SPIN model checker, providing an environment for users engaged in model … + + + + + + + JANI + The JANI specification defines the jani-model model interchange format and the jani-interaction tool … + + + + + + + Kind 2 + Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems. + + + + + + + + LEAN + cvc5 is an automatic theorem prover for SMT problems. + + + + @@ -183,11 +303,52 @@ APIs and Bindings This tool is available through the following … + + + + LTSmin + LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the … + + + MathSAT - [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … + [ Closed-Source Tool ]  MathSAT is an SMT solver supporting a wide range of theories … + + + + + + + mCRL2 + mCRL2 is a formal specification language with an associated toolset. The toolset can be used for … + + + + + + + Momba + Momba is a Python framework for dealing with quantitative models centered around the JANI-model … + + + + + + + NuSMV + NuSMV is a symbolic model checker. + + + + + + + + NuXMV + [ Closed-Source Tool ]  nuXmv is a symbolic model checker for the analysis of synchronous … @@ -207,6 +368,15 @@ APIs and Bindings This tool is available through the following … + + + + Pnmc + Pnmc is a symbolic model checker for Petri nets. + + + + @@ -215,6 +385,33 @@ APIs and Bindings This tool is available through the following … + + + + pyPL + pyPL is a naive model generator, model checker and theorem prover. + + + + + + + + Roméo + Romeo allows the modelling of complex systems using extensions of time Petri nets. + + + + + + + + Rumur + Rumur is a model checker. + + + + @@ -224,6 +421,14 @@ APIs and Bindings This tool is available through the following … + + + + SM(P/)T + SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes … + + + @@ -242,6 +447,23 @@ APIs and … + + + + SpaceEx + The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to … + + + + + + + Spin + Spin is a model checker for multi-threaded software. + + + + @@ -250,6 +472,15 @@ APIs and … + + + + stateright + stateright is a Rust library for model checking systems, with an emphasis on distributed systems. + + + + @@ -268,6 +499,31 @@ APIs and Bindings This tool is available … + + + + TAPAAL + TAPAAL is a tool for verification of timed-arc petri nets + + + + + + + + TLA+ + TLA+ is a high-level language for modeling programs and systems–especially concurrent and … + + + + + + + Uppaal + [ Closed-Source Tool ]  Uppaal is an integrated tool environment for modeling, validation and … + + + diff --git a/maintenance/actively-maintained/index.xml b/maintenance/actively-maintained/index.xml index c3797ab..3fda198 100644 --- a/maintenance/actively-maintained/index.xml +++ b/maintenance/actively-maintained/index.xml @@ -29,6 +29,27 @@ https://fmtools.fyi/tools/sat-smt/cadical/ <p>CaDiCaL is a simplified satisfiability solver.</p>
+ + CADP + https://fmtools.fyi/tools/mc/cadp/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cadp/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CADP (&ldquo;Construction and Analysis of Distributed Processes&rdquo;, formerly known as &ldquo;CAESAR/ALDEBARAN Development Package&rdquo;) is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.</p> + + + Caesar + https://fmtools.fyi/tools/prob/caesar/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/prob/caesar/ + <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> + + + CGAAL + https://fmtools.fyi/tools/mc/cgaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cgaal/ + <p>CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).</p> + Colibri https://fmtools.fyi/tools/sat-smt/colibri/ @@ -36,6 +57,20 @@ https://fmtools.fyi/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> + + Concuerror + https://fmtools.fyi/tools/mc/concuerror/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/concuerror/ + <p>Concuerror is a stateless model checking tool for Erlang programs.</p> + + + CPAchecker + https://fmtools.fyi/tools/mc/cpachecker/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cpachecker/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CPAchecker is a tool for configurable software verification.</p> + CryptoMiniSat https://fmtools.fyi/tools/sat-smt/cryptominisat/ @@ -50,6 +85,13 @@ https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> + + DSCheck + https://fmtools.fyi/tools/mc/dscheck/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/dscheck/ + <p>DSCheck is an experimental model checker for testing concurrent OCaml programs.</p> + E https://fmtools.fyi/tools/sat-smt/e/ @@ -57,6 +99,27 @@ https://fmtools.fyi/tools/sat-smt/e/ <p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.</p> + + Eldarica + https://fmtools.fyi/tools/mc/eldarica/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/eldarica/ + <p>Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.</p> + + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + Geyser + https://fmtools.fyi/tools/mc/geyser/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/geyser/ + <p>Geyser is a simple symbolic model checker for propositional transition system systems.</p> + Glucose https://fmtools.fyi/tools/sat-smt/glucose/ @@ -64,6 +127,41 @@ https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> + + IMITATOR + https://fmtools.fyi/tools/mc/imitator/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/imitator/ + <p>IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.</p> + + + ImSpin + https://fmtools.fyi/tools/mc/imspin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/imspin/ + <p>ImSpin is a frontend for the <a href="../spin" >SPIN</a> model checker, providing an environment for users engaged in model checking tasks.</p> + + + JANI + https://fmtools.fyi/tools/mod/jani/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/jani/ + <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p> + + + Kind 2 + https://fmtools.fyi/tools/mc/kind2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/kind2/ + <p>Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.</p> + + + LEAN + https://fmtools.fyi/tools/sat-smt/lean/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/sat-smt/lean/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + Lingeling https://fmtools.fyi/tools/sat-smt/lingeling/ @@ -71,12 +169,47 @@ https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> + + LTSmin + https://fmtools.fyi/tools/mc/ltsmin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/ltsmin/ + <p>LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.</p> + MathSAT https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 https://fmtools.fyi/tools/sat-smt/mathsat/ - <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).</p> + + + mCRL2 + https://fmtools.fyi/tools/mc/mcrl2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mcrl2/ + <p>mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.</p> + + + Momba + https://fmtools.fyi/tools/mod/momba/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/momba/ + <p>Momba is a Python framework for dealing with quantitative models centered around the <a href="../jani" >JANI-model</a> interchange format.</p> + + + NuSMV + https://fmtools.fyi/tools/mc/nusmv/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/nusmv/ + <p>NuSMV is a symbolic model checker.</p> + + + NuXMV + https://fmtools.fyi/tools/mc/nuxmv/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/nuxmv/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.</p> OpenSMT @@ -92,6 +225,13 @@ https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> + + Pnmc + https://fmtools.fyi/tools/mc/pnmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/pnmc/ + <p>Pnmc is a symbolic model checker for Petri nets.</p> + PRISM https://fmtools.fyi/tools/prob/prism/ @@ -99,6 +239,27 @@ https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> + + pyPL + https://fmtools.fyi/tools/mc/pypl/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/pypl/ + <p>pyPL is a naive model generator, model checker and theorem prover.</p> + + + Roméo + https://fmtools.fyi/tools/mc/romeo/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/romeo/ + <p>Romeo allows the modelling of complex systems using extensions of time Petri nets.</p> + + + Rumur + https://fmtools.fyi/tools/mc/rumur/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/rumur/ + <p>Rumur is a model checker.</p> + Sally https://fmtools.fyi/tools/mc/sally/ @@ -106,6 +267,13 @@ https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> + + SM(P/)T + https://fmtools.fyi/tools/mc/smpt/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/smpt/ + <p>SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).</p> + SMT-RAT https://fmtools.fyi/tools/sat-smt/smt-rat/ @@ -120,6 +288,20 @@ https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> + + SpaceEx + https://fmtools.fyi/tools/mc/spaceex/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/spaceex/ + <p>The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.</p> + + + Spin + https://fmtools.fyi/tools/mc/spin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/spin/ + <p>Spin is a model checker for multi-threaded software.</p> + STAMINA https://fmtools.fyi/tools/prob/stamina/ @@ -127,6 +309,13 @@ https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> + + stateright + https://fmtools.fyi/tools/mc/stateright/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/stateright/ + <p><code>stateright</code> is a Rust library for model checking systems, with an emphasis on distributed systems.</p> + Storm https://fmtools.fyi/tools/prob/storm/ @@ -141,6 +330,27 @@ https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> + + TAPAAL + https://fmtools.fyi/tools/mc/tapaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/tapaal/ + <p>TAPAAL is a tool for verification of timed-arc petri nets</p> + + + TLA+ + https://fmtools.fyi/tools/mod/tlaplus/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mod/tlaplus/ + <p>TLA+ is a high-level language for modeling programs and systems&ndash;especially concurrent and distributed ones.</p> + + + Uppaal + https://fmtools.fyi/tools/mc/uppaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/uppaal/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).</p> + Vampire https://fmtools.fyi/tools/sat-smt/vampire/ diff --git a/maintenance/not-maintained/index.html b/maintenance/not-maintained/index.html index 0779ae5..27da502 100644 --- a/maintenance/not-maintained/index.html +++ b/maintenance/not-maintained/index.html @@ -107,6 +107,14 @@ + + BLAST + [ Not Maintained Since 2012 ] BLAST (Berkeley Lazy Abstraction Software verification Tool) is a … + + + + + Boolector [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … @@ -129,6 +137,39 @@ + + + + Intrepyd + [ Not Maintained Since 2021 ] Intrepyd is a python module that provides a simulator and a model … + + + + + + + LTSA + [ Not Maintained Since 2018 ] LTSA is a verification tool for concurrent systems. It mechanically … + + + + + + + mcltl-rs + [ Not Maintained Since 2020 ] mcltl-rs is an experimental model checker for LTL written in Rust. + + + + + + + + Mercury + [ Not Maintained Since 2020 ] Mercury is a Model Checker developed for multicore, multiprocessors … + + + @@ -137,6 +178,14 @@ + + + + MUNTA + [ Not Maintained Since 2020 ] MUNTA is a model checker for the popular realtime systems modeling … + + + @@ -154,6 +203,14 @@ + + + + TimeSolver + [ Not Maintained Since 2019 ] TimeSolver is a Model Checker for timed automata that uses pes … + + + diff --git a/maintenance/not-maintained/index.xml b/maintenance/not-maintained/index.xml index 60a5f2e..2255872 100644 --- a/maintenance/not-maintained/index.xml +++ b/maintenance/not-maintained/index.xml @@ -8,6 +8,13 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + BLAST + https://fmtools.fyi/tools/mc/blast/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/blast/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2012</span> <span style="display:none">]</span> </div> BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.</p> + Boolector https://fmtools.fyi/tools/sat-smt/boolector/ @@ -29,6 +36,34 @@ https://fmtools.fyi/tools/sat-smt/dreal/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.</p> + + Intrepyd + https://fmtools.fyi/tools/mc/intrepyd/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/intrepyd/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> Intrepyd is a python module that provides a simulator and a model checker in form of a rich API, to allow the rapid prototyping of formal methods algorithms for the rigorous analysis of circuits, specifications, models.</p> + + + LTSA + https://fmtools.fyi/tools/mc/ltsa/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/ltsa/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2018</span> <span style="display:none">]</span> </div> LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour.</p> + + + mcltl-rs + https://fmtools.fyi/tools/mc/mcltlrs/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mcltlrs/ + <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> <p>mcltl-rs is an experimental model checker for LTL written in Rust.</p> + + + Mercury + https://fmtools.fyi/tools/mc/mercury/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mercury/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.</p> + MiniSat https://fmtools.fyi/tools/sat-smt/minisat/ @@ -36,6 +71,13 @@ https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> + + MUNTA + https://fmtools.fyi/tools/mc/munta/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/munta/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata</p> + Q3B https://fmtools.fyi/tools/sat-smt/q3b/ @@ -50,5 +92,12 @@ https://fmtools.fyi/tools/sat-smt/riss/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span> <span style="display:none">]</span> </div> Riss is a SAT solving tool collection.</p> + + TimeSolver + https://fmtools.fyi/tools/mc/timesolver/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/timesolver/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2019</span> <span style="display:none">]</span> </div> TimeSolver is a Model Checker for timed automata that uses pes (predicate equation systems).</p> + diff --git a/sitemap.xml b/sitemap.xml index 9cb46ca..c312395 100644 --- a/sitemap.xml +++ b/sitemap.xml @@ -2,14 +2,23 @@ + https://fmtools.fyi/developers/-leslie-lamport/ + 2025-06-07T00:00:00+00:00 + https://fmtools.fyi/interfaces/.net/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/aalborg-university/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/about/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/maintenance/actively-maintained/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/licenses/agpl-v3/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/albert-ludwigs-universit%C3%A4t/ 2025-06-07T00:00:00+00:00 @@ -31,15 +40,30 @@ https://fmtools.fyi/applications/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/bell-labs/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/sat-smt/bitwuzla/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/blast/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/sat-smt/boolector/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/licenses/bsd/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/licenses/bsd-3-clause/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/licenses/bsd-4-clause/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/licenses/bsl/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/interfaces/c/ 2025-06-07T00:00:00+00:00 @@ -49,12 +73,24 @@ https://fmtools.fyi/tools/sat-smt/cadical/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/cadp/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/prob/caesar/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/techniques/car/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/techniques/cdcl/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/cea/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/cgaal/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/interfaces/cli/ 2025-06-07T00:00:00+00:00 @@ -67,6 +103,9 @@ https://fmtools.fyi/tools/prob/comics/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/concuerror/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/applications/constraint-solver/ 2025-06-07T00:00:00+00:00 @@ -76,6 +115,9 @@ https://fmtools.fyi/applications/counterexample-generator/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/cpachecker/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/sat-smt/cryptominisat/ 2025-06-07T00:00:00+00:00 @@ -100,24 +142,42 @@ https://fmtools.fyi/tools/sat-smt/dreal/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/dscheck/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/sat-smt/e/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/eindhoven-university-of-technology/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/eldarica/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/esbmc/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/federal-university-of-amazonas/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/fondazione-bruno-kessler/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/inputs/galileo/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/geyser/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/gilles-audemard/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/sat-smt/glucose/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/licenses/gpl/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/licenses/gplv2/ 2025-06-07T00:00:00+00:00 @@ -130,27 +190,72 @@ https://fmtools.fyi/inputs/greatspn/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/inputs/heyvl/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/applications/hybrid-systems/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/imitator/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/imspin/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/inputs/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/inria-rh%C3%B4ne-alpes/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/inria-rocquencourt/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/interfaces/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/intrepyd/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/licenses/isc/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/iscas/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/inputs/jani/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mod/jani/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/interfaces/java/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/johannes-kepler-universit%C3%A4t-linz/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/jonathan-nadal/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/kind2/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/laas-cnrs/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/laurent-simon/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/sat-smt/lean/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/lean-fro/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/licenses/lgpl/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/licenses/lgplv2/ 2025-06-07T00:00:00+00:00 @@ -163,6 +268,15 @@ https://fmtools.fyi/developers/loria/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/ltsa/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/ltsmin/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/ludwig-maximilians-universit%C3%A4t-m%C3%BCnchen/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/maintenance/ 2025-06-07T00:00:00+00:00 @@ -172,6 +286,18 @@ https://fmtools.fyi/tools/sat-smt/mathsat/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/matthew-fernandez/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/mcltlrs/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/mcrl2/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/mercury/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/microsoft-research/ 2025-06-07T00:00:00+00:00 @@ -190,9 +316,27 @@ https://fmtools.fyi/tools/mc/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/applications/model-generator/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mod/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/applications/modeling-framework/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/applications/modeling-language/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mod/momba/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/inputs/mrmc/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/munta/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/niklas-e%C3%A9n/ 2025-06-07T00:00:00+00:00 @@ -205,6 +349,12 @@ https://fmtools.fyi/maintenance/not-maintained/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/nusmv/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/nuxmv/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/ocaml-pro/ 2025-06-07T00:00:00+00:00 @@ -214,6 +364,9 @@ https://fmtools.fyi/interfaces/online/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/licenses/open-source-3.0/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/sat-smt/opensmt/ 2025-06-07T00:00:00+00:00 @@ -223,6 +376,15 @@ https://fmtools.fyi/tools/sat-smt/parafrost/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/applications/parameter-synthesizer/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/techniques/pdr/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/pnmc/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/inputs/pnml/ 2025-06-07T00:00:00+00:00 @@ -238,9 +400,15 @@ https://fmtools.fyi/applications/probabilistic-model-checker/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/applications/probabilistic-program-prover/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/prob/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/pypl/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/interfaces/python/ 2025-06-07T00:00:00+00:00 @@ -250,12 +418,21 @@ https://fmtools.fyi/tools/sat-smt/riss/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/romeo/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/rumur/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/interfaces/rust/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/rwth-aachen/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/saarland-university/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/inputs/sally/ 2025-06-07T00:00:00+00:00 @@ -268,6 +445,9 @@ https://fmtools.fyi/applications/sat-solver/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/smpt/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/applications/smt-solver/ 2025-06-07T00:00:00+00:00 @@ -280,6 +460,12 @@ https://fmtools.fyi/inputs/smtlib2/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/spaceex/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/spin/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/sri-international/ 2025-06-07T00:00:00+00:00 @@ -289,12 +475,18 @@ https://fmtools.fyi/developers/stanford-university/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/stateright/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/prob/storm/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/sat-smt/stp/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/tapaal/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/techniques/ 2025-06-07T00:00:00+00:00 @@ -307,12 +499,30 @@ https://fmtools.fyi/applications/theorem-prover/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/timesolver/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mod/tlaplus/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/tu-wien/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/uliege/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/licenses/unilicense/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/universidad-nacional-de-cordoba/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/universite-sorbonne-paris-nord/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/university-of-bristol/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/university-of-freiburg/ 2025-06-07T00:00:00+00:00 @@ -325,18 +535,51 @@ https://fmtools.fyi/developers/university-of-lugano/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/university-of-manchester/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/university-of-nantes/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/university-of-southampton/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/university-of-stellenbosch/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/university-of-twente/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/university-of-virginia/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/tools/mc/uppaal/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/uppsala-universitet/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/uppsala-university/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/developers/utah-state-university/ 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/sat-smt/vampire/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/verimag/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/tools/sat-smt/verit/ 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/developers/vertics/ + 2025-06-07T00:00:00+00:00 + + https://fmtools.fyi/interfaces/vscode/ + 2025-06-07T00:00:00+00:00 https://fmtools.fyi/inputs/yices-2/ 2025-06-07T00:00:00+00:00 diff --git a/taxonomies/index.html b/taxonomies/index.html index 44b68eb..0813330 100644 --- a/taxonomies/index.html +++ b/taxonomies/index.html @@ -148,6 +148,23 @@ the tools developed at SRI International).

+ + Hybrid Systems + + + + + + + + + + + + + Model Generator + + + + + + + + + + + + + Modeling Framework + + + + + + + + + + + + + Modeling Language + + + + + + + + + + + + + Parameter Synthesizer + + + + + + + + + + + + + Probabilistic Program Prover + + + + + + + + + + + + + Leslie Lamport + + + + + + + + + + + + + Aalborg University + + + + + + + + + + + + + Bell Labs + + + + + + + + + + + + + Federal University of Amazonas + + + + + + + + + + + + + INRIA Rocquencourt + + + + + + + + + + + + + ISCAS + + + + + + + + + + + + + Jonathan Nadal + + + + + + + + + + + + + LAAS-CNRS + + + + + + + + + + + + + Lean FRO + + + + + + + + + + + + + Ludwig-Maximilians-Universität München + + + + + + + + + + + + + Matthew Fernandez + + + + + + + + + + + + + Saarland University + + + + + + + + + + + + + Universidad Nacional De Cordoba + + + + + + + + + + + + + Universite Sorbonne Paris Nord + + + + + + + + + + + + + University of Bristol + + + + + + + + + + + + + University of Manchester + + + + + + + + + + + + + University of Nantes + + + + + + + + + + + + + University of Southampton + + + + + + + + + + + + + University of Stellenbosch + + + + + + + + + + + + + University of Twente + + + + + + + + + + + + + Uppsala Universitet + + + + + + + + + + + + + Uppsala University + + + + + + + + + + + + + + + + + + + + + Verimag + + + + + + + + + + + + + Vertics + + + @@ -843,6 +1353,23 @@ the tools developed at SRI International).

+ + HeyVL + + + + + + + + + + + + + + + + + + + + + VSCode + + + @@ -1128,6 +1672,23 @@ the tools developed at SRI International).

+ + AGPL-V3 + + + + + + + + + + + + + BSD 3-Clause + + + + + + + + + + + + + BSD 4-Clause + + + + + + + + + + + + + BSL + + + + + + + + + + + + + GPL + + + + + + + + + + + + + ISC + + + + + + + + + + + + + LGPL + + + + + + + + + + + + + + + + + + + + + Open Source 3.0 + + + + + + + + + + + + + Unilicense + + + @@ -1328,6 +2025,23 @@ the tools developed at SRI International).

+ + CAR + + + + + + + + + + + + + + + + + + + + + PDR + + + diff --git a/techniques/car/index.html b/techniques/car/index.html new file mode 100644 index 0000000..5da2d84 --- /dev/null +++ b/techniques/car/index.html @@ -0,0 +1,131 @@ + + + + + + + + +CAR | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + CAR + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
GeyserGeyser is a simple symbolic model checker for propositional transition system systems. +
+ +
+ + + diff --git a/techniques/car/index.xml b/techniques/car/index.xml new file mode 100644 index 0000000..8aaaeac --- /dev/null +++ b/techniques/car/index.xml @@ -0,0 +1,19 @@ + + + + CAR on Formal Methods Tools + https://fmtools.fyi/techniques/car/ + Recent content in CAR on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Geyser + https://fmtools.fyi/tools/mc/geyser/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/geyser/ + <p>Geyser is a simple symbolic model checker for propositional transition system systems.</p> + + + diff --git a/techniques/index.html b/techniques/index.html index 5b570bf..d69f0fb 100644 --- a/techniques/index.html +++ b/techniques/index.html @@ -96,6 +96,24 @@ + + CAR + + + + + + + + + + + + + + + + + + + + + + + PDR + + + diff --git a/techniques/index.xml b/techniques/index.xml index c7fa838..8320d20 100644 --- a/techniques/index.xml +++ b/techniques/index.xml @@ -8,6 +8,13 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + CAR + https://fmtools.fyi/techniques/car/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/techniques/car/ + + CDCL https://fmtools.fyi/techniques/cdcl/ @@ -22,5 +29,12 @@ https://fmtools.fyi/techniques/gpu/ + + PDR + https://fmtools.fyi/techniques/pdr/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/techniques/pdr/ + + diff --git a/techniques/pdr/index.html b/techniques/pdr/index.html new file mode 100644 index 0000000..9c1b0b8 --- /dev/null +++ b/techniques/pdr/index.html @@ -0,0 +1,131 @@ + + + + + + + + +PDR | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + PDR + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
GeyserGeyser is a simple symbolic model checker for propositional transition system systems. +
+ +
+ + + diff --git a/techniques/pdr/index.xml b/techniques/pdr/index.xml new file mode 100644 index 0000000..ecb0cf5 --- /dev/null +++ b/techniques/pdr/index.xml @@ -0,0 +1,19 @@ + + + + PDR on Formal Methods Tools + https://fmtools.fyi/techniques/pdr/ + Recent content in PDR on Formal Methods Tools + Hugo + en-us + Sat, 07 Jun 2025 00:00:00 +0000 + + + Geyser + https://fmtools.fyi/tools/mc/geyser/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/geyser/ + <p>Geyser is a simple symbolic model checker for propositional transition system systems.</p> + + + diff --git a/tools/index.html b/tools/index.html index 0747974..fde6b2e 100644 --- a/tools/index.html +++ b/tools/index.html @@ -93,10 +93,61 @@ Click a colorful item in the"> - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -117,6 +168,34 @@ Click a colorful item in the"> + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -189,6 +268,8 @@ Colors are generated by hashing each term’s name and converting it to RGB
  • Model Checking Tools
  • +
  • Modeling (Tools and Languages)
  • +
  • Probabilistic Tools
  • SAT & SMT Tools
  • @@ -482,6 +563,119 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + +
    + BLAST + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + + + + @@ -755,6 +949,340 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + CADP + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + + + + + + + + + + + + + + Caesar + + + + + + + + + + + + + + + + + + + Probabilistic Program Prover + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + + CGAAL + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + AGPL-v3 + + + + + + + + + + + + + + + + @@ -950,6 +1478,226 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + + + Concuerror + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + + + + + + + + + + + CPAchecker + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + + @@ -1485,6 +2233,116 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + DSCheck + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ISC + + + + + + + + + + + + + + + + @@ -1599,6 +2457,404 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + Eldarica + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSL + + + + + + + + + + + + + + + + + + + + + + + + + + ESBMC + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + BSD 4-clause + + + + + + + + + + + + + MIT + + + + + + + + + + + + + BSD 3-clause + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + + + + + + + + + Geyser + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + @@ -1717,6 +2973,695 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + IMITATOR + + + + + + + + + + + + + + + + + + + Parameter Synthesizer + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + + + + + + + + + ImSpin + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + +
    + Intrepyd + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + + + + + + + + + + + JANI + + + + + + + + + + + + + + + + + + + Modeling Language + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + + Kind 2 + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + + + + + + + + + + + + + + LEAN + + + + + + + + + + + + + + + + + + + Theorem Prover + + + + + + + + + + + + + Modeling Language + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + + + + @@ -1831,6 +3776,200 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + +
    + LTSA + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + LTSmin + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + @@ -1945,6 +4084,313 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + +
    + mcltl-rs + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + mCRL2 + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSL + + + + + + + + + + + + + + + + + + + + + + + + + +
    + Mercury + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + @@ -2062,6 +4508,462 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + Momba + + + + + + + + + + + + + + + + + + + Modeling Framework + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + +
    + MUNTA + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + + NuSMV + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + LGPL + + + + + + + + + + + + + + + + + + + + + + + + + + NuXMV + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + + + + @@ -2306,6 +5208,112 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + Pnmc + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + @@ -2428,6 +5436,150 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + pyPL + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + Model Generator + + + + + + + + + + + + + Theorem Prover + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Unilicense + + + + + + + + + + + + + + + + @@ -2674,6 +5826,226 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + Roméo + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPL + + + + + + + + + + + + + + + + + + + + + + + + + + Rumur + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Unilicense + + + + + + + + + + + + + + + + @@ -2792,6 +6164,116 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + SM(P/)T + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + @@ -3053,6 +6535,226 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + SpaceEx + + + + + + + + + + + + + + + + + + + Hybrid Systems + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + + + + + + + + + Spin + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + + + + @@ -3192,6 +6894,116 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + stateright + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + @@ -3470,6 +7282,488 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + TAPAAL + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Open Source 3.0 + + + + + + + + + + + + + BSD + + + + + + + + + + + + + GPLv2 + + + + + + + + + + + + + + + + + + + + + + + + + +
    + TimeSolver + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + TLA+ + + + + + + + + + + + + + + + + + + + Modeling Language + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Open Source 3.0 + + + + + + + + + + + + + BSD + + + + + + + + + + + + + GPLv2 + + + + + + + + + + + + + + + + + + + + + + + + + + Uppaal + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + + + + diff --git a/tools/mc/blast/index.html b/tools/mc/blast/index.html new file mode 100644 index 0000000..7353318 --- /dev/null +++ b/tools/mc/blast/index.html @@ -0,0 +1,336 @@ + + + + + + + + +BLAST | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + Aalborg University + + + + + + + + + + + + + Uppsala Universitet + + + +
    + + Licenses + + + + + + + + + + + + + Apache-2.0 + + + +
    + + Maintenance + + + + + + + + + + + + + Not Maintained + + + +
    +
    + + +
    +

    Description

    +

    + +

    + + [ + + Not Maintained Since 2012 + + ] +
    +BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/cadp/index.html b/tools/mc/cadp/index.html new file mode 100644 index 0000000..8e016ff --- /dev/null +++ b/tools/mc/cadp/index.html @@ -0,0 +1,311 @@ + + + + + + + + +CADP | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + INRIA Rocquencourt + + + +
    + + Licenses + + + + + + + + + + + + + All Rights Reserved + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    + + [ + Closed-Source Tool + +
    +CADP (“Construction and Analysis of Distributed Processes”, formerly known as “CAESAR/ALDEBARAN Development Package”) is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/cgaal/index.html b/tools/mc/cgaal/index.html new file mode 100644 index 0000000..2f4b0b7 --- /dev/null +++ b/tools/mc/cgaal/index.html @@ -0,0 +1,267 @@ + + + + + + + + +CGAAL | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Licenses + + + + + + + + + + + + + AGPL-v3 + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/concuerror/index.html b/tools/mc/concuerror/index.html new file mode 100644 index 0000000..0679133 --- /dev/null +++ b/tools/mc/concuerror/index.html @@ -0,0 +1,299 @@ + + + + + + + + +Concuerror | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + Uppsala University + + + +
    + + Licenses + + + + + + + + + + + + + BSD + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    Concuerror is a stateless model checking tool for Erlang programs.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/cpachecker/index.html b/tools/mc/cpachecker/index.html new file mode 100644 index 0000000..ec7d9d0 --- /dev/null +++ b/tools/mc/cpachecker/index.html @@ -0,0 +1,311 @@ + + + + + + + + +CPAchecker | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + Ludwig-Maximilians-Universität München + + + +
    + + Licenses + + + + + + + + + + + + + Apache-2.0 + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    + + [ + Closed-Source Tool + +
    +CPAchecker is a tool for configurable software verification.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/dscheck/index.html b/tools/mc/dscheck/index.html new file mode 100644 index 0000000..ea4d126 --- /dev/null +++ b/tools/mc/dscheck/index.html @@ -0,0 +1,297 @@ + + + + + + + + +DSCheck | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + University of Twente + + + +
    + + Licenses + + + + + + + + + + + + + ISC + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    DSCheck is an experimental model checker for testing concurrent OCaml programs.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/eldarica/index.html b/tools/mc/eldarica/index.html new file mode 100644 index 0000000..cafc8cc --- /dev/null +++ b/tools/mc/eldarica/index.html @@ -0,0 +1,297 @@ + + + + + + + + +Eldarica | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + Uppsala University + + + +
    + + Licenses + + + + + + + + + + + + + BSL + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/esbmc/index.html b/tools/mc/esbmc/index.html new file mode 100644 index 0000000..5368dd2 --- /dev/null +++ b/tools/mc/esbmc/index.html @@ -0,0 +1,435 @@ + + + + + + + + +ESBMC | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + Federal University of Amazonas + + + + + + + + + + + + + University of Bristol + + + + + + + + + + + + + University of Manchester + + + + + + + + + + + + + University of Southampton + + + + + + + + + + + + + University of Stellenbosch + + + +
    + + Licenses + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + BSD 3-clause + + + + + + + + + + + + + BSD 4-clause + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + MIT + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/geyser/index.html b/tools/mc/geyser/index.html new file mode 100644 index 0000000..c2e2c21 --- /dev/null +++ b/tools/mc/geyser/index.html @@ -0,0 +1,314 @@ + + + + + + + + +Geyser | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Licenses + + + + + + + + + + + + + MIT + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    + + Techniques + + + + + + + + + + + + + CAR + + + + + + + + + + + + + PDR + + + +
    +
    + + +
    +

    Description

    +

    Geyser is a simple symbolic model checker for propositional transition system systems.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/imitator/index.html b/tools/mc/imitator/index.html new file mode 100644 index 0000000..5361168 --- /dev/null +++ b/tools/mc/imitator/index.html @@ -0,0 +1,299 @@ + + + + + + + + +IMITATOR | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Parameter Synthesizer + + + +
    + + Developers + + + + + + + + + + + + + Universite Sorbonne Paris Nord + + + +
    + + Licenses + + + + + + + + + + + + + GPLv3 + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/imspin/index.html b/tools/mc/imspin/index.html new file mode 100644 index 0000000..5b11226 --- /dev/null +++ b/tools/mc/imspin/index.html @@ -0,0 +1,267 @@ + + + + + + + + +ImSpin | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Licenses + + + + + + + + + + + + + MIT + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    ImSpin is a frontend for the SPIN model checker, providing an environment for users engaged in model checking tasks.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/index.html b/tools/mc/index.html index 2de57c4..3148bf0 100644 --- a/tools/mc/index.html +++ b/tools/mc/index.html @@ -92,6 +92,134 @@ Click a colorful"> + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -119,6 +247,2798 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + +
    + BLAST + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + + + + + + + + + + + + + + CADP + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + + + + + + + + + + + + + + CGAAL + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + AGPL-v3 + + + + + + + + + + + + + + + + + + + + + + + + + + Concuerror + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + + + + + + + + + + + CPAchecker + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + + + + + + + + + + + + + + DSCheck + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ISC + + + + + + + + + + + + + + + + + + + + + + + + + + Eldarica + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSL + + + + + + + + + + + + + + + + + + + + + + + + + + ESBMC + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + BSD 4-clause + + + + + + + + + + + + + MIT + + + + + + + + + + + + + BSD 3-clause + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + + + + + + + + + Geyser + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + + + + IMITATOR + + + + + + + + + + + + + + + + + + + Parameter Synthesizer + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + + + + + + + + + ImSpin + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + +
    + Intrepyd + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + + + + + + + + + + + Kind 2 + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + + + + + + + + + + + + + +
    + LTSA + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + LTSmin + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + + + + + + + + + + +
    + mcltl-rs + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + mCRL2 + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSL + + + + + + + + + + + + + + + + + + + + + + + + + +
    + Mercury + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + +
    + MUNTA + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + + NuSMV + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + LGPL + + + + + + + + + + + + + + + + + + + + + + + + + + NuXMV + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + + + + + + + + + + + + + + Pnmc + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + + + + + + + + + + + pyPL + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + Model Generator + + + + + + + + + + + + + Theorem Prover + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Unilicense + + + + + + + + + + + + + + + + + + + + + + + + + + Roméo + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPL + + + + + + + + + + + + + + + + + + + + + + + + + + Rumur + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Unilicense + + + + + + + + + + + + + + + + + + + + + @@ -232,6 +3152,784 @@ Colors are generated by hashing each term’s name and converting it to RGB + + + + + + + + + + SM(P/)T + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + + + + + + + + + SpaceEx + + + + + + + + + + + + + + + + + + + Hybrid Systems + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + + + + + + + + + Spin + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + + + + + + + + + + + + + + stateright + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + + + + + + + + + TAPAAL + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Open Source 3.0 + + + + + + + + + + + + + BSD + + + + + + + + + + + + + GPLv2 + + + + + + + + + + + + + + + + + + + + + + + + + +
    + TimeSolver + +
    + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Uppaal + + + + + + + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + + + + diff --git a/tools/mc/index.xml b/tools/mc/index.xml index 62b0103..6a2d346 100644 --- a/tools/mc/index.xml +++ b/tools/mc/index.xml @@ -8,6 +8,181 @@ en-us Sat, 07 Jun 2025 00:00:00 +0000 + + BLAST + https://fmtools.fyi/tools/mc/blast/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/blast/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2012</span> <span style="display:none">]</span> </div> BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.</p> + + + CADP + https://fmtools.fyi/tools/mc/cadp/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cadp/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CADP (&ldquo;Construction and Analysis of Distributed Processes&rdquo;, formerly known as &ldquo;CAESAR/ALDEBARAN Development Package&rdquo;) is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.</p> + + + CGAAL + https://fmtools.fyi/tools/mc/cgaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cgaal/ + <p>CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).</p> + + + Concuerror + https://fmtools.fyi/tools/mc/concuerror/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/concuerror/ + <p>Concuerror is a stateless model checking tool for Erlang programs.</p> + + + CPAchecker + https://fmtools.fyi/tools/mc/cpachecker/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/cpachecker/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> CPAchecker is a tool for configurable software verification.</p> + + + DSCheck + https://fmtools.fyi/tools/mc/dscheck/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/dscheck/ + <p>DSCheck is an experimental model checker for testing concurrent OCaml programs.</p> + + + Eldarica + https://fmtools.fyi/tools/mc/eldarica/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/eldarica/ + <p>Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.</p> + + + ESBMC + https://fmtools.fyi/tools/mc/esbmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/esbmc/ + <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p> + + + Geyser + https://fmtools.fyi/tools/mc/geyser/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/geyser/ + <p>Geyser is a simple symbolic model checker for propositional transition system systems.</p> + + + IMITATOR + https://fmtools.fyi/tools/mc/imitator/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/imitator/ + <p>IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.</p> + + + ImSpin + https://fmtools.fyi/tools/mc/imspin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/imspin/ + <p>ImSpin is a frontend for the <a href="../spin" >SPIN</a> model checker, providing an environment for users engaged in model checking tasks.</p> + + + Intrepyd + https://fmtools.fyi/tools/mc/intrepyd/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/intrepyd/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> Intrepyd is a python module that provides a simulator and a model checker in form of a rich API, to allow the rapid prototyping of formal methods algorithms for the rigorous analysis of circuits, specifications, models.</p> + + + Kind 2 + https://fmtools.fyi/tools/mc/kind2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/kind2/ + <p>Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.</p> + + + LTSA + https://fmtools.fyi/tools/mc/ltsa/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/ltsa/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2018</span> <span style="display:none">]</span> </div> LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour.</p> + + + LTSmin + https://fmtools.fyi/tools/mc/ltsmin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/ltsmin/ + <p>LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.</p> + + + mcltl-rs + https://fmtools.fyi/tools/mc/mcltlrs/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mcltlrs/ + <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> <p>mcltl-rs is an experimental model checker for LTL written in Rust.</p> + + + mCRL2 + https://fmtools.fyi/tools/mc/mcrl2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mcrl2/ + <p>mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.</p> + + + Mercury + https://fmtools.fyi/tools/mc/mercury/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/mercury/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.</p> + + + MUNTA + https://fmtools.fyi/tools/mc/munta/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/munta/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span> <span style="display:none">]</span> </div> MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata</p> + + + NuSMV + https://fmtools.fyi/tools/mc/nusmv/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/nusmv/ + <p>NuSMV is a symbolic model checker.</p> + + + NuXMV + https://fmtools.fyi/tools/mc/nuxmv/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/nuxmv/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.</p> + + + Pnmc + https://fmtools.fyi/tools/mc/pnmc/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/pnmc/ + <p>Pnmc is a symbolic model checker for Petri nets.</p> + + + pyPL + https://fmtools.fyi/tools/mc/pypl/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/pypl/ + <p>pyPL is a naive model generator, model checker and theorem prover.</p> + + + Roméo + https://fmtools.fyi/tools/mc/romeo/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/romeo/ + <p>Romeo allows the modelling of complex systems using extensions of time Petri nets.</p> + + + Rumur + https://fmtools.fyi/tools/mc/rumur/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/rumur/ + <p>Rumur is a model checker.</p> + Sally https://fmtools.fyi/tools/mc/sally/ @@ -15,5 +190,54 @@ https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> + + SM(P/)T + https://fmtools.fyi/tools/mc/smpt/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/smpt/ + <p>SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).</p> + + + SpaceEx + https://fmtools.fyi/tools/mc/spaceex/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/spaceex/ + <p>The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.</p> + + + Spin + https://fmtools.fyi/tools/mc/spin/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/spin/ + <p>Spin is a model checker for multi-threaded software.</p> + + + stateright + https://fmtools.fyi/tools/mc/stateright/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/stateright/ + <p><code>stateright</code> is a Rust library for model checking systems, with an emphasis on distributed systems.</p> + + + TAPAAL + https://fmtools.fyi/tools/mc/tapaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/tapaal/ + <p>TAPAAL is a tool for verification of timed-arc petri nets</p> + + + TimeSolver + https://fmtools.fyi/tools/mc/timesolver/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/timesolver/ + <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2019</span> <span style="display:none">]</span> </div> TimeSolver is a Model Checker for timed automata that uses pes (predicate equation systems).</p> + + + Uppaal + https://fmtools.fyi/tools/mc/uppaal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://fmtools.fyi/tools/mc/uppaal/ + <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).</p> + diff --git a/tools/mc/intrepyd/index.html b/tools/mc/intrepyd/index.html new file mode 100644 index 0000000..5283fbc --- /dev/null +++ b/tools/mc/intrepyd/index.html @@ -0,0 +1,287 @@ + + + + + + + + +Intrepyd | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Licenses + + + + + + + + + + + + + BSD + + + +
    + + Maintenance + + + + + + + + + + + + + Not Maintained + + + +
    +
    + + +
    +

    Description

    +

    + +

    + + [ + + Not Maintained Since 2021 + + ] +
    +Intrepyd is a python module that provides a simulator and a model checker in form of a rich API, to allow the rapid prototyping of formal methods algorithms for the rigorous analysis of circuits, specifications, models.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/kind2/index.html b/tools/mc/kind2/index.html new file mode 100644 index 0000000..c48589d --- /dev/null +++ b/tools/mc/kind2/index.html @@ -0,0 +1,299 @@ + + + + + + + + +Kind 2 | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + University of Iowa + + + +
    + + Licenses + + + + + + + + + + + + + Apache-2.0 + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/ltsa/index.html b/tools/mc/ltsa/index.html new file mode 100644 index 0000000..6ad9466 --- /dev/null +++ b/tools/mc/ltsa/index.html @@ -0,0 +1,257 @@ + + + + + + + + +LTSA | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Maintenance + + + + + + + + + + + + + Not Maintained + + + +
    +
    + + +
    +

    Description

    +

    + +

    + + [ + + Not Maintained Since 2018 + + ] +
    +LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/ltsmin/index.html b/tools/mc/ltsmin/index.html new file mode 100644 index 0000000..10d6908 --- /dev/null +++ b/tools/mc/ltsmin/index.html @@ -0,0 +1,299 @@ + + + + + + + + +LTSmin | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + University of Twente + + + +
    + + Licenses + + + + + + + + + + + + + BSD + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/mcltlrs/index.html b/tools/mc/mcltlrs/index.html new file mode 100644 index 0000000..405dc6b --- /dev/null +++ b/tools/mc/mcltlrs/index.html @@ -0,0 +1,255 @@ + + + + + + + + +mcltl-rs | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Maintenance + + + + + + + + + + + + + Not Maintained + + + +
    +
    + + +
    +

    Description

    + + +
    + + [ + + Not Maintained Since 2020 + + ] +
    +

    mcltl-rs is an experimental model checker for LTL written in Rust.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/mcrl2/index.html b/tools/mc/mcrl2/index.html new file mode 100644 index 0000000..3fafb8f --- /dev/null +++ b/tools/mc/mcrl2/index.html @@ -0,0 +1,299 @@ + + + + + + + + +mCRL2 | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + Eindhoven University of Technology + + + +
    + + Licenses + + + + + + + + + + + + + BSL + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/mercury/index.html b/tools/mc/mercury/index.html new file mode 100644 index 0000000..1407450 --- /dev/null +++ b/tools/mc/mercury/index.html @@ -0,0 +1,334 @@ + + + + + + + + +Mercury | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + LAAS-CNRS + + + + + + + + + + + + + Vertics + + + +
    + + Licenses + + + + + + + + + + + + + MIT + + + +
    + + Maintenance + + + + + + + + + + + + + Not Maintained + + + +
    +
    + + +
    +

    Description

    +

    + +

    + + [ + + Not Maintained Since 2020 + + ] +
    +Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/munta/index.html b/tools/mc/munta/index.html new file mode 100644 index 0000000..fc89fd7 --- /dev/null +++ b/tools/mc/munta/index.html @@ -0,0 +1,287 @@ + + + + + + + + +MUNTA | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Licenses + + + + + + + + + + + + + MIT + + + +
    + + Maintenance + + + + + + + + + + + + + Not Maintained + + + +
    +
    + + +
    +

    Description

    +

    + +

    + + [ + + Not Maintained Since 2020 + + ] +
    +MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/nusmv/index.html b/tools/mc/nusmv/index.html new file mode 100644 index 0000000..f6e118f --- /dev/null +++ b/tools/mc/nusmv/index.html @@ -0,0 +1,297 @@ + + + + + + + + +NuSMV | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + Fondazione Bruno Kessler + + + +
    + + Licenses + + + + + + + + + + + + + LGPL + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    NuSMV is a symbolic model checker.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/nuxmv/index.html b/tools/mc/nuxmv/index.html new file mode 100644 index 0000000..a085089 --- /dev/null +++ b/tools/mc/nuxmv/index.html @@ -0,0 +1,309 @@ + + + + + + + + +NuXMV | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + Fondazione Bruno Kessler + + + +
    + + Licenses + + + + + + + + + + + + + All Rights Reserved + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    + + [ + Closed-Source Tool + +
    +nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/pnmc/index.html b/tools/mc/pnmc/index.html new file mode 100644 index 0000000..5961a27 --- /dev/null +++ b/tools/mc/pnmc/index.html @@ -0,0 +1,267 @@ + + + + + + + + +Pnmc | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Licenses + + + + + + + + + + + + + BSD + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    Pnmc is a symbolic model checker for Petri nets.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/pypl/index.html b/tools/mc/pypl/index.html new file mode 100644 index 0000000..e79fe88 --- /dev/null +++ b/tools/mc/pypl/index.html @@ -0,0 +1,331 @@ + + + + + + + + +pyPL | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + + + + + + + + + + + Model Generator + + + + + + + + + + + + + Theorem Prover + + + +
    + + Developers + + + + + + + + + + + + + Matthew Fernandez + + + +
    + + Licenses + + + + + + + + + + + + + Unilicense + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    pyPL is a naive model generator, model checker and theorem prover.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/romeo/index.html b/tools/mc/romeo/index.html new file mode 100644 index 0000000..6ad6f67 --- /dev/null +++ b/tools/mc/romeo/index.html @@ -0,0 +1,297 @@ + + + + + + + + +Roméo | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + University of Nantes + + + +
    + + Licenses + + + + + + + + + + + + + GPL + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    Romeo allows the modelling of complex systems using extensions of time Petri nets.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/rumur/index.html b/tools/mc/rumur/index.html new file mode 100644 index 0000000..0cb6d8d --- /dev/null +++ b/tools/mc/rumur/index.html @@ -0,0 +1,297 @@ + + + + + + + + +Rumur | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    +

    Formal Methods Tools

    + + + + +
    +
    + + + + + +
    +

    At a Glance

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + + Applications + + + + + + + + + + + + + Model Checker + + + +
    + + Developers + + + + + + + + + + + + + Matthew Fernandez + + + +
    + + Licenses + + + + + + + + + + + + + Unilicense + + + +
    + + Maintenance + + + + + + + + + + + + + Actively Maintained + + + +
    +
    + + +
    +

    Description

    +

    Rumur is a model checker.

    + +
    + + + + +
    + + + + +
    + + + +
    + + + diff --git a/tools/mc/sally/index.html b/tools/mc/sally/index.html index d4fec86..bdc87fd 100644 --- a/tools/mc/sally/index.html +++ b/tools/mc/sally/index.html @@ -86,7 +86,7 @@ -MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.

    +MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).