fmtools/content
1
0
Fork 0
Code Issues 20 Pull Requests Actions Packages Releases Wiki Activity

partial work toward #2

Browse Source
This commit is contained in:
Landon Taylor
2025-06-13 16:46:24 -06:00
parent b6cc09e6e1
commit a591cca1cd
12 changed files with 234 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

21
tools/mc/concuerror.md Normal file
View File

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

21
tools/mc/dscheck.md Normal file
View File

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

21
tools/mc/eldarica.md Normal file
View File

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

21
tools/mc/imitator.md Normal file
View File

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

22
tools/mc/intrepyd.md Normal file
View File

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

21
tools/mc/ltsmin.md Normal file
View File

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

21
tools/mc/mcrl2.md Normal file
View File

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

22
tools/mc/munta.md Normal file
View File

@@ -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

21
tools/mc/pypl.md Normal file
View File

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

21
tools/mc/rumur.md Normal file
View File

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

2
tools/mc/sally.md
View File

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

21
tools/mc/smpt.md Normal file
View File

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