> For the complete documentation index, see [llms.txt](https://dev2ero.gitbook.io/notes-cs/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://dev2ero.gitbook.io/notes-cs/cyber-security/xin-xi-an-quan-shi-jian/bug-hunting/lou-dong-wa-jue-ji-shu-gai-shu/fu-hao-zhi-hang/xiang-guan-gong-ju-yu-kuang-jia.md).

# 工具与框架

**Java**

* [JPF-Symbc](https://link.zhihu.com/?target=https%3A//babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc) - Symbolic execution tool built on [Java PathFinder](https://link.zhihu.com/?target=https%3A//babelfish.arc.nasa.gov/trac/jpf/). Supports multiple constraint solvers, lazy initialization, etc.
* [JDart](https://link.zhihu.com/?target=https%3A//github.com/psycopaths/jdart) - Dynamic symbolic execution tool built on [Java PathFinder](https://link.zhihu.com/?target=https%3A//babelfish.arc.nasa.gov/trac/jpf/). Supports multiple constraint solvers using [JConstraints](https://link.zhihu.com/?target=https%3A//github.com/psycopaths/jconstraints).
* [CATG](https://link.zhihu.com/?target=https%3A//github.com/ksen007/janala2) - Concolic execution tool that uses [ASM](https://link.zhihu.com/?target=http%3A//asm.ow2.org/) for instrumentation. Uses CVC4.
* [LimeTB](https://link.zhihu.com/?target=http%3A//www.tcs.hut.fi/Software/lime/) - Concolic execution tool that uses [Soot](https://link.zhihu.com/?target=https%3A//sable.github.io/soot/) for instrumentation. Supports [Yices](https://link.zhihu.com/?target=http%3A//yices.csl.sri.com/) and [Boolector](https://link.zhihu.com/?target=http%3A//fmv.jku.at/boolector/). Concolic execution can be distributed.
* [Acteve](https://link.zhihu.com/?target=https%3A//code.google.com/archive/p/acteve/) - Concolic execution tool that uses [Soot](https://link.zhihu.com/?target=https%3A//sable.github.io/soot/) for instrumentation. Originally for Android analysis. Supports [Z3](https://link.zhihu.com/?target=https%3A//github.com/Z3Prover/z3).
* [jCUTE](https://link.zhihu.com/?target=http%3A//osl.cs.illinois.edu/software/jcute/) - Concolic execution tool that uses [Soot](https://link.zhihu.com/?target=https%3A//sable.github.io/soot/) for instrumentation. Supports [lp\_solve](https://link.zhihu.com/?target=http%3A//lpsolve.sourceforge.net/).
* [JFuzz](https://link.zhihu.com/?target=http%3A//people.csail.mit.edu/akiezun/jfuzz/) - Concolic execution tool built on [Java PathFinder](https://link.zhihu.com/?target=https%3A//babelfish.arc.nasa.gov/trac/jpf/).
* [JBSE](https://link.zhihu.com/?target=http%3A//pietrobraione.github.io/jbse/) - Symbolic execution tool that uses a custom JVM. Supports CVC3, CVC4, Sicstus, and Z3.
* [Key](https://link.zhihu.com/?target=https%3A//www.key-project.org/) - Theorem Prover that uses specifications written in Java Modeling Language (JML).

**LLVM**

* [KLEE](https://link.zhihu.com/?target=http%3A//klee.github.io/) - Symbolic execution engine built on LLVM.
* [Cloud9](https://link.zhihu.com/?target=http%3A//cloud9.epfl.ch/) - Parallel symbolic execution engine built on KLEE.
* [Kite](https://link.zhihu.com/?target=http%3A//www.cs.ubc.ca/labs/isd/Projects/Kite/) - Based on KLEE and LLVM.

**.NET**

* [PEX](https://link.zhihu.com/?target=http%3A//pex4fun.com/About.aspx) - Dynamic symbolic execution tool for .NET.

**C**

* [CREST](https://link.zhihu.com/?target=https%3A//github.com/jburnim/crest).
* [Otter](https://link.zhihu.com/?target=https%3A//bitbucket.org/khooyp/otter/).
* [CIVL](https://link.zhihu.com/?target=http%3A//vsl.cis.udel.edu/civl/) - A framework that includes the CIVL-C programming language, a model checker and a symbolic execution tool.

**JavaScript**

* [Jalangi2](https://link.zhihu.com/?target=https%3A//github.com/Samsung/jalangi2).
* [SymJS](https://link.zhihu.com/?target=https%3A//doi.org/10.1145/2635868.2635913).

**Python**

* [PyExZ3](https://link.zhihu.com/?target=https%3A//github.com/thomasjball/PyExZ3) - Symbolic execution of Python functions. A rewrite of the [NICE](https://link.zhihu.com/?target=https%3A//code.google.com/archive/p/nice-of) project's symbolic execution tool.

**Ruby**

* [Rubyx](https://link.zhihu.com/?target=https%3A//www.cs.umd.edu/~avik/papers/ssarorwa.pdf) - Symbolic execution tool for Ruby on Rails web apps.

**Android**

* [SymDroid](https://link.zhihu.com/?target=http%3A//www.cs.umd.edu/~jfoster/papers/cs-tr-5022.pdf).

**Binaries**

* [Mayhem](https://link.zhihu.com/?target=http%3A//dx.doi.org/10.1109/SP.2012.31).
* [SAGE](https://link.zhihu.com/?target=https%3A//patricegodefroid.github.io/public_psfiles/ndss2008.pdf) - Whitebox file fuzzing tool for X86 Windows applications.
* [DART](https://link.zhihu.com/?target=https%3A//doi.org/10.1145/1064978.1065036).
* [BitBlaze](https://link.zhihu.com/?target=http%3A//bitblaze.cs.berkeley.edu/).
* [PathGrind](https://link.zhihu.com/?target=https%3A//github.com/codelion/pathgrind) - Path-based dynamic analysis for 32-bit programs.
* [FuzzBALL](https://link.zhihu.com/?target=http%3A//bitblaze.cs.berkeley.edu/fuzzball.html) - Symbolic execution tool built on the BitBlaze Vine component.
* [S2E](https://link.zhihu.com/?target=http%3A//s2e.systems/) - Symbolic execution platform supporting x86, x86-64, or ARM software stacks.
* [miasm](https://link.zhihu.com/?target=https%3A//github.com/cea-sec/miasm) - Reverse engineering framework. Includes symbolic execution.
* [pysymemu](https://link.zhihu.com/?target=https%3A//github.com/feliam/pysymemu/) - Supports x86/x64 binaries.
* [BAP](https://link.zhihu.com/?target=https%3A//github.com/BinaryAnalysisPlatform/bap) - Binary Analysis Platform provides a framework for writing program analysis tools.
* [angr](https://link.zhihu.com/?target=http%3A//angr.io/) - Python framework for analyzing binaries. Includes a symbolic execution tool.
* [Triton](https://link.zhihu.com/?target=https%3A//triton.quarkslab.com/) - Dynamic binary analysis platform that includes a dynamic symbolic execution tool.
* [manticore](https://link.zhihu.com/?target=https%3A//github.com/trailofbits/manticore) - Symbolic execution tool for binaries (x86, x86\_64 and ARMV7) and Ethereum smart contract bytecode.

**Misc**

* [Symbooglix](https://link.zhihu.com/?target=https%3A//github.com/symbooglix/symbooglix) - Symbolic execution tool for Boogie programs.