cbmc

Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).

AProver: Agentic Prover for AI-Generated Code — LLM agents + BMC for automated verification of systems software

Fuzzing Lua runtimes without pain

This repo investigates Chrome's Verified Boot (Vboot) through C Bounded Model Checker (CBMC) and the use of the Software TPM library

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.

BEAST aims to make the verification of voting rules easier

Bounded model checking on lock free data structure

這是一個用於麥塊匿名發文平台的 npm package。

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

SKILL.md-standard proofreading skill — code & document review with real, verified formal-verification backends for C, Python, Rust, Java, and C++

Technical report on CBMC (C Bounded Model Checker) - Software Engineering II course project - Computer Science @ FAMAF (UNC)

Theory notes, exercises, and project - Software Engineering II course - Computer Science @ FAMAF (UNC)

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

Expediting verification of assertions in loops by isolation

Encoding Vesicle Traffic System in Z3 and CBMC

AI-native Code-OSS workbench for safety-critical firmware. DO-178C evidence, MISRA, CBMC, CodeQL, measured MC/DC and hardware tooling in one window — with compliance runs that record what was actually measured, and claim nothing else.

Contains a common interface for software analyzers/verifiers/test-suites (also known as oracles)

Verification of Lock-Free Data Structure

An unofficial 麥塊匿名發文平台 API wrapper.