SRI Sally: A model checker for infinite-state systems.
-
Updated
Jul 31, 2025 - C++
#
bounded-model-checking
Here are 24 public repositories matching this topic...
Automated Code Repair suite powered by ESBMC and LLMs.
-
Updated
Feb 20, 2026 - Python
AProver: Agentic Prover for AI-Generated Code — LLM agents + BMC for automated verification of systems software
-
Updated
Jun 14, 2026 - Python
LSVerifier - Large Systems Verifier
model-checking software-verification formal-verification bounded-model-checking c-language open-source-software security-vulnerabilities
-
Updated
Dec 3, 2025 - Python
Implementation of bounded model checking with Z3py. (AIGER1.0 support)
-
Updated
Jul 22, 2023 - Python
A Symbolic Executor based on Separaton Logic
-
Updated
Mar 27, 2024 - SWIG
A bounded model checker for an IMP-style imperative language.
-
Updated
Feb 23, 2019 - Rust
This program introduces formal verification to card-based cryptography by providing a technique which automatically finds new protocols using as few as possible operations and searches for lowest bounds on card-minimal protocols.
cryptography formal-verification bounded-model-checking cbmc automated-reasoning multiparty-computation card-protocols
-
Updated
May 11, 2026 - C
bmc4j is a easy to use formal verification tool set for Kotlin (and Java).
-
Updated
Jun 14, 2026 - Kotlin
Python Package Model Checking Toolkit
python verification model-checking formal-verification bounded-model-checking symbolic-model-checking
-
Updated
Feb 5, 2024 - Python
The ESBMC ibmc (Invariant Based Model Checking) Tool.
software-verification formal-verification bounded-model-checking large-language-models first-order-theorem-prover
-
Updated
Apr 15, 2025 - C
A tool for domain-guided quantifier instantiation. Currently focused on BMC for the array theory.
-
Updated
Jun 12, 2026 - Rust
Prototype implementation of a hyperbug finder for ∀∃-safety hyperproperties to accompany the OOPSLA 2024 paper "Finding ∀∃ Hyperbugs using Symbolic Execution" by Arthur Correnson, Tobias Nießen, Bernd Finkbeiner, and Georg Weissenbacher.
-
Updated
Oct 28, 2024 - C++
A teaching aid for concepts and algorithms in logic
automata logic finite-state-machine temporal-logic logic-programming sat-solver boolean-algebra deterministic ctl bounded-model-checking boolean-logic kripke-structure finite-automata finite-automaton simulation-finite-automaton
-
Updated
Jun 8, 2024 - Java
A random testcase generator for program analysis. Provides a program and its Bounded Model Checking smt-formula
-
Updated
Nov 9, 2018 - C
Towards automatic voting rule argumentation by using computer-aided verification such as software bounded model checking.
-
Updated
Jul 13, 2021 - C
A generic bounded model checker.
minimization ltl model-checking formal-methods modeling-language ctl bounded-model-checking kripke-structure
-
Updated
Oct 18, 2022 - Java
VERIFIER of ACCESS CONTROL
-
Updated
Feb 1, 2020 - C
Technical report on CBMC (C Bounded Model Checker) - Software Engineering II course project - Computer Science @ FAMAF (UNC)
cryptography static-analysis university-project software-engineering formal-verification bounded-model-checking cbmc ctf-writeup famaf
-
Updated
Jun 22, 2025 - TeX
A verification tool used to check some of the distributed properties of Hydra.
-
Updated
Aug 21, 2021
Improve this page
Add a description, image, and links to the bounded-model-checking topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the bounded-model-checking topic, visit your repo's landing page and select "manage topics."