Triton is a dynamic binary analysis library. Build your own program analysis tools, automate your reverse engineering, perform software verification or just emulate code.

KLEE Symbolic Execution Engine

IDA 2016 plugin contest winner! Symbolic Execution just one-click away!

An open source interactive disassembler

Automatic verification of LLVM optimizations

Angora is a mutation-based fuzzer. The main goal of Angora is to increase branch coverage by solving path constraints without symbolic execution.

Simple Theorem Prover, an efficient SMT solver for bitvectors

Tool that generates unit test by C/C++ source code, trying to reach all branches and maximize code coverage

Fuzzing tutorial with easy-to-learn labs 🚀

The exploit generator CRAX++ is CRAX with a plugin system, s2e 2.0 upgrade, dynamic ROP, code selection, and I/O states (HITCON 2022)

Super Fast Concolic Execution Engine based on Source Code Taint Tracing

Symbolic Execution Engine based on Ghidra's PCode

TTexplore is a library that performs path exploration on binary code using symbolic execution

Static Analysis Course

KLEE-TAINT - Klee with taint analysis support

APISan: Sanitizing API Usages through Semantic Cross-Checking

Symbolic execution engine for .NET Core

gradient-based symbolic execution engine implemented from scratch

Teaching and Learning Software Verification via SVF

A concolic testing engine for RISC-V embedded software with support for SystemC peripherals