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
