Merge branch 'main' of https://gitmoss.fyi/fmtools/content

.gitea/issue_template/add_tool.md

@@ -7,6 +7,8 @@ assignees: ["mossbiscuits"]
 labels:
 - "new tool"
 - "enhancement"
+projects:
+- "Tool Collection"
 ---
 
 Fill in as little or as much information as you like, but more information increases my ability to add your tool effectively.

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.

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.

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.

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. 

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 = ['']
++++
+
+{{<inactive year="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.

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.

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.

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 = ['']
++++
+
+{{<inactive year="2020">}}
+MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata

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.

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.

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'  },

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).