MrDiver/ImSpin

ImSpin is an advanced and modernized version of the classic iSpin frontend, leveraging the power and flexibility of ImGui to provide a superior user experience. Designed as the frontend for the SPIN model checker, ImSpin aims to offer an intuitive, efficient, and visually appealing interface for model checking enthusiasts and professionals.

Language: C++ - Size: 7.65 MB - Last synced: about 7 hours ago - Pushed: about 9 hours ago - Stars: 0 - Forks: 0

Smattr/rumur

yet another model checker

Language: C++ - Size: 3.4 MB - Last synced: about 14 hours ago - Pushed: about 16 hours ago - Stars: 12 - Forks: 5

nclarius/pyPL

Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions

Language: Python - Size: 5.77 MB - Last synced: 3 days ago - Pushed: 4 days ago - Stars: 18 - Forks: 2

moves-rwth/storm

A Modern Probabilistic Model Checker

Language: C++ - Size: 199 MB - Last synced: 12 days ago - Pushed: 12 days ago - Stars: 124 - Forks: 71

mCRL2org/mCRL2

The Git repository for the mCRL2 toolset.

Language: C++ - Size: 101 MB - Last synced: 13 days ago - Pushed: 13 days ago - Stars: 84 - Forks: 36

parapluu/Concuerror

Concuerror is a stateless model checking tool for Erlang programs.

Language: Erlang - Size: 10.5 MB - Last synced: 18 days ago - Pushed: 18 days ago - Stars: 329 - Forks: 43

uuverifiers/eldarica

The Eldarica model checker

Language: Scala - Size: 53.5 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 75 - Forks: 21

imitator-model-checker/imitator

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

Language: OCaml - Size: 50 MB - Last synced: 3 days ago - Pushed: 4 days ago - Stars: 26 - Forks: 12

stateright/stateright

A model checker for implementing distributed systems.

Language: Rust - Size: 2.69 MB - Last synced: 2 months ago - Pushed: 2 months ago - Stars: 1,510 - Forks: 53

yylonly/LTSA

Real-time System Modeling and Verification through Labeled Transition System Analyser (LTSA)

Language: Visual Basic - Size: 5.42 MB - Last synced: about 2 months ago - Pushed: over 5 years ago - Stars: 3 - Forks: 4

ocaml-multicore/dscheck

Experimental model checker for testing concurrent algorithms

Language: OCaml - Size: 116 KB - Last synced: about 1 month ago - Pushed: 3 months ago - Stars: 29 - Forks: 5

formalmethods/intrepid

Intrepyd Model Checker

Language: Python - Size: 147 MB - Last synced: 29 days ago - Pushed: over 2 years ago - Stars: 17 - Forks: 1

juliendelplanque/DatabaseCritics

A tool to run critics on SQL database schema dumps.

Language: Smalltalk - Size: 495 KB - Last synced: 2 months ago - Pushed: about 6 years ago - Stars: 0 - Forks: 0

utwente-fmt/ltsmin

The LTSmin model checking toolset

Language: C - Size: 7.22 MB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 49 - Forks: 30

phagenlocher/braincheck

A static and dynamic analyzer for Brainfuck

Language: C++ - Size: 46.9 KB - Last synced: about 1 month ago - Pushed: 10 months ago - Stars: 1 - Forks: 0

koehlma/momba

A toolbox for dealing with formal models from construction to analysis based on the JANI-model interchange format.

Language: PDDL - Size: 27.6 MB - Last synced: 20 days ago - Pushed: 4 months ago - Stars: 18 - Forks: 3

d702e20/CGAAL

An on-the-fly, multi-threaded ATL model checker on concurrent game structures

Language: Rust - Size: 33.5 MB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 8 - Forks: 1

ahamez/pnmc

An efficient Petri net model checker using Hierarchical Set Decision Diagrams.

Language: C++ - Size: 1.29 MB - Last synced: about 1 month ago - Pushed: 6 months ago - Stars: 9 - Forks: 2

SRI-CSL/sally

A model checker for infinite-state systems.

Language: C++ - Size: 5.6 MB - Last synced: 6 months ago - Pushed: almost 3 years ago - Stars: 68 - Forks: 12

nicolasAmat/SMPT

SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).

Language: Python - Size: 8.91 MB - Last synced: 7 months ago - Pushed: 7 months ago - Stars: 25 - Forks: 4

jkeiren/TimeSolver

On-the-fly model checker for timed automata with support for the alternation-free modal mu-calculus.

Language: C++ - Size: 63.4 MB - Last synced: 8 months ago - Pushed: 12 months ago - Stars: 4 - Forks: 2

LucaGrasso/LPVS----Model-Checker-di-una-BlockChain

Progetto di Model Checker - Progetto presentato al il corso di laurea L31 a Urbino

Size: 269 KB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 0 - Forks: 0

NotBad4U/mcltl-rs

[beta] An experimental model checker for LTL written in Rust

Language: Rust - Size: 614 KB - Last synced: about 1 year ago - Pushed: about 4 years ago - Stars: 3 - Forks: 0

sgomber/traffic-controller-NuSMV

Project done for my B.Tech course on Formal Methods for System Verification

Size: 354 KB - Last synced: about 1 year ago - Pushed: over 2 years ago - Stars: 5 - Forks: 0

wimmers/munta

Fully verified model checker for realtime systems

Language: Isabelle - Size: 6.49 MB - Last synced: about 1 year ago - Pushed: almost 2 years ago - Stars: 15 - Forks: 2

sybila/pithya-core

Language: Kotlin - Size: 2.97 MB - Last synced: about 2 months ago - Pushed: almost 2 years ago - Stars: 1 - Forks: 0

iamonur/the_legendary_pipeline

Study for mah thesis

Language: C - Size: 473 KB - Last synced: about 1 year ago - Pushed: almost 3 years ago - Stars: 0 - Forks: 0

bergfi/llmc

LLMC is a multi-core model checker of LLVM IR. It translates the input LLVM IR into a model LLVM IR that implements the DMC API, the API of the model checker DMC. This allows LLMC to execute the model's next-state function, instead of interpreting the input LLVM IR, enabling speedups of orders of magnitude.

Language: C++ - Size: 412 KB - Last synced: over 1 year ago - Pushed: about 3 years ago - Stars: 1 - Forks: 0

sybila/pithya-gui

R based GUI for biodivine

Language: R - Size: 1.73 MB - Last synced: about 2 months ago - Pushed: over 3 years ago - Stars: 1 - Forks: 1

rtsaad/mercury

High-Performance Model Checker developed for multicore, multiprocessors machines (NUMA).

Language: C - Size: 600 KB - Last synced: about 1 year ago - Pushed: over 3 years ago - Stars: 3 - Forks: 0

Jentsch/modelchecker

Language: Scala - Size: 328 KB - Last synced: about 1 year ago - Pushed: over 4 years ago - Stars: 6 - Forks: 0

porglezomp/hyalite

A bounded model checker for an IMP-style imperative language.

Language: Rust - Size: 10.7 KB - Last synced: about 1 year ago - Pushed: over 5 years ago - Stars: 6 - Forks: 0

pablofcastro/faulty

A Model Checker for the logic dCTL

Language: Java - Size: 10.9 MB - Last synced: about 1 year ago - Pushed: over 5 years ago - Stars: 0 - Forks: 0