From a591cca1cd7aa8fd4feb58a74774453b055865e4 Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Fri, 13 Jun 2025 16:46:24 -0600 Subject: [PATCH] partial work toward #2 --- tools/mc/concuerror.md | 21 +++++++++++++++++++++ tools/mc/dscheck.md | 21 +++++++++++++++++++++ tools/mc/eldarica.md | 21 +++++++++++++++++++++ tools/mc/imitator.md | 21 +++++++++++++++++++++ tools/mc/intrepyd.md | 22 ++++++++++++++++++++++ tools/mc/ltsmin.md | 21 +++++++++++++++++++++ tools/mc/mcrl2.md | 21 +++++++++++++++++++++ tools/mc/munta.md | 22 ++++++++++++++++++++++ tools/mc/pypl.md | 21 +++++++++++++++++++++ tools/mc/rumur.md | 21 +++++++++++++++++++++ tools/mc/sally.md | 2 +- tools/mc/smpt.md | 21 +++++++++++++++++++++ 12 files changed, 234 insertions(+), 1 deletion(-) create mode 100644 tools/mc/concuerror.md create mode 100644 tools/mc/dscheck.md create mode 100644 tools/mc/eldarica.md create mode 100644 tools/mc/imitator.md create mode 100644 tools/mc/intrepyd.md create mode 100644 tools/mc/ltsmin.md create mode 100644 tools/mc/mcrl2.md create mode 100644 tools/mc/munta.md create mode 100644 tools/mc/pypl.md create mode 100644 tools/mc/rumur.md create mode 100644 tools/mc/smpt.md diff --git a/tools/mc/concuerror.md b/tools/mc/concuerror.md new file mode 100644 index 0000000..f66b760 --- /dev/null +++ b/tools/mc/concuerror.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Concuerror' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "http://parapluu.github.io/Concuerror", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/parapluu/Concuerror", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Uppsala University'] +licenses = ['BSD'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +Concuerror is a stateless model checking tool for Erlang programs. \ No newline at end of file diff --git a/tools/mc/dscheck.md b/tools/mc/dscheck.md new file mode 100644 index 0000000..26df5c4 --- /dev/null +++ b/tools/mc/dscheck.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'DSCheck' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/ocaml-multicore/dscheck", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['University of Twente'] +licenses = ['ISC'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +DSCheck is an experimental model checker for testing concurrent OCaml programs. \ No newline at end of file diff --git a/tools/mc/eldarica.md b/tools/mc/eldarica.md new file mode 100644 index 0000000..dba1a13 --- /dev/null +++ b/tools/mc/eldarica.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Eldarica' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/uuverifiers/eldarica", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Uppsala University'] +licenses = ['BSL'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs. \ No newline at end of file diff --git a/tools/mc/imitator.md b/tools/mc/imitator.md new file mode 100644 index 0000000..2761e71 --- /dev/null +++ b/tools/mc/imitator.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'IMITATOR' +subtitle = 'Parameter Synthesis' +links = [ + { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/imitator-model-checker/imitator", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Parameter Synthesizer'] +developers = ['Universite Sorbonne Paris Nord'] +licenses = ['GPLv3'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more. \ No newline at end of file diff --git a/tools/mc/intrepyd.md b/tools/mc/intrepyd.md new file mode 100644 index 0000000..9a5e40a --- /dev/null +++ b/tools/mc/intrepyd.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Intrepyd' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/formalmethods/intrepid", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +# developers = [''] +licenses = ['BSD'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +{{}} +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. \ No newline at end of file diff --git a/tools/mc/ltsmin.md b/tools/mc/ltsmin.md new file mode 100644 index 0000000..816a833 --- /dev/null +++ b/tools/mc/ltsmin.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'LTSmin' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/utwente-fmt/ltsmin", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['University of Twente'] +licenses = ['BSD'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +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. \ No newline at end of file diff --git a/tools/mc/mcrl2.md b/tools/mc/mcrl2.md new file mode 100644 index 0000000..a5e2028 --- /dev/null +++ b/tools/mc/mcrl2.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'mCRL2' +subtitle = 'Model Checker' +links = [ + { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/mCRL2org/mCRL2", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Eindhoven University of Technology'] +licenses = ['BSL'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +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. \ No newline at end of file diff --git a/tools/mc/munta.md b/tools/mc/munta.md new file mode 100644 index 0000000..fe6cc9c --- /dev/null +++ b/tools/mc/munta.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'MUNTA' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/wimmers/munta", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +# developers = [''] +licenses = ['MIT'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +{{}} +MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata \ No newline at end of file diff --git a/tools/mc/pypl.md b/tools/mc/pypl.md new file mode 100644 index 0000000..a392c52 --- /dev/null +++ b/tools/mc/pypl.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'pyPL' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/nclarius/pyPL", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker', 'Model Generator', 'Theorem Prover'] +developers = ['Matthew Fernandez'] +licenses = ['Unilicense'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +pyPL is a naive model generator, model checker and theorem prover. \ No newline at end of file diff --git a/tools/mc/rumur.md b/tools/mc/rumur.md new file mode 100644 index 0000000..675562a --- /dev/null +++ b/tools/mc/rumur.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Rumur' +subtitle = 'Model Checker' +links = [ + # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/Smattr/rumur", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['Matthew Fernandez'] +licenses = ['Unilicense'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +Rumur is a model checker. \ No newline at end of file diff --git a/tools/mc/sally.md b/tools/mc/sally.md index d0b2fbf..5eba793 100644 --- a/tools/mc/sally.md +++ b/tools/mc/sally.md @@ -2,7 +2,7 @@ date = 2025-06-07 draft = false title = 'Sally' -subtitle = 'Probabilistic Model Checker' +subtitle = 'Model Checker' links = [ { title = "Homepage", url = "http://sri-csl.github.io/sally/", icon = 'fa-solid fa-home' }, { title = "Source Code", url = "https://github.com/SRI-CSL/sally", icon = 'fa-brands fa-github' }, diff --git a/tools/mc/smpt.md b/tools/mc/smpt.md new file mode 100644 index 0000000..a1ef830 --- /dev/null +++ b/tools/mc/smpt.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'SM(P/)T' +subtitle = 'Satisfiability Modulo Petri Net' +links = [ + # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/nicolasAmat/SMPT", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker'] +developers = ['LAAS-CNRS'] +licenses = ['GPLv3'] +# inputs = ['Sally'] +# interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + +SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions). \ No newline at end of file