Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of functions by generating (succinct) first-order verification conditions.

A monadic library for symbolic evaluation

Python infrastructure to train paths selectors for symbolic execution engines.

A symbolic execution engine for EVM smart contract binaries

Automatic verification of LLVM optimizations

Symbolic-execution-based verifier for the Viper intermediate verification language.

A platform for analysis of Java bytecode

Software Security Analysis Course

Binary Analysis Platform

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

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

A symbolic execution tool for Move, which is a smart contract language designed for Facebook Diem.

Universal Symbolic Virtual Machine

"This repository focuses on implementing Compiler-Related concepts."

DIG is a numerical invariant generation tool. It infers program invariants or properties over (i) program execution traces or (ii) program source code. DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations.

A Guix channel for reproducible symbolic execution research

Use angr in Ghidra

OSS-Sydr-Fuzz - OSS-Fuzz fork for hybrid fuzzing (fuzzer+DSE) open source software.

Teaching and Learning Software Verification via SVF