Record and Replay Framework

Icarus Verilog

KLEE Symbolic Execution Engine

A minimalistic and high-performance SAT solver

Automatic verification of LLVM optimizations

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.

C Bounded Model Checker

An advanced SAT solver

🦉 A grounder and solver for logic programs.

A fast and accurate disassembler

Simple Theorem Prover, an efficient SMT solver for bitvectors

CaDiCaL SAT Solver

DMTCP: Distributed MultiThreaded CheckPointing

CrashMonkey: tools for testing file-system reliability (OSDI 18)

Generic model checker for concurrent C programs (mirror repository)

A Modern Probabilistic Model Checker

Pono: A flexible and extensible SMT-based model checker

The HW-CBMC and EBMC Model Checkers for Verilog

The opensmt solver

SRI Sally: A model checker for infinite-state systems.

Solver for Constrained Horn Clauses

KORE to llvm translation

CDSChecker: A Model Checker for C11 and C++11 Atomics

[ICSE 2022] Controlled Concurrency Testing via Periodical Scheduling

yet another model checker

Automatic verification of LLVM optimizations

A Small, Extensible DPOR-based Model Checker for C Programs

Model checker for Maude systems controlled by strategies

In this repo, I'm writing SystemC examples ranging from basic to advanced.