GitHub topics: bounded-model-checking
esbmc/esbmc-ai
Automated Code Repair suite powered by ESBMC and LLMs.
Language: C - Size: 1.74 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 34 - Forks: 5
adilanwar2399/ESBMC-ibmc
The ESBMC ibmc (Invariant Based Model Checking) Tool.
Language: C - Size: 327 KB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 6 - Forks: 1
SRI-CSL/sally
A model checker for infinite-state systems.
Language: C++ - Size: 5.61 MB - Last synced at: 17 days ago - Pushed at: 4 months ago - Stars: 74 - Forks: 13
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
kaled-alshmrany/FuSeBMC
FuSeBMC is a novel Energy-Efficient Test Generator that exploits fuzzing and BMC engines to detect security vulnerabilities in real-world C programs.
Language: C - Size: 86.6 MB - Last synced at: 5 months ago - Pushed at: about 1 year ago - Stars: 46 - Forks: 6
tniessen/hyena0
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.
Language: C++ - Size: 52.7 KB - Last synced at: about 1 month ago - Pushed at: 6 months ago - Stars: 2 - Forks: 0
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
marcusm117/mctk
Python Package Model Checking Toolkit
Language: Python - Size: 2.74 MB - Last synced at: 27 days ago - Pushed at: about 1 year ago - Stars: 5 - Forks: 0
danielbinder/LogiVis
A teaching aid for concepts and algorithms in logic
Language: Java - Size: 15.5 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 2 - Forks: 0
yepengding/Kiwami
A generic bounded model checker.
Language: Java - Size: 90.8 KB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0
porglezomp/hyalite
A bounded model checker for an IMP-style imperative language.
Language: Rust - Size: 10.7 KB - Last synced at: 21 days ago - Pushed at: about 6 years ago - Stars: 7 - Forks: 0
dj-d/VoLFDS
Verification of Lock-Free Data Structure
Language: Python - Size: 314 KB - Last synced at: about 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
SpencerL-Y/SESL
A Symbolic Executor based on Separaton Logic
Language: SWIG - Size: 76.5 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 6 - Forks: 0
mi-ki/cardCryptoVerification
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.
Language: C - Size: 43 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 3 - Forks: 1
mi-ki/voting-rule-argumentation
Towards automatic voting rule argumentation by using computer-aided verification such as software bounded model checking.
Language: C - Size: 6.32 MB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 2 - Forks: 1
spencerwuwu/benchmark-generator
A random testcase generator for program analysis. Provides a program and its Bounded Model Checking smt-formula
Language: C - Size: 33.2 KB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 1
trucnguyenlam/vac
VERIFIER of ACCESS CONTROL
Language: C - Size: 177 MB - Last synced at: over 1 year ago - Pushed at: about 5 years ago - Stars: 2 - Forks: 1
JordiROP/Automatic-Test-Case-Generation-With-CMBC
Program for helping in the automation of the process of generating input test cases for the code coverage analysis of a set of functions.
Language: Python - Size: 9.77 KB - Last synced at: about 2 years ago - Pushed at: almost 7 years ago - Stars: 0 - Forks: 0
