KLEE Symbolic Execution Engine

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

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

Automatic verification of LLVM optimizations

An open source interactive disassembler

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

Symbolic execution engine for .NET Core

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

Static Analysis Course

APISan: Sanitizing API Usages through Semantic Cross-Checking

Teaching and Learning Software Verification via SVF

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)

KLEE-TAINT - Klee with taint analysis support

COIN Attacks: on Insecurity of Enclave Untrusted Interfaces in SGX - ASPLOS 2020

Super Fast Concolic Execution Engine based on Source Code Taint Tracing

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

Sydr benchmark applications

Adaptive Callsite-sensitive Control Flow Integrity - EuroS&P'19