A high-performance IC3/PDR algorithm implementation in Rust.
-
Updated
May 15, 2024 - Rust
A high-performance IC3/PDR algorithm implementation in Rust.
Interactive, web-based environment for exploring TLA+ specifications.
Verification framework and tool for higher-order Scala programs
A multi-formalism, multi-solution model-checker centered on the language GAL
Concuerror is a stateless model checking tool for Erlang programs.
The Ultimate program analysis framework.
DARPA's Cyber Assured Systems Engineering (CASE) project named Verification Evidence and Resilient Design in Anticipation of Cybersecurity Threats (VERDICT)
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.
TChecker is an open-source verification tool for timed automata
Symbolic Model Checker for the Gossip Problem
Read-only mirror of the Klever Git repository
Automatic verification of LLVM optimizations
The P programming language.
APALACHE: symbolic model checker for TLA+ and Quint
The Git repository for the mCRL2 toolset.
A Modern Probabilistic Model Checker
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
Tool for creating Timed Automata and checking their language emptiness.
Add a description, image, and links to the model-checking topic page so that developers can more easily learn about it.
To associate your repository with the model-checking topic, visit your repo's landing page and select "manage topics."