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.

LSVerifier - Large Systems Verifier

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

A Symbolic Executor based on Separaton Logic

Implementation of bounded model checking with Z3py. (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

ESBMC ibmc tool code for the Paper LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling.

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

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.

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