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

Add model checkers. Close #2

Browse Source
This commit is contained in:
Landon Taylor
2025-06-23 13:44:10 -06:00
parent 2545c47377
commit 67276e8e46
21 changed files with 450 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'BLAST'
subtitle = 'Model Checker'
links = [
{ title = "Homepage", url = "https://forge.ispras.ru/projects/blast", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['Uppsala Universitet', 'Aalborg University']
licenses = ['Apache-2.0']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Not Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
{{<inactive year="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.

23
tools/mc/cadp.md Normal file
View File

@@ -0,0 +1,23 @@
+++
date = 2025-06-07
draft = false
title = 'CADP'
subtitle = 'Model Checker'
links = [
{ title = "Homepage", url = "https://cadp.inria.fr/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['INRIA Rocquencourt']
licenses = ['All Rights Reserved']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
<!-- {{<inactive year="2012">}} -->
{{<closed-source>}}
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.

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

@@ -0,0 +1,21 @@
+++
date = 2025-06-07
draft = false
title = 'CGAAL'
subtitle = 'Model Checker'
links = [
# { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/d702e20/CGAAL", 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 = ['AGPL-v3']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).

23
tools/mc/cpachecker.md Normal file
View File

@@ -0,0 +1,23 @@
+++
date = 2025-06-07
draft = false
title = 'CPAchecker'
subtitle = 'Model Checker'
links = [
{ title = "Homepage", url = "https://cpachecker.sosy-lab.org/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://gitlab.com/sosy-lab/software/cpachecker/", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['Ludwig-Maximilians-Universität München']
licenses = ['Apache-2.0']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
<!-- {{<inactive year="2012">}} -->
{{<closed-source>}}
CPAchecker is a tool for configurable software verification.

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

@@ -0,0 +1,21 @@
+++
date = 2025-06-07
draft = false
title = 'ESBMC'
subtitle = 'Model Checker'
links = [
{ title = "Homepage", url = "https://ssvlab.github.io/esbmc/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/esbmc/esbmc", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['Federal University of Amazonas', 'University of Bristol', 'University of Manchester', 'University of Stellenbosch', 'University of Southampton']
licenses = ['Apache-2.0', 'BSD 4-clause', 'MIT', 'BSD 3-clause', 'GPLv3', ]
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.

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

@@ -0,0 +1,21 @@
+++
date = 2025-06-07
draft = false
title = 'Geyser'
subtitle = 'Model Checker'
links = [
# { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/JakubSarnik/geyser", 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 = ['MIT']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
techniques = ['PDR', 'CAR']
# publications = ['']
+++
Geyser is a simple symbolic model checker for propositional transition system systems.

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

@@ -0,0 +1,21 @@
+++
date = 2025-06-07
draft = false
title = 'ImSpin'
subtitle = 'Model Checker'
links = [
# { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/MrDiver/ImSpin", 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 = ['MIT']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['PDR', 'CAR']
# publications = ['']
+++
ImSpin is a frontend for the [SPIN](../spin) model checker, providing an environment for users engaged in model checking tasks.

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

@@ -0,0 +1,21 @@
+++
date = 2025-06-07
draft = false
title = 'Kind 2'
subtitle = 'Model Checker'
links = [
{ title = "Homepage", url = "https://kind2-mc.github.io/kind2/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/kind2-mc/kind2", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['University of Iowa']
licenses = ['Apache-2.0']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.

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

@@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'LTSA'
subtitle = 'Labelled Transition System Analyser'
links = [
{ title = "Homepage", url = "https://www.doc.ic.ac.uk/ltsa/", icon = 'fa-solid fa-home' },
# { title = "Source Code", url = "https://github.com/ahamez/pnmc", 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 = ['Not Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
{{<inactive year="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.

23
tools/mc/mcltlrs.md Normal file
View File

@@ -0,0 +1,23 @@
+++
date = 2025-06-07
draft = false
title = 'mcltl-rs'
subtitle = 'Model Checker'
links = [
# { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/NotBad4U/mcltl-rs", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
# developers = ['Fondazione Bruno Kessler']
# licenses = ['All Rights Reserved']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Not Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
{{<inactive year="2020">}}
<!-- {{<closed-source>}} -->
mcltl-rs is an experimental model checker for LTL written in Rust.

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

@@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'Mercury'
subtitle = 'Model Checker'
links = [
# { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/rtsaad/mercury", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['LAAS-CNRS', 'Vertics']
licenses = ['MIT']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Not Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
{{<inactive year="2020">}}
Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.

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

@@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'NuSMV'
subtitle = 'Symbolic Model Checker'
links = [
{ title = "Homepage", url = "https://nusmv.fbk.eu/index.html", icon = 'fa-solid fa-home' },
# { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['Fondazione Bruno Kessler']
licenses = ['LGPL']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
<!-- {{<inactive year="2018">}} -->
NuSMV is a symbolic model checker.

23
tools/mc/nuxmv.md Normal file
View File

@@ -0,0 +1,23 @@
+++
date = 2025-06-07
draft = false
title = 'NuXMV'
subtitle = 'Symbolic Model Checker'
links = [
{ title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' },
# { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['Fondazione Bruno Kessler']
licenses = ['All Rights Reserved']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
<!-- {{<inactive year="2018">}} -->
{{<closed-source>}}
nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.

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

@@ -0,0 +1,21 @@
+++
date = 2025-06-07
draft = false
title = 'Pnmc'
subtitle = 'Model Checker'
links = [
# { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/ahamez/pnmc", 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 = ['']
+++
Pnmc is a symbolic model checker for Petri nets.

23
tools/mc/romeo.md Normal file
View File

@@ -0,0 +1,23 @@
+++
date = 2025-06-07
draft = false
title = 'Roméo'
subtitle = 'Model Checker'
links = [
{ title = "Homepage", url = "https://romeo.ls2n.fr/", icon = 'fa-solid fa-home' },
# { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['University of Nantes']
licenses = ['GPL']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
<!-- {{<inactive year="2018">}} -->
<!-- {{<closed-source>}} -->
Romeo allows the modelling of complex systems using extensions of time Petri nets.

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

@@ -0,0 +1,21 @@
+++
date = 2025-06-07
draft = false
title = 'Spin'
subtitle = 'Model Checker'
links = [
{ title = "Homepage", url = "https://spinroot.com/spin/whatispin.html", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/nimble-code/Spin", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['Bell Labs']
licenses = ['All Rights Reserved']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['PDR', 'CAR']
# publications = ['']
+++
Spin is a model checker for multi-threaded software.

23
tools/mc/tapaal.md Normal file
View File

@@ -0,0 +1,23 @@
+++
date = 2025-06-07
draft = false
title = 'TAPAAL'
subtitle = 'Model Checker'
links = [
{ title = "Homepage", url = "https://www.tapaal.net/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/TAPAAL/", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
developers = ['Aalborg University']
licenses = ['Open Source 3.0', 'BSD', 'GPLv2']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
<!-- {{<inactive year="2012">}} -->
<!-- {{<closed-source>}} -->
TAPAAL is a tool for verification of timed-arc petri nets

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

@@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'TimeSolver'
subtitle = 'Model Checker'
links = [
# { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/jkeiren/TimeSolver", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
]
applications = ['Model Checker']
# developers = ['Fondazione Bruno Kessler']
# licenses = ['All Rights Reserved']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Not Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
{{<inactive year="2019">}}
TimeSolver is a Model Checker for timed automata that uses pes (predicate equation systems).

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

@@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'Uppaal'
subtitle = 'Model Checker'
links = [
{ title = "Homepage", url = "https://uppaal.org/", 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 = ['Model Checker']
developers = ['Uppsala Universitet', 'Aalborg University']
licenses = ['All Rights Reserved']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['']
+++
{{<closed-source>}}
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.).