gipsyh/rIC3

A high-performance IC3/PDR algorithm implementation in Rust.

Language: Rust - Size: 606 KB - Last synced: about 18 hours ago - Pushed: about 18 hours ago - Stars: 4 - Forks: 0

lip6/ITSTools

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

Language: Python - Size: 336 MB - Last synced: about 18 hours ago - Pushed: about 19 hours ago - Stars: 22 - Forks: 10

epfl-lara/stainless

Verification framework and tool for higher-order Scala programs

Language: HTML - Size: 139 MB - Last synced: about 19 hours ago - Pushed: about 19 hours ago - Stars: 346 - Forks: 48

parapluu/Concuerror

Concuerror is a stateless model checking tool for Erlang programs.

Language: Erlang - Size: 10.5 MB - Last synced: about 23 hours ago - Pushed: about 24 hours ago - Stars: 329 - Forks: 43

p-org/P

The P programming language.

Language: C# - Size: 142 MB - Last synced: 1 day ago - Pushed: 1 day ago - Stars: 2,925 - Forks: 168

pitt-miskov-zivanov-lab/ACCORDION

ACCORDION (ACCelerating and Optimizing model RecommenDatIONs) is a novel tool and methodology for rapid model assembly by automatically extending and evaluating dynamic network models with the information published in literature.

Language: Python - Size: 23 MB - Last synced: 1 day ago - Pushed: 2 days ago - Stars: 0 - Forks: 0

ticktac-project/tchecker

TChecker is an open-source verification tool for timed automata

Language: C++ - Size: 24.4 MB - Last synced: 2 days ago - Pushed: 2 days ago - Stars: 19 - Forks: 16

Pathemeous/Symbolic-Gossip

Symbolic Model Checker for the Gossip Problem

Language: TeX - Size: 280 KB - Last synced: 4 days ago - Pushed: 4 days ago - Stars: 1 - Forks: 0

ldv-klever/klever

Read-only mirror of the Klever Git repository

Language: Python - Size: 162 MB - Last synced: 7 days ago - Pushed: 10 days ago - Stars: 20 - Forks: 12

AliveToolkit/alive2

Automatic verification of LLVM optimizations

Language: C++ - Size: 5.95 MB - Last synced: 5 days ago - Pushed: 5 days ago - Stars: 692 - Forks: 87

semperos/river-crossing-spec

TLA Specification for the "Wolf, goat, and cabbage" puzzle (https://en.wikipedia.org/wiki/Wolf,_goat_and_cabbage_problem)

Language: TLA - Size: 290 KB - Last synced: 6 days ago - Pushed: over 4 years ago - Stars: 1 - Forks: 0

mCRL2org/mCRL2

The Git repository for the mCRL2 toolset.

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

moves-rwth/storm

A Modern Probabilistic Model Checker

Language: C++ - Size: 198 MB - Last synced: 6 days ago - Pushed: 6 days ago - Stars: 124 - Forks: 69

Smattr/rumur

yet another model checker

Language: C++ - Size: 3.36 MB - Last synced: 6 days ago - Pushed: 6 days ago - Stars: 12 - Forks: 5

tlaplus/tlaplus

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

Language: Java - Size: 136 MB - Last synced: 7 days ago - Pushed: 7 days ago - Stars: 2,217 - Forks: 181

andreamanini98/TABEC

Tool for creating Timed Automata and checking their language emptiness.

Language: C++ - Size: 6.39 MB - Last synced: 6 days ago - Pushed: 7 days ago - Stars: 0 - Forks: 0

v-research/website

v-research website

Language: SCSS - Size: 3.32 MB - Last synced: 8 days ago - Pushed: 8 days ago - Stars: 0 - Forks: 0

lip6/libITS

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

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

mryndzionek/tlaplus_specs

Different TLA+ specifications, mostly for learning purposes

Language: TLA - Size: 144 MB - Last synced: 8 days ago - Pushed: 9 days ago - Stars: 28 - Forks: 1

hlisdero/cargo-check-deadlock

Find deadlocks in Rust code with Petri net model checking

Language: Rust - Size: 1.76 MB - Last synced: 9 days ago - Pushed: 10 days ago - Stars: 18 - Forks: 1

jens-classen/vergo

Vergo: A Verification System for GOLOG Programs

Language: Prolog - Size: 1.14 MB - Last synced: 11 days ago - Pushed: 11 days ago - Stars: 4 - Forks: 1

informalsystems/apalache

APALACHE: symbolic model checker for TLA+ and Quint

Language: Scala - Size: 57.9 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 403 - Forks: 38

ahamez/caesar.sdd

An implementation of caesar.bdd using SDD

Language: C++ - Size: 963 KB - Last synced: 13 days ago - Pushed: almost 5 years ago - Stars: 2 - Forks: 2

montao/formal-verification

🌍 The SMV models

Language: Matlab - Size: 22.5 KB - Last synced: 14 days ago - Pushed: almost 7 years ago - Stars: 0 - Forks: 0

Ohara124c41/ASML-Wafer_Stepper

This project was for a course at TU/e called System Validation. The goal was to create an architecture with parallel components and use formal model checking to evaluate the model. The use case is a simplified EUV wafer stepper from ASML.

Size: 26.7 MB - Last synced: 14 days ago - Pushed: over 5 years ago - Stars: 1 - Forks: 0

ftsrg/theta

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

Language: Java - Size: 195 MB - Last synced: 17 days ago - Pushed: 17 days ago - Stars: 46 - Forks: 40

spacejam/tla-rust

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

Language: TLA - Size: 728 KB - Last synced: 13 days ago - Pushed: almost 7 years ago - Stars: 1,023 - Forks: 26

janislley/LSVerifier

LSVerifier - Large Systems Verifier

Language: Python - Size: 22.4 MB - Last synced: 13 days ago - Pushed: about 1 month ago - Stars: 7 - Forks: 4

jrclogic/SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.

Language: Haskell - Size: 14.1 MB - Last synced: 20 days ago - Pushed: 21 days ago - Stars: 39 - Forks: 9

benkeks/equivalence-fiddle

Tool for finding the best ways of equating / preordering / distinguishing finite process models.

Language: Scala - Size: 11.2 MB - Last synced: 25 days ago - Pushed: 25 days ago - Stars: 3 - Forks: 1

ligurio/sqa-wiki

My own notes (drafts mostly) about software quality

Size: 392 KB - Last synced: 22 days ago - Pushed: over 1 year ago - Stars: 2,216 - Forks: 401

model-checking/kani

Kani Rust Verifier

Language: Rust - Size: 29.3 MB - Last synced: 23 days ago - Pushed: 23 days ago - Stars: 1,886 - Forks: 77

moves-rwth/attestor

A Shape Analysis Tool based on Graph Grammars

Language: Java - Size: 38.4 MB - Last synced: 23 days ago - Pushed: over 1 year ago - Stars: 10 - Forks: 4

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: 12 days ago - Pushed: 12 days ago - Stars: 26 - Forks: 12

informalsystems/modelator

Model-based testing tool

Language: Python - Size: 334 MB - Last synced: 9 days ago - Pushed: 11 months ago - Stars: 51 - Forks: 5

seahorn/seahorn

SeaHorn Verification Framework

Language: C - Size: 7.52 MB - Last synced: 26 days ago - Pushed: 26 days ago - Stars: 429 - Forks: 132

ultimate-pa/ultimate

The Ultimate program analysis framework.

Language: Java - Size: 818 MB - Last synced: 28 days ago - Pushed: 29 days ago - Stars: 182 - Forks: 40

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: 29 days ago - Pushed: 29 days ago - Stars: 37 - Forks: 14

parof/protocol-validation

Language: TeX - Size: 222 KB - Last synced: 28 days ago - Pushed: over 4 years ago - Stars: 2 - Forks: 0

tlaplus/vscode-tlaplus

TLA+ language support for Visual Studio Code

Language: TypeScript - Size: 24.9 MB - Last synced: 25 days ago - Pushed: 3 months ago - Stars: 329 - Forks: 29

will62794/tla-web

TLA+ Web Explorer.

Language: TLA - Size: 24 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 34 - Forks: 4

yepengding/Kiwami

A generic bounded model checker.

Language: Java - Size: 90.8 KB - Last synced: about 1 month ago - Pushed: over 1 year ago - Stars: 2 - Forks: 0

yepengding/ModelCheckingNotes

Notes in fundamentals of model checking.

Size: 16.6 KB - Last synced: about 1 month ago - Pushed: almost 2 years ago - Stars: 0 - 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: about 1 month ago - Pushed: over 5 years ago - Stars: 3 - Forks: 4

AhmedShafique313/sml_udemy

Its contain all labs and lecture records of Machine Learning specialization course. This course is made by AI/ML team DevIEO and this course is presented by Services By IEO.

Language: Python - Size: 52 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 0 - Forks: 2

johnyf/tool_lists

Links to tools by subject

Size: 63.5 KB - Last synced: 27 days ago - Pushed: about 2 months ago - Stars: 360 - Forks: 81

formalmethods/intrepid

Intrepyd Model Checker

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

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: about 1 month ago - Pushed: about 1 month ago - Stars: 12 - Forks: 3

github/deli 📦

Language: Haskell - Size: 48.8 KB - Last synced: about 1 month ago - Pushed: over 3 years ago - Stars: 165 - Forks: 9

UPPAALModelChecker/uppaal-libs

Dynamic libraries for Uppaal models

Language: C++ - Size: 101 KB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 1 - Forks: 3

Rapfff/jajapy

Baum-Welch for all kind of Markov models

Language: Python - Size: 8.23 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 12 - Forks: 1

tlaplus-workshops/ewd998

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

Language: TLA - Size: 1.95 MB - Last synced: 21 days ago - Pushed: 7 months ago - Stars: 46 - Forks: 47

harmonylang/harmony

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

Language: Python - Size: 86.3 MB - Last synced: 10 days ago - Pushed: 10 days ago - Stars: 14 - Forks: 3

seer-lab/CORE

An automatic bug repair tool for concurrent Java programs. Utilizes Java PathFinder (JPF) model checker.

Language: Python - Size: 8.64 MB - Last synced: about 2 months ago - Pushed: over 9 years ago - Stars: 0 - Forks: 0

aai-institute/tfl-training-probabilistic-model-checking

TfL course on probabilistic model checking using storm

Language: Jupyter Notebook - Size: 59.4 MB - Last synced: about 2 months ago - Pushed: about 2 months ago - Stars: 1 - Forks: 0

cristian-mattarei/CoSA

CoreIR Symbolic Analyzer

Language: Python - Size: 7.98 MB - Last synced: 19 days ago - Pushed: over 3 years ago - Stars: 60 - Forks: 15

fadoss/umaudemc

Unified Maude model-checking tool

Language: Python - Size: 270 KB - Last synced: about 2 months ago - Pushed: about 2 months ago - Stars: 8 - Forks: 1

utwente-fmt/ltsmin

The LTSmin model checking toolset

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

ptgm/bioNuSMV Fork of hklarner/NuSMV-a

bioNuSMV is a fork and extension of https://github.com/hklarner/NuSMV-a, which adds a handful of features to ease the use of model checking by biological modelers, in particular, in the context of the verification of qualitative regulatory networks

Language: C - Size: 12 MB - Last synced: 2 months ago - Pushed: almost 6 years ago - Stars: 2 - Forks: 1

hub-se/PSP-UPPAAL

Property Specification Patterns for UPPAAL

Language: Java - Size: 286 KB - Last synced: about 2 months ago - Pushed: over 2 years ago - Stars: 4 - Forks: 0

TechnionFV/CaDiCaL-DRUPing-for-Interpolants-Project-Version-Base Fork of arminbiere/cadical

This repository provides an extension to the CaDiCaL SAT solver that implements the "DRUPing for Interpolants" algorithm.

Size: 2.39 MB - Last synced: 2 months ago - Pushed: 2 months ago - Stars: 0 - Forks: 0

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

firmai/datagene

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

Language: Jupyter Notebook - Size: 1.12 MB - Last synced: 1 day ago - Pushed: over 2 years ago - Stars: 191 - Forks: 22

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: 18 days ago - Pushed: about 1 year ago - Stars: 18 - Forks: 2

phagenlocher/braincheck

A static and dynamic analyzer for Brainfuck

Language: C++ - Size: 46.9 KB - Last synced: 17 days ago - Pushed: 9 months ago - Stars: 1 - Forks: 0

sbu-fsl/Metis

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

Language: C - Size: 2.71 MB - Last synced: 4 days ago - Pushed: 4 days ago - Stars: 6 - Forks: 1

barnslig/bachelor-thesis

My bachelor's thesis, including an experimental swarm verification model checker running on the GPU.

Language: Jupyter Notebook - Size: 7.79 MB - Last synced: 27 days ago - Pushed: over 2 years ago - Stars: 1 - Forks: 0

kframework/p4-semantics

Formal Semantics of P4 in K

Language: P4 - Size: 1.01 MB - Last synced: about 2 months ago - Pushed: almost 3 years ago - Stars: 18 - Forks: 2

aman-goel/avr

Reads a state transition system and performs property checking

Language: C++ - Size: 910 MB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 68 - Forks: 17

tniessen/aiger-safety-properties

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

Size: 2.39 MB - Last synced: 13 days ago - Pushed: 6 months ago - Stars: 11 - Forks: 7

probing-lab/HyperPAYNT

Synthesizing controllers for Probabilistic HyperProperties on MDPs.

Language: C++ - Size: 144 MB - Last synced: 22 days ago - Pushed: about 2 months ago - Stars: 0 - Forks: 0

rohitdureja/FuseIC3

An Algorithm for Checking Large Design Spaces

Language: C++ - Size: 122 KB - Last synced: 2 months ago - Pushed: almost 7 years ago - Stars: 7 - Forks: 3

will62794/tlaplus_repl

A simple REPL for TLA+.

Language: Python - Size: 21.5 KB - Last synced: about 2 months ago - Pushed: 2 months ago - Stars: 39 - Forks: 2

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.2 MB - Last synced: 3 months ago - Pushed: 11 months ago - Stars: 474 - Forks: 20

at0m-b0mb/Mlflow-TensorFlow-Image-Classification-Guide

The MLflow TensorFlow Guide is an educational project. This project demonstrates how to build, train, and manage a TensorFlow machine learning model using MLflow, a powerful open-source platform for the end-to-end machine learning lifecycle.

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

tuura/sync-models

Tool for creating synchronous models and behavioral specifications for asynchronous circuits

Language: Verilog - Size: 543 KB - Last synced: about 2 months ago - Pushed: almost 6 years ago - Stars: 5 - Forks: 0

kelvich/tlaplus_jupyter

Jupyter kernel for TLA⁺

Language: Python - Size: 78.1 KB - Last synced: 27 days ago - Pushed: over 1 year ago - Stars: 118 - Forks: 7

m4lvin/GoMoChe

🗣️📞 Gossip Model Checking

Language: Haskell - Size: 85.9 KB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 2 - Forks: 1

d702e20/CGAAL

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

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

UPPAALModelChecker/uppaal-latex

LaTeX package to typeset Uppaal timed automata specifications

Language: TeX - Size: 427 KB - Last synced: 7 days ago - Pushed: 7 days ago - Stars: 11 - Forks: 1

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: 2.51 MB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 17 - Forks: 4

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: 4 months ago - Pushed: 4 months ago - Stars: 27 - Forks: 8

hengxin/tla-deep-into-code

Applying TLA+/TLC/TLAPS to Source Code

Size: 13.5 MB - Last synced: 4 months ago - Pushed: about 4 years ago - Stars: 0 - 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: 8 days ago - Pushed: 9 days ago - Stars: 11 - Forks: 5

DerYeger/MiniCheck

MiniCheck is a CLI for CTL and bounded LTL model checking on transition systems.

Language: Haskell - Size: 531 KB - Last synced: 14 days ago - Pushed: 11 months ago - Stars: 2 - Forks: 0

ftsrg/gazer

An LLVM-based formal verification frontend for C programs.

Language: C++ - Size: 1.45 MB - Last synced: about 2 months ago - Pushed: over 2 years ago - Stars: 21 - Forks: 5

paultristanwagner/model-checking

Practice environment implementing a model checker for LTL, CTL and CTL* formulas

Language: Java - Size: 562 KB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 7 - Forks: 0

shanthiachar18/Project-onMultiple-Linear-Regression-2

Multiple Linear Regression model for ToyotaCorolla data

Language: Jupyter Notebook - Size: 1.24 MB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

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

Azure Cosmos TLA+ specifications

Language: TLA - Size: 1.27 MB - Last synced: 25 days ago - Pushed: 5 months ago - Stars: 17 - Forks: 5

rvprasad/verification-validation-course 📦

Verification and Validation course offered at Kansas State University in Fall'15, '16, and '17

Size: 37 MB - Last synced: 5 months ago - Pushed: over 6 years ago - Stars: 1 - Forks: 0

alcestes/effpi

Verified message-passing programs in Dotty

Language: Scala - Size: 281 KB - Last synced: 5 months ago - Pushed: about 3 years ago - Stars: 48 - Forks: 8

Demon-2-Angel/Handwritten-Digit-Classification

This document explores the use of Principal Component Analysis (PCA) in a machine learning context, specifically for image classification using a dataset of numerical representations of digits. The dataset is loaded using sci-kit-learn's load_digits function, and initial exploration is conducted to understand its structure.

Language: Jupyter Notebook - Size: 15.6 KB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

f-musa/ctl-model-checker

This project's objective is to program a model checking software that verifies the validity of a CTL formula on the initial state of a finite automaton.

Language: Java - Size: 55.7 KB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

karankashyap04/cs1710-kmeans

Final project for CS1710: Model checking for the k-means clustering algorithm

Language: Python - Size: 1.85 MB - Last synced: 5 months ago - Pushed: about 1 year ago - Stars: 0 - Forks: 0

vijitVM/Lending-Club

Exploratory Data Analysis and Model Evaluation

Language: Jupyter Notebook - Size: 21.1 MB - Last synced: 6 months ago - Pushed: over 2 years ago - Stars: 0 - Forks: 0

go-air/reach

symbolic reachability checker

Language: Go - Size: 1.9 MB - Last synced: 14 days ago - Pushed: over 2 years ago - Stars: 21 - Forks: 3

Smart-Contract-Modelling-uOttawa/Symboleo-Model-Checker-Test-Generator

A test generator application designed to create performance benchmarks for SymploeoPC

Language: Java - Size: 17.6 MB - Last synced: 17 days ago - Pushed: 4 months ago - Stars: 4 - Forks: 0

jayhorn/jayhorn

Static checker for Java

Language: Java - Size: 180 MB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 72 - Forks: 19

marcusm117/mctk

Python Package Model Checking Toolkit

Language: Python - Size: 2.74 MB - Last synced: 18 days ago - Pushed: 3 months ago - Stars: 4 - Forks: 0

thomasp85/lime

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

Language: R - Size: 10.6 MB - Last synced: 6 months ago - Pushed: over 1 year ago - Stars: 480 - Forks: 110