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

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

Automatic verification of LLVM optimizations

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 🚀

Super Fast Concolic Execution Engine based on Source Code Taint Tracing

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

Symbolic Execution Engine based on Ghidra's PCode

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

KLEE-TAINT - Klee with taint analysis support

APISan: Sanitizing API Usages through Semantic Cross-Checking

Symbolic execution engine for .NET Core

Software Security Analysis Course

gradient-based symbolic execution engine implemented from scratch

Teaching and Learning Software Verification via SVF

Code for my blog post on using S2E for malware analysis