model-checking | Topic | Ecosyste.ms: Repos

Topic: "model-checking"

p-org/P

The P programming language.

Language: C# - Size: 143 MB - Last synced at: 1 day ago - Pushed at: 2 days ago - Stars: 3,274 - Forks: 194

model-checking/kani

Kani Rust Verifier

Language: Rust - Size: 32.6 MB - Last synced at: about 7 hours ago - Pushed at: about 18 hours ago - Stars: 2,531 - Forks: 111

tlaplus/tlaplus

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

Language: Java - Size: 138 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 2,417 - Forks: 210

ligurio/sqa-wiki

My own notes (drafts mostly) about software quality

Size: 392 KB - Last synced at: 5 days ago - Pushed at: about 2 years ago - Stars: 2,282 - Forks: 409

spacejam/tla-rust

writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+

Language: TLA - Size: 728 KB - Last synced at: 5 days ago - Pushed at: almost 8 years ago - Stars: 1,054 - Forks: 27

AliveToolkit/alive2

Automatic verification of LLVM optimizations

Language: C++ - Size: 6.23 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 887 - Forks: 116

lemmy/BlockingQueue

Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!

Language: TLA - Size: 18.3 MB - Last synced at: 15 days ago - Pushed at: 6 months ago - Stars: 491 - Forks: 22

thomasp85/lime

Local Interpretable Model-Agnostic Explanations (R port of original Python package)

Language: R - Size: 10.6 MB - Last synced at: 23 days ago - Pushed at: over 2 years ago - Stars: 484 - Forks: 109

apalache-mc/apalache

APALACHE: symbolic model checker for TLA+ and Quint

Language: Scala - Size: 62.2 MB - Last synced at: 1 day ago - Pushed at: 7 days ago - Stars: 456 - Forks: 42

seahorn/seahorn

SeaHorn Verification Framework

Language: C - Size: 7.46 MB - Last synced at: 9 days ago - Pushed at: about 2 months ago - Stars: 446 - Forks: 131

johnyf/tool_lists

Links to tools by subject

Size: 63.5 KB - Last synced at: about 1 month ago - Pushed at: about 1 year ago - Stars: 375 - Forks: 83

tlaplus/vscode-tlaplus

TLA+ language support for Visual Studio Code

Language: TypeScript - Size: 25 MB - Last synced at: 16 days ago - Pushed at: 24 days ago - Stars: 374 - Forks: 38

epfl-lara/stainless

Verification framework and tool for higher-order Scala programs

Language: Scala - Size: 139 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 372 - Forks: 56

parapluu/Concuerror

Concuerror is a stateless model checking tool for Erlang programs.

Language: Erlang - Size: 10.5 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 338 - Forks: 42

ultimate-pa/ultimate

The Ultimate program analysis framework.

Language: Java - Size: 879 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 217 - Forks: 44

firmai/datagene

DataGene - Identify How Similar TS Datasets Are to One Another (by @firmai)

Language: Jupyter Notebook - Size: 1.12 MB - Last synced at: 7 days ago - Pushed at: about 3 years ago - Stars: 205 - Forks: 24

github/deli 📦

Language: Haskell - Size: 48.8 KB - Last synced at: 3 months ago - Pushed at: over 4 years ago - Stars: 167 - Forks: 9

pmer/tla-bin

Command line binaries for the TLA+ language

Language: Shell - Size: 23.4 KB - Last synced at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 157 - Forks: 21

moves-rwth/storm

A Modern Probabilistic Model Checker

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

kelvich/tlaplus_jupyter

Jupyter kernel for TLA⁺

Language: Python - Size: 78.1 KB - Last synced at: 8 days ago - Pushed at: over 2 years ago - Stars: 119 - Forks: 8

will62794/spectacle

Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+.

Language: JavaScript - Size: 27.8 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 117 - Forks: 8

mCRL2org/mCRL2

The Git repository for the mCRL2 toolset.

Language: C++ - Size: 102 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 97 - Forks: 42

jayhorn/jayhorn

Static checker for Java

Language: Java - Size: 180 MB - Last synced at: about 2 months ago - Pushed at: 3 months ago - Stars: 85 - Forks: 23

aman-goel/avr

Reads a state transition system and performs property checking

Language: C++ - Size: 910 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 76 - Forks: 20

cristian-mattarei/CoSA

CoreIR Symbolic Analyzer

Language: Python - Size: 7.98 MB - Last synced at: 12 months ago - Pushed at: over 4 years ago - Stars: 60 - Forks: 15

informalsystems/modelator

Model-based testing tool

Language: Python - Size: 334 MB - Last synced at: 5 days ago - Pushed at: about 1 month ago - Stars: 56 - Forks: 5

utwente-fmt/ltsmin

The LTSmin model checking toolset

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

alcestes/effpi

Verified message-passing programs in Dotty

Language: Scala - Size: 281 KB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 48 - Forks: 8

jrclogic/SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.

Language: Haskell - Size: 14.2 MB - Last synced at: 13 days ago - Pushed at: 2 months ago - Stars: 46 - Forks: 9

ftsrg/theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms

Language: Java - Size: 195 MB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 46 - Forks: 40

tlaplus-workshops/ewd998

Distributed termination detection on a ring, due to Shmuel Safra:

Language: TLA - Size: 1.95 MB - Last synced at: 12 months ago - Pushed at: over 1 year ago - Stars: 46 - Forks: 47

gipsyh/rIC3

Hardware Formal Verification Tool

Language: Rust - Size: 1.88 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 45 - Forks: 9

model-checking/cbmc-starter-kit

The CBMC starter kit makes it easy to add CBMC verification to a software project.

Language: Python - Size: 1.42 MB - Last synced at: 9 days ago - Pushed at: about 2 months ago - Stars: 45 - Forks: 22

lemmy/ewd998 📦

Distributed termination detection on a ring, due to Shmuel Safra: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF

Language: TLA - Size: 1.61 MB - Last synced at: almost 2 years ago - Pushed at: about 2 years ago - Stars: 41 - Forks: 12

will62794/tlaplus_repl

A simple REPL for TLA+.

Language: Python - Size: 21.5 KB - Last synced at: 22 days ago - Pushed at: about 1 year ago - Stars: 40 - Forks: 2

ge-high-assurance/VERDICT

DARPA's Cyber Assured Systems Engineering (CASE) project named Verification Evidence and Resilient Design in Anticipation of Cybersecurity Threats (VERDICT)

Language: Java - Size: 23.4 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 37 - Forks: 14

robkorn/plutus-experimental-smart-contracts

Experimental Smart Contracts In Plutus.

Language: Haskell - Size: 68.4 KB - Last synced at: about 2 years ago - Pushed at: about 6 years ago - Stars: 34 - Forks: 8

mryndzionek/tlaplus_specs

Different TLA+ specifications, mostly for learning purposes

Language: TLA - Size: 161 MB - Last synced at: about 2 months ago - Pushed at: 12 months ago - Stars: 31 - Forks: 1

y-taka-23/ddsv-go

A toy deadlock detector written in Go. 🔍

Language: Go - Size: 428 KB - Last synced at: 13 days ago - Pushed at: about 5 years ago - Stars: 30 - Forks: 2

informalsystems/modelator-py

Utilities for the TLA+ ecoystem and model-based testing using TLA+.

Language: Python - Size: 68.7 MB - Last synced at: 20 days ago - Pushed at: over 2 years ago - Stars: 29 - Forks: 3

hlisdero/cargo-check-deadlock

Find deadlocks in Rust code with Petri net model checking

Language: Rust - Size: 1.78 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 28 - 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: 9 days ago - Pushed at: 9 days ago - Stars: 28 - Forks: 14

johnwickerson/memalloy

Memory consistency modelling using Alloy

Language: OCaml - Size: 4.99 MB - Last synced at: 6 months ago - Pushed at: over 4 years ago - Stars: 28 - Forks: 6

ai4reason/Prover9

Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.

Language: C - Size: 1.81 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 27 - Forks: 8

ElNiak/awesome-formal-verification

Welcome to the ultimate list of resources for formal verification techniques and tools. This repository aims to provide an organized collection of high-quality resources to help professionals, researchers, and enthusiasts stay updated and advance their knowledge in the field.

Size: 24.4 KB - Last synced at: 8 days ago - Pushed at: 3 months ago - Stars: 25 - Forks: 2

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

lip6/ITSTools

A multi-formalism, multi-solution model-checker centered on the language GAL

Language: Python - Size: 624 MB - Last synced at: 2 days ago - Pushed at: 9 days ago - Stars: 24 - Forks: 12

draeger-lab/ModelPolisher

ModelPolisher accesses the BiGG Models knowledgebase to annotate SBML models.

Language: Java - Size: 63.8 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 23 - Forks: 7

go-air/reach

symbolic reachability checker

Language: Go - Size: 1.9 MB - Last synced at: 10 months ago - Pushed at: over 3 years ago - Stars: 22 - Forks: 3

ldv-klever/klever

Read-only mirror of the Klever Git repository

Language: Python - Size: 162 MB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 21 - Forks: 14

tlaplus/azure-cosmos-tla Fork of Azure/azure-cosmos-tla

Azure Cosmos TLA+ specifications

Language: TLA - Size: 1.28 MB - Last synced at: 28 days ago - Pushed at: 3 months ago - Stars: 21 - Forks: 5

Rapfff/jajapy

Baum-Welch for all kind of Markov models

Language: Python - Size: 8.23 MB - Last synced at: 13 days ago - Pushed at: about 1 year ago - Stars: 21 - Forks: 2

ftsrg/gazer

An LLVM-based formal verification frontend for C programs.

Language: C++ - Size: 1.45 MB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 21 - Forks: 5

Smattr/rumur

yet another model checker

Language: C++ - Size: 3.58 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 20 - Forks: 6

ticktac-project/tchecker

TChecker is an open-source verification tool for timed automata

Language: C++ - Size: 24.5 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 20 - Forks: 16

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: 5 months ago - Pushed at: 5 months ago - Stars: 19 - Forks: 2

xlauko/lart

LLVM Abstraction & Refinement Tool. The goal of this tool is to provide LLVM-to-LLVM transformations that implement various program abstractions. In terms of the instruction set, the resulting programs are normal, concrete LLVM programs that can be executed and analyzed.

Language: C++ - Size: 1.06 MB - Last synced at: 11 days ago - Pushed at: about 2 years ago - Stars: 19 - Forks: 2

harmonylang/harmony

A Python-like programming language for testing and experimenting with concurrent programs.

Language: Python - Size: 86.2 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 18 - Forks: 6

formalmethods/intrepid

Intrepyd Model Checker

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

kframework/p4-semantics

Formal Semantics of P4 in K

Language: P4 - Size: 1.01 MB - Last synced at: about 1 year ago - Pushed at: almost 4 years ago - Stars: 18 - Forks: 2

eve-mas/eve-parity

Equilibrium Verification Environment (EVE) is a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems.

Language: Python - Size: 8.91 MB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 17 - Forks: 3

alcestes/mpstk

Multiparty Session Types toolKit

Language: Scala - Size: 1.15 MB - Last synced at: over 1 year ago - Pushed at: almost 6 years ago - Stars: 15 - Forks: 4

tniessen/aiger-safety-properties

AIGER files designed by hand, for testing (and limited benchmarking) of new model checkers

Size: 2.39 MB - Last synced at: 27 days ago - Pushed at: over 1 year ago - Stars: 14 - Forks: 7

vincenzoml/VoxLogicA

VoxLogicA: the "Voxel-based Logical Analyser", is an interpreter of a declarative language, inspired by spatial logics, to analyse images in a simple way. See also http://www.voxlogica.org .

Size: 252 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 13 - Forks: 4

UPPAALModelChecker/uppaal-latex

LaTeX package to typeset Uppaal timed automata specifications

Language: TeX - Size: 428 KB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 13 - Forks: 1

cubicle-model-checker/cubicle

The Cubicle model checker

Language: OCaml - Size: 57.4 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 13 - Forks: 8

yurukute/CTU

Repo tổng hợp các bài thực hành và bài làm trên hệ thống ELSE

Language: C - Size: 37.8 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 12 - Forks: 5

stateright/stateright.github.io

"Building Distributed Systems with Stateright"

Language: JavaScript - Size: 5.05 MB - Last synced at: 18 days ago - Pushed at: almost 2 years ago - Stars: 12 - Forks: 3

eras/tlsd

Generate (message) sequence diagrams from TLA+ state traces

Language: Python - Size: 95.7 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 12 - Forks: 0

hengxin/tlaplus-at-nju-disalg

Learning [Lamport's TLA+](http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).

Language: TeX - Size: 231 MB - Last synced at: about 2 months ago - Pushed at: about 3 years ago - Stars: 12 - Forks: 7

LauZyHou/sbid-ava

🔮内生安全建模工具，基于.Net Core 3.0的Avalonia跨平台桌面应用。

Language: C# - Size: 714 KB - Last synced at: 5 months ago - Pushed at: almost 4 years ago - Stars: 12 - Forks: 4

GaloisInc/LIMA

LIMA: Language for Integrated Modeling and Analysis

Language: Haskell - Size: 195 KB - Last synced at: 12 months ago - Pushed at: over 6 years ago - Stars: 12 - Forks: 2

AliAtaollahi/Solidity2mCRL2-Compiler-Project

A compiler developed using ANTLR in Java that translates Solidity smart contracts into mCRL2 models

Language: Java - Size: 18.7 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 11 - Forks: 0

Broundal/Pytolemaic

Toolbox for analysis of model's quality and model's description. For further details see

Language: Python - Size: 1.16 MB - Last synced at: about 1 month ago - Pushed at: 12 months ago - Stars: 11 - Forks: 3

janislley/LSVerifier

LSVerifier - Large Systems Verifier

Language: Python - Size: 22.4 MB - Last synced at: 14 days ago - Pushed at: about 1 year ago - Stars: 11 - Forks: 3

SmnTin/lincheck

A linearizability checker for concurrent data structures

Language: Rust - Size: 67.4 KB - Last synced at: 26 days ago - Pushed at: over 1 year ago - Stars: 11 - Forks: 0

cesaro/cunf

A model checker for safe Petri nets based on partial-order semantics

Language: C++ - Size: 6.95 MB - Last synced at: over 1 year ago - Pushed at: over 4 years ago - Stars: 11 - Forks: 1

burakim/Kaptan-Field-Checker

A Class Field Value Validation Library.

Language: Java - Size: 112 KB - Last synced at: about 1 year ago - Pushed at: over 6 years ago - Stars: 11 - Forks: 0

dalzilio/mcc

High-Level Nets Blaster for the Model-Checking Contest

Language: Go - Size: 1.18 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 10 - Forks: 1

paultristanwagner/model-checking

Command line tool for model checking using LTL, CTL and CTL* formulas

Language: Java - Size: 562 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 10 - Forks: 0

moves-rwth/attestor

A Shape Analysis Tool based on Graph Grammars

Language: Java - Size: 38.4 MB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 10 - Forks: 4

amamory-verification/hw-formal-verif

Hardware Formal Verification

Language: Verilog - Size: 3.74 MB - Last synced at: almost 2 years ago - Pushed at: over 4 years ago - Stars: 10 - Forks: 3

pfnet-research/pml

A ML-like programming language with type-based probabilistic behavior specification, developed as part of PFN summer internship 2018.

Language: C++ - Size: 41 KB - Last synced at: 11 days ago - Pushed at: over 6 years ago - Stars: 10 - Forks: 2

fadoss/umaudemc

Unified Maude model-checking tool

Language: Python - Size: 273 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 9 - Forks: 1

Gy-Hu/pyBMC

Implementation of bounded model checking with Z3py. (AIGER1.0 support)

Language: Python - Size: 104 MB - Last synced at: 5 days ago - Pushed at: almost 2 years ago - Stars: 9 - Forks: 0

lip6/libITS

Core Guarded Action Language and Instantiable Transition System semantics using libDDD.

Language: C++ - Size: 180 MB - Last synced at: 2 days ago - Pushed at: 9 days ago - Stars: 8 - Forks: 5

d702e20/CGAAL

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

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

gdellapenna/UPMurphi 📦

UPMurphi planner for linear and nonlinear continuous PDDL+ models with processes and events

Language: C++ - Size: 360 KB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 8 - Forks: 4

sbu-fsl/Metis

Metis: File System Model Checking via Versatile Input and State Exploration (FAST '24)

Language: C - Size: 2.78 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 7 - Forks: 1

rohitdureja/FuseIC3

An Algorithm for Checking Large Design Spaces

Language: C++ - Size: 122 KB - Last synced at: about 1 year ago - Pushed at: almost 8 years ago - Stars: 7 - Forks: 3

huffyhenry/ltl24

An experimental verification and querying language for F24 football data

Language: Haskell - Size: 74.2 KB - Last synced at: about 18 hours ago - Pushed at: over 8 years ago - Stars: 7 - Forks: 0

spatstat/spatstat.core

sub-package of spatstat containing core functionality for data analysis and modelling

Language: R - Size: 3.83 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 6 - Forks: 9

moves-rwth/prophesy

Parameter Synthesis in Markov Models

Language: Python - Size: 71.1 MB - Last synced at: 14 days ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 3

lip6/ITS-CTL 📦

CTL symbolic model-checker based on libDDD and libITS

Language: C - Size: 1.77 MB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 6 - Forks: 3