uuverifiers/eldarica

The Eldarica model checker

Language: Scala - Size: 53.6 MB - Last synced at: about 13 hours ago - Pushed at: about 14 hours ago - Stars: 85 - Forks: 25

mCRL2org/mCRL2

The Git repository for the mCRL2 toolset.

Language: C++ - Size: 102 MB - Last synced at: about 21 hours ago - Pushed at: about 22 hours ago - Stars: 98 - Forks: 42

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.92 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 27 - Forks: 5

stateright/stateright

A model checker for implementing distributed systems.

Language: Rust - Size: 2.71 MB - Last synced at: 4 days ago - Pushed at: 6 days ago - Stars: 1,631 - Forks: 59

moves-rwth/storm

A Modern Probabilistic Model Checker

Language: C++ - Size: 195 MB - Last synced at: 20 days ago - Pushed at: 20 days ago - Stars: 147 - Forks: 80

parapluu/Concuerror

Concuerror is a stateless model checking tool for Erlang programs.

Language: Erlang - Size: 10.5 MB - Last synced at: 3 days ago - Pushed at: 26 days ago - Stars: 338 - Forks: 42

danielamadori98/PACO Fork of ansimonetti/PACO

Given a BPMN+CPI diagram and a impact bound, determine if a strategy exists to complete the process within the expectation limit and explain the necessary decisions.

Language: Python - Size: 74.8 MB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 0 - Forks: 0

Smattr/rumur

yet another model checker

Language: C++ - Size: 3.58 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 20 - Forks: 6

SRI-CSL/sally

A model checker for infinite-state systems.

Language: C++ - Size: 5.61 MB - Last synced at: about 1 month ago - Pushed at: 5 months ago - Stars: 74 - Forks: 13

koehlma/momba

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

Language: PDDL - Size: 32 MB - Last synced at: 9 days ago - Pushed at: 10 months ago - Stars: 19 - Forks: 3

ocaml-multicore/dscheck

Experimental model checker for testing concurrent algorithms

Language: OCaml - Size: 132 KB - Last synced at: about 1 month ago - Pushed at: 5 months ago - Stars: 33 - Forks: 5

LeonardoSaccotelli/Formal-Methods-For-Computer-Science

Language: Jupyter Notebook - Size: 83.4 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

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.5 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 28 - Forks: 14

formalmethods/intrepid

Intrepyd Model Checker

Language: Python - Size: 147 MB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 1

nclarius/pyPL

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

Language: Python - Size: 6.22 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 19 - Forks: 2

ahamez/pnmc

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

Language: C++ - Size: 1.26 MB - Last synced at: about 1 month ago - Pushed at: 3 months ago - Stars: 9 - Forks: 2

JakubSarnik/geyser

Simple implementation of PDR and CAR model checking algorithms

Language: C++ - Size: 2.07 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

utwente-fmt/ltsmin

The LTSmin model checking toolset

Language: C - Size: 7.43 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 52 - Forks: 30

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.67 MB - Last synced at: about 2 months ago - Pushed at: 11 months ago - Stars: 1 - Forks: 0

yylonly/LTSA

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

Language: Visual Basic - Size: 5.42 MB - Last synced at: about 1 year ago - Pushed at: over 6 years ago - Stars: 3 - Forks: 4

NotBad4U/mcltl-rs

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

Language: Rust - Size: 614 KB - Last synced at: 28 days ago - Pushed at: about 5 years ago - Stars: 5 - Forks: 2

phagenlocher/braincheck

A static and dynamic analyzer for Brainfuck

Language: C++ - Size: 46.9 KB - Last synced at: about 1 year ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0

d702e20/CGAAL

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

Language: Rust - Size: 33.5 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 8 - Forks: 1

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 at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 4 - Forks: 2

porglezomp/hyalite

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

Language: Rust - Size: 10.7 KB - Last synced at: about 2 months ago - Pushed at: about 6 years ago - Stars: 7 - Forks: 0

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 at: about 2 years ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0

sgomber/traffic-controller-NuSMV

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

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

wimmers/munta

Fully verified model checker for realtime systems

Language: Isabelle - Size: 6.49 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 15 - Forks: 2

sybila/pithya-core

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

iamonur/the_legendary_pipeline

Study for mah thesis

Language: C - Size: 473 KB - Last synced at: about 2 years ago - Pushed at: almost 4 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 at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 1 - Forks: 0

sybila/pithya-gui

R based GUI for biodivine

Language: R - Size: 1.73 MB - Last synced at: 2 months ago - Pushed at: over 4 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 at: about 2 years ago - Pushed at: over 4 years ago - Stars: 3 - Forks: 0

Jentsch/modelchecker

Language: Scala - Size: 328 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 6 - Forks: 0

juliendelplanque/DatabaseCritics

A tool to run critics on SQL database schema dumps.

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

pablofcastro/faulty

A Model Checker for the logic dCTL

Language: Java - Size: 10.9 MB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 0 - Forks: 0