An open API service providing repository metadata for many open source software ecosystems.

GitHub topics: symbolic-execution

SVF-tools/Software-Security-Analysis

Static Analysis Course

Language: C++ - Size: 75.1 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 73 - Forks: 28

klee/klee

KLEE Symbolic Execution Engine

Language: C++ - Size: 9.02 MB - Last synced at: 2 days ago - Pushed at: 3 days ago - Stars: 2,799 - Forks: 697

BillHallahan/G2

Language: Haskell - Size: 60.6 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 37 - Forks: 7

supra-nlpn/FuSS

This repository contains the full implementation of FuSS (Firmware-based Symbolic-guided SoC Fuzzing)

Language: Python - Size: 91.6 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 1 - Forks: 0

UnitTestBot/usvm

Universal Symbolic Virtual Machine

Language: Kotlin - Size: 134 MB - Last synced at: 3 days ago - Pushed at: 4 days ago - Stars: 24 - Forks: 25

ConsenSysDiligence/mythril

Mythril is a symbolic-execution-based securty analysis tool for EVM bytecode. It detects security vulnerabilities in smart contracts built for Ethereum and other EVM-compatible blockchains.

Language: Python - Size: 47.4 MB - Last synced at: 3 days ago - Pushed at: about 1 month ago - Stars: 4,062 - Forks: 778

GaloisInc/grease

CLI tool, Ghidra plug-in, and Haskell library for analyzing binaries using under-constrained symbolic execution

Language: Haskell - Size: 1.61 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 119 - Forks: 7

ispras/oss-sydr-fuzz

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

Language: C - Size: 12 MB - Last synced at: 5 days ago - Pushed at: 6 days ago - Stars: 138 - Forks: 37

HarvardPL/formulog

Datalog with support for SMT queries and first-order functional programming

Language: Java - Size: 2.94 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 158 - Forks: 10

OCamlPro/owi

Symbolic execution for Wasm, C, C++, Rust and Zig

Language: OCaml - Size: 20.1 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 235 - Forks: 34

katamaran-project/katamaran

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.

Language: Rocq Prover - Size: 6.6 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 18 - Forks: 4

metagon/ithildin

Semantic analyzer of EVM bytecode based on Mythril

Language: Python - Size: 172 KB - Last synced at: 5 days ago - Pushed at: over 4 years ago - Stars: 10 - Forks: 3

Generative-Program-Analysis/GenSym

A high-performance, parallel, compilation-based symbolic execution engine

Language: Java - Size: 21.5 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 131 - Forks: 5

PySymGym/PySymGym

Python infrastructure to train paths selectors for symbolic execution engines.

Language: Python - Size: 13.3 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 6 - Forks: 2

viperproject/silicon

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

Language: Scala - Size: 39.5 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 108 - Forks: 36

formalsec/smtml

An SMT solver frontend for OCaml

Language: OCaml - Size: 2.83 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 42 - Forks: 12

csvl/SEMA

SEMA is based on angr, a symbolic execution engine used to extract API calls. Especially, we extend ANGR with strategies to create representative signatures based on System Call Dependency graph (SCDG). Those SCDGs can be exploited in machine learning modules to do classification/detection.

Language: Python - Size: 1.42 GB - Last synced at: 9 days ago - Pushed at: 4 months ago - Stars: 115 - Forks: 23

GaloisInc/MATE

MATE is a suite of tools for interactive program analysis with a focus on hunting for bugs in C and C++ code using Code Property Graphs.

Language: Python - Size: 117 MB - Last synced at: 9 days ago - Pushed at: over 2 years ago - Stars: 192 - Forks: 12

jordan9001/dobby2

Build your emulation environment as needed

Language: Python - Size: 495 KB - Last synced at: 2 days ago - Pushed at: about 4 years ago - Stars: 67 - Forks: 10

AliveToolkit/alive2

Automatic verification of LLVM optimizations

Language: C++ - Size: 6.32 MB - Last synced at: 23 days ago - Pushed at: 23 days ago - Stars: 917 - Forks: 122

etiams/supercompilation-resources

๐Ÿ“š A collection of resources about supercompilation

Size: 19.5 KB - Last synced at: 23 days ago - Pushed at: 23 days ago - Stars: 1 - Forks: 0

stp/stp

Simple Theorem Prover, an efficient SMT solver for bitvectors

Language: C++ - Size: 33.1 MB - Last synced at: 4 days ago - Pushed at: 10 months ago - Stars: 545 - Forks: 142

JonathanSalwan/Triton

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

Language: C++ - Size: 57.1 MB - Last synced at: 23 days ago - Pushed at: about 2 months ago - Stars: 3,777 - Forks: 550

Thanh-WuTan/YAN85-SymbolicExecutionToolkit

A Python tool using Angr for symbolic execution to deobfuscate YAN85 binaries, auto-identifying registers, opcodes, and syscalls. Includes an autoassembler to generate shellcode from readable code.

Language: Python - Size: 78.1 KB - Last synced at: 24 days ago - Pushed at: 24 days ago - Stars: 11 - Forks: 0

ksluckow/awesome-symbolic-execution

A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.

Size: 49.8 KB - Last synced at: 24 days ago - Pushed at: 24 days ago - Stars: 1,411 - Forks: 142

kyle-elliott/DVM

Symbolic Execution based on lifting amd64 to z3

Language: C# - Size: 55.7 KB - Last synced at: 11 days ago - Pushed at: about 1 year ago - Stars: 28 - Forks: 2

quarkslab/pastis

PASTIS: Collaborative Fuzzing Framework

Language: Python - Size: 63.4 MB - Last synced at: 4 days ago - Pushed at: 2 months ago - Stars: 162 - Forks: 10

yuawn/Fuzzing

Fuzzing tutorial with easy-to-learn labs ๐Ÿš€

Language: C++ - Size: 78.1 KB - Last synced at: 7 days ago - Pushed at: almost 3 years ago - Stars: 161 - Forks: 18

lsrcz/grisette

A monadic library for symbolic evaluation

Language: Haskell - Size: 35.9 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 67 - Forks: 3

UnitTestBot/UTBotJava

Automated unit test generation and precise code analysis for Java

Language: Kotlin - Size: 204 MB - Last synced at: 9 days ago - Pushed at: about 1 year ago - Stars: 139 - Forks: 46

d4em0n/exrop ๐Ÿ“ฆ

Automatic ROPChain Generation

Language: Python - Size: 1.39 MB - Last synced at: 2 days ago - Pushed at: over 5 years ago - Stars: 288 - Forks: 22

pschanely/CrossHair

An analysis tool for Python that blurs the line between testing and type systems.

Language: Python - Size: 4.96 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 1,162 - Forks: 61

illera88/Ponce

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

Language: C++ - Size: 332 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 1,546 - Forks: 78

palkeo/pakala

Offensive vulnerability scanner for ethereum, and symbolic execution tool for the Ethereum Virtual Machine

Language: Python - Size: 204 KB - Last synced at: 19 days ago - Pushed at: about 3 years ago - Stars: 344 - Forks: 30

SVF-tools/Teaching-Software-Verification

Teaching and Learning Software Verification via SVF

Language: C++ - Size: 10.8 MB - Last synced at: about 1 month ago - Pushed at: about 2 months ago - Stars: 34 - Forks: 23

season-lab/fuzzolic

fuzzing + concolic = fuzzolic :)

Language: C - Size: 23.6 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 121 - Forks: 7

LEAFERx/Movable

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

Language: Rust - Size: 387 KB - Last synced at: 3 days ago - Pushed at: about 1 year ago - Stars: 2 - Forks: 0

JonathanSalwan/VMProtect-devirtualization

Playing with the VMProtect software protection. Automatic deobfuscation of pure functions using symbolic execution and LLVM.

Language: Roff - Size: 28.1 MB - Last synced at: about 2 months ago - Pushed at: about 3 years ago - Stars: 1,252 - Forks: 195

BinaryAnalysisPlatform/bap

Binary Analysis Platform

Language: OCaml - Size: 8.21 MB - Last synced at: about 2 months ago - Pushed at: 2 months ago - Stars: 2,136 - Forks: 277

cea-sec/miasm

Reverse engineering framework in Python

Language: Python - Size: 16.5 MB - Last synced at: about 2 months ago - Pushed at: 6 months ago - Stars: 3,666 - Forks: 479

JonathanSalwan/Tigress_protection

Playing with the Tigress software protection. Break some of its protections and solve their reverse engineering challenges. Automatic deobfuscation using symbolic execution, taint analysis and LLVM.

Language: LLVM - Size: 13.1 MB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 831 - Forks: 145

ergrelet/themida-unmutate

Static deobfuscator for Themida, WinLicense and Code Virtualizer 3.x's mutation-based obfuscation.

Language: Python - Size: 1.1 MB - Last synced at: about 2 months ago - Pushed at: 12 months ago - Stars: 281 - Forks: 25

0xM3R/cgPwn

A lightweight VM for hardware hacking, RE (fuzzing, symEx, exploiting etc) and wargaming tasks

Language: Shell - Size: 10.7 KB - Last synced at: about 2 months ago - Pushed at: almost 6 years ago - Stars: 357 - Forks: 59

trailofbits/manticore

Symbolic execution tool

Language: Python - Size: 43.5 MB - Last synced at: about 2 months ago - Pushed at: almost 2 years ago - Stars: 3,760 - Forks: 479

enzet/symbolic-execution

History of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)

Language: Kotlin - Size: 14.9 MB - Last synced at: about 2 months ago - Pushed at: 11 months ago - Stars: 493 - Forks: 56

bdcht/amoco

yet another tool for analysing binaries

Language: Python - Size: 3.18 MB - Last synced at: about 2 months ago - Pushed at: 5 months ago - Stars: 483 - Forks: 64

SoftSec-KAIST/MeanDiff

Testing Intermediate Representations for Binary Analysis (ASE '17)

Language: F# - Size: 369 KB - Last synced at: 7 days ago - Pushed at: over 6 years ago - Stars: 80 - Forks: 11

ispras/crusher

Language: Python - Size: 32 MB - Last synced at: 3 days ago - Pushed at: 4 days ago - Stars: 39 - Forks: 17

ExpoSEJS/ExpoSE

A Dynamic Symbolic Execution (DSE) engine for JavaScript. ExpoSE is highly scalable, compatible with recent JavaScript standards, and supports symbolic modelling of strings and regular expressions.

Language: JavaScript - Size: 12.1 MB - Last synced at: 2 months ago - Pushed at: 6 months ago - Stars: 202 - Forks: 40

brocbyte/brocstruct

Ghidra plugin for automatic struct definition extraction from executables.

Language: Java - Size: 49.8 KB - Last synced at: about 1 month ago - Pushed at: 7 months ago - Stars: 1 - Forks: 0

ercoppa/symbolic-execution-tutorial

Tutorial on Symbolic Execution. Hands-on session is based on the angr framework.

Language: Python - Size: 2.92 MB - Last synced at: 7 days ago - Pushed at: about 4 years ago - Stars: 132 - Forks: 18

huchenxucs/ChatDB

The official repository of "ChatDB: Augmenting LLMs with Databases as Their Symbolic Memory".

Language: Python - Size: 369 KB - Last synced at: 2 months ago - Pushed at: about 2 years ago - Stars: 576 - Forks: 52

SQLab/CRAXplusplus

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

Language: C++ - Size: 4.18 MB - Last synced at: 8 days ago - Pushed at: over 2 years ago - Stars: 102 - Forks: 15

Abbass21/Craxs

LICENSE

Size: 2.93 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

yk0112/SpecOrder

A tool for detecting Spectre vulnerabilities

Language: C++ - Size: 1.55 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

borzacchiello/seninja

symbolic execution plugin for binary ninja

Language: Python - Size: 2.34 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 320 - Forks: 24

mdsakibanwar/gosonar

Binary symbolic execution for detecting uncontrolled recursion in Go binaries. Published at IEEE S&P 2025.

Language: Python - Size: 6.94 MB - Last synced at: 2 months ago - Pushed at: 3 months ago - Stars: 1 - Forks: 0

ispras/juliet-dynamic

Juliet C/C++ Dynamic Test Suite

Size: 38.7 MB - Last synced at: about 1 month ago - Pushed at: about 2 years ago - Stars: 29 - Forks: 7

dynaroars/dig

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.

Language: Python - Size: 80.8 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 41 - Forks: 6

andreafioraldi/IDAngr

Use angr in the IDA Pro debugger generating a state from the current debug session

Language: Python - Size: 30.1 MB - Last synced at: 2 months ago - Pushed at: almost 5 years ago - Stars: 277 - Forks: 31

hanshibo001213/kleedebuggger

VS Code Debugger Extension for KLEE Symbolic Execution Engine

Language: TypeScript - Size: 52.1 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

thisisnotgcsar/ODC_23-24-CTFs

All CTFs solved in Offensive and Defensive Cyber Security course of Polytechnic of Milan 23/24 edition

Language: Python - Size: 12.1 MB - Last synced at: 8 days ago - Pushed at: 9 months ago - Stars: 2 - Forks: 0

ergrelet/themida-unmutate-bn

A Binary Ninja plugin to deobfuscate Themida, WinLicense and Code Virtualizer 3.x's mutation-based obfuscation.

Language: Python - Size: 27.3 KB - Last synced at: 3 months ago - Pushed at: 12 months ago - Stars: 29 - Forks: 3

trailofbits/deepstate

A unit test-like interface for fuzzing and symbolic execution

Language: Python - Size: 1.44 MB - Last synced at: about 2 months ago - Pushed at: 6 months ago - Stars: 831 - Forks: 97

mazeppa-dev/mazeppa

A modern supercompiler for call-by-value functional languages

Language: OCaml - Size: 664 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 407 - Forks: 9

farosato/angr-antievasion

Final project for the M.Sc. in Engineering in Computer Science at Universitร  degli Studi di Roma "La Sapienza" (A.Y. 2016/2017).

Language: Python - Size: 1.94 MB - Last synced at: 7 days ago - Pushed at: over 7 years ago - Stars: 34 - Forks: 7

crytic/optik

Optik is a set of symbolic execution tools that assist smart-contract fuzzers

Language: Python - Size: 594 KB - Last synced at: 2 months ago - Pushed at: 10 months ago - Stars: 94 - Forks: 12

ucsb-seclab/greed

A symbolic execution engine for EVM smart contract binaries.

Language: Python - Size: 10.1 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 104 - Forks: 16

tukcps/AADD

This repository holds the Affine Arithmetic Decision Diagrams library

Language: C++ - Size: 379 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 7 - Forks: 2

sbhakim/ansr-dt

ANSR-DT: An open-source Adaptive Neuro-Symbolic framework for real-time learning and reasoning in Digital Twins. Combines CNN-LSTM, reinforcement learning, and symbolic reasoning for interpretable, adaptive decision-making.

Language: Python - Size: 41.6 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 1 - Forks: 1

FuzzingLabs/thoth

Cairo/Starknet security toolkit (bytecode analyzer, disassembler, decompiler, symbolic execution, SBMC)

Language: Python - Size: 5.63 MB - Last synced at: 3 months ago - Pushed at: 6 months ago - Stars: 254 - Forks: 23

Ivan-Klikovac/symexec

A symbolic execution engine that works on GCC's SSA GIMPLE

Language: C++ - Size: 20.5 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

sjmikler/pytorch-symbolic

Symbolic API for model creation in PyTorch.

Language: Jupyter Notebook - Size: 5.39 MB - Last synced at: 21 days ago - Pushed at: 4 months ago - Stars: 66 - Forks: 3

sdasgup3/binary-decompilation

Extracting high level semantic information from binary code

Language: Assembly - Size: 244 MB - Last synced at: 3 months ago - Pushed at: about 6 years ago - Stars: 65 - Forks: 8

staticafi/symbiotic

Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE

Language: Python - Size: 2.13 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 320 - Forks: 57

JonathanSalwan/ttexplore

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

Language: C++ - Size: 552 KB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 76 - Forks: 7

mttcrn/ODC-challenges

CTF challenges taken during the course of "Offensive & Defensive Cybersecurity" - Polimi Computer Science Engineering - A.Y. 2024/2025.

Language: Python - Size: 32.5 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

open-crs/vulnerability_detection

Module for discovering vulnerabilities in executables ๐Ÿงจ

Language: Python - Size: 1.57 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 4 - Forks: 1

catseye/SixtyPical

MIRROR of https://codeberg.org/catseye/SixtyPical : A 6502-oriented low-level programming language supporting advanced static analysis

Language: Python - Size: 1010 KB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 33 - Forks: 3

Kraks/sai

Staged Abstract Interpreters

Language: Scala - Size: 18.1 MB - Last synced at: 12 days ago - Pushed at: over 2 years ago - Stars: 66 - Forks: 8

PLSysSec/sys

Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code

Language: LLVM - Size: 4.55 MB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 227 - Forks: 41

MrRhuezzler/delta-dx

A Symbolic Differentiator

Language: Python - Size: 181 KB - Last synced at: 25 days ago - Pushed at: over 3 years ago - Stars: 5 - Forks: 0

agra-uni-bremen/symex-vp

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

Language: C++ - Size: 31.7 MB - Last synced at: 3 months ago - Pushed at: almost 2 years ago - Stars: 23 - Forks: 5

pfnet-research/ATPG4SV

A prototype of Concolic Testing engine for SystemVerilog, developed as part of PFN summer internship 2018.

Language: OCaml - Size: 40 KB - Last synced at: 3 months ago - Pushed at: over 6 years ago - Stars: 18 - Forks: 2

AngoraFuzzer/Angora

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

Language: C++ - Size: 13 MB - Last synced at: 3 months ago - Pushed at: almost 3 years ago - Stars: 941 - Forks: 170

casm-lang/casmi ๐Ÿ“ฆ

CASM Numeric and Symbolic Interpreter

Language: C++ - Size: 495 KB - Last synced at: 6 days ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

mgree/smoosh

The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.

Language: OCaml - Size: 3.66 MB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 118 - Forks: 5

zyedidia/rvsym

A small RISC-V symbolic execution engine

Language: Go - Size: 523 KB - Last synced at: 3 months ago - Pushed at: almost 3 years ago - Stars: 8 - Forks: 0

cleanunicorn/karl

Monitor smart contracts deployed on blockchain and test against vulnerabilities with Mythril. It was presented at DEFCON 2019.

Language: Python - Size: 4.3 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 318 - Forks: 78

tukcps/jAADD

This repository holds the Affine Arithmetic Decision Diagrams library written for Java and JVM languages http://cps.cs.uni-kl.de/en/AADD

Language: Kotlin - Size: 1.26 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 2 - Forks: 2

crytic/etheno ๐Ÿ“ฆ

Simplify Ethereum security analysis and testing

Language: Python - Size: 738 KB - Last synced at: 27 days ago - Pushed at: 5 months ago - Stars: 340 - Forks: 33

UCLA-SEAL/NaturalSym

FSE 2024: Natural Symbolic Execution-based Testing for Big Data Analytics

Language: Java - Size: 608 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 1 - Forks: 0

Robbepop/stevia

A simple (unfinished) SMT solver for QF_ABV.

Language: Rust - Size: 1.38 MB - Last synced at: about 13 hours ago - Pushed at: over 6 years ago - Stars: 36 - Forks: 5

redtrama/awesome-halmos

List of Halmos resources.

Size: 27.3 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 53 - Forks: 7

kotcrab/mist

MIPS disassembler, symbolic execution engine, recompiler and decompiler focusing on the Allegrex CPU

Language: Kotlin - Size: 974 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 8 - Forks: 2

tracer-x/TracerX

TracerX Symbolic Virtual Machine

Language: C - Size: 209 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 33 - Forks: 11

filipeom/wasm-se-bench

Benchmarking Symbolic Execution tools for Wasm

Language: Python - Size: 126 KB - Last synced at: 4 months ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0

binsec/Rel

Binsec/Rel is an extension of Binsec that implements relational symbolic execution for constant-time verification and secret-erasure at binary-level.

Language: OCaml - Size: 1.01 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 33 - Forks: 2

JonathanSalwan/X-Tunnel-Opaque-Predicates

IDA+Triton plugin in order to extract opaque predicates using a Forward-Bounded DSE. Example with X-Tunnel.

Language: Python - Size: 83 KB - Last synced at: 3 months ago - Pushed at: almost 6 years ago - Stars: 52 - Forks: 16

Slava0135/gobber

Go symbolic execution (Z3 SMT solver)

Language: Go - Size: 137 KB - Last synced at: 4 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0