A model checker for infinite-state systems.

FuSeBMC is a novel Energy-Efficient Test Generator that exploits fuzzing and BMC engines to detect security vulnerabilities in real-world C programs.

Automated Code Repair suite powered by ESBMC and LLMs.

A bounded model checker for an IMP-style imperative language.

A Symbolic Executor based on Separaton Logic

LSVerifier - Large Systems Verifier

Implementation of bounded model checking in python. (AIGER1.0 support)

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.

Python Package Model Checking Toolkit

Towards automatic voting rule argumentation by using computer-aided verification such as software bounded model checking.

A generic bounded model checker.

VERIFIER of ACCESS CONTROL

A random testcase generator for program analysis. Provides a program and its Bounded Model Checking smt-formula

A teaching aid for concepts and algorithms in logic

Program for helping in the automation of the process of generating input test cases for the code coverage analysis of a set of functions.

A verification tool used to check some of the distributed properties of Hydra.

Verification of Lock-Free Data Structure