Showing 16 of 16 projects
A high-performance theorem prover and satisfiability modulo theories (SMT) solver from Microsoft Research.
A platform-agnostic binary analysis framework for disassembly, symbolic execution, and program analysis.
A symbolic-execution-based security analysis tool for detecting vulnerabilities in Ethereum and EVM-compatible smart contracts.
A dynamic binary analysis library for building program analysis tools, automating reverse engineering, and emulating code.
A suite of utilities and libraries for analyzing binary programs, supporting multiple architectures and offering symbolic execution.
A Python framework for disassembly, static analysis, symbolic execution, and debugging of binaries and malware.
A mutation-based coverage-guided fuzzer that increases branch coverage by solving path constraints without symbolic execution.
A formal semantics of the Ethereum Virtual Machine (EVM) written in the K framework, enabling verification and symbolic execution of smart contracts.
A symbolic model checker for TLA+ and Quint specifications, translating them into SMT constraints for verification.
A security analysis framework for WebAssembly modules and blockchain smart contracts (BTC/ETH/NEO/EOS).
A modern supercompiler for call-by-value functional languages that transforms programs via symbolic evaluation and metasystem transitions.
An automatic bug-finding tool for C, C++, Go, Rust, and Zig using WebAssembly-level symbolic execution.
A static and symbolic analysis tool for finding memory safety bugs in browser code and other software.
A toolkit for extracting and simplifying virtualized binary code from 32-bit execution traces.
A concolic unit testing engine for Java programs that combines concrete and symbolic execution to generate test inputs.
A multi-backend SMT solver frontend for OCaml providing a consistent interface to various solvers.
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.