Editing Symbolic execution (section)

==Tools==
{| class="wikitable sortable"
|-
! Tool
! Target
! URL
! Can anybody use it/ Open source/ Downloadable
|-
| angr
| libVEX based (supporting x86, x86-64, ARM, AARCH64, MIPS, MIPS64, PPC, PPC64, and Java)
| http://angr.io/
| {{free | yes}} 
|-
| BE-PUM
| x86
| https://github.com/NMHai/BE-PUM
| {{free | yes}} 
|-
|BINSEC
|x86, ARM, RISC-V (32 bits)
|http://binsec.github.io
| {{free | yes}}
|-
|crucible
|LLVM, JVM, etc
|https://github.com/GaloisInc/crucible
| {{free | yes}} 
|-
| ExpoSE
| [[JavaScript]]
| https://github.com/ExpoSEJS/ExpoSE
| {{free | yes}} 
|-
| FuzzBALL
| VineIL / Native
| http://bitblaze.cs.berkeley.edu/fuzzball.html
| {{free | yes}} 
|-
| GenSym
| LLVM
| https://github.com/Generative-Program-Analysis/GenSym
| {{free | yes}} 
|-
| Jalangi2
| [[JavaScript]]
| https://github.com/Samsung/jalangi2
| {{free | yes}} 
|-
| janala2
|Java
| https://github.com/ksen007/janala2
| {{free | yes}} 
|-
| JaVerT
| [[JavaScript]]
| https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2019JaVerT.pdf
| {{free | yes}}
|-
| JBSE
|Java
| https://github.com/pietrobraione/jbse
| {{free | yes}} 
|-
| jCUTE
|Java
| https://github.com/osl/jcute
| {{free | yes}} 
|-
| KeY
|Java
| http://www.key-project.org/
| {{free | yes}} 
|-
| Kite
| LLVM
| http://www.cs.ubc.ca/labs/isd/Projects/Kite/
| {{free | yes}} 
|-
| KLEE
| LLVM
| https://klee.github.io/
| {{free | yes}} 
|-
| Kudzu
| [[JavaScript]]
| http://webblaze.cs.berkeley.edu/2010/kudzu/kudzu.pdf
| {{proprietary|no}}
|-
|MPro
|[[Ethereum#Virtual machine|Ethereum Virtual Machine (EVM)]] / Native
|https://sites.google.com/view/smartcontract-analysis/home
| {{free | yes}} 
|-
| Maat
| Ghidra P-code / SLEIGH
| https://maat.re/
| {{free | yes}} 
|-
| Manticore
| x86-64, ARMv7, [[Ethereum#Virtual machine|Ethereum Virtual Machine (EVM)]] / Native
| https://github.com/trailofbits/manticore/
| {{free | yes}} 
|-
| Mayhem
| Binary
| http://forallsecure.com
| {{proprietary|no}}
|-
| Mythril
| [[Ethereum#Virtual machine|Ethereum Virtual Machine (EVM)]] / Native
| https://github.com/ConsenSys/mythril
| {{free | yes}} 
|-
| Otter
| C
| https://bitbucket.org/khooyp/otter/overview
| {{free | yes}} 
|-
| Owi <ref>{{Cite journal
| doi = 10.22152/programming-journal.org/2025/9/3
| year = 2024
| last1 = Andrès
| first1 = Léo
| title = Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly
| journal = The Art, Science, and Engineering of Programming
| volume= 9
| arxiv= 2412.06391
| url = https://programming-journal.org/2025/9/3/
}}</ref>
| [[C (programming language)|C]], [[C++]], [[Rust (programming language)|Rust]], [[WebAssembly]], [[Zig (programming language)|Zig]]
| https://github.com/ocamlpro/owi
| {{free | yes}} 
|-
| Oyente-NG
| [[Ethereum#Virtual machine|Ethereum Virtual Machine (EVM)]] / Native
| http://www.comp.ita.br/labsca/waiaf/papers/RafaelShigemura_paper_16.pdf
| {{proprietary | no}}
|-
| Pathgrind<ref>{{Cite book
| chapter= Exploiting Undefined Behaviors for Efficient Symbolic Execution
| title=ICSE Companion 2014: Companion Proceedings of the 36th International Conference on Software Engineering
| pages = 727–729
| doi = 10.1145/2591062.2594450
| year = 2014
| last1 = Sharma
| first1 = Asankhaya
| s2cid=10092664
| isbn = 9781450327688
}}</ref>
| Native 32-bit Valgrind-based
| https://github.com/codelion/pathgrind
| {{free | yes}} 
|-
| Pex
| [[.NET Framework]]
| http://research.microsoft.com/en-us/projects/pex/
| {{proprietary|no}}
|-
| pysymemu
| x86-64 / Native
| https://github.com/feliam/pysymemu/
| {{free | yes}} 
|-
| Rosette
| Dialect of [[Racket (programming language)|Racket]]
| https://emina.github.io/rosette/
| {{free | yes}} 
|-
| Rubyx
| [[Ruby (programming language)|Ruby]]
| http://www.cs.umd.edu/~avik/papers/ssarorwa.pdf
| {{proprietary|no}}
|-
| S2E
| x86, x86-64, ARM / User and kernel-mode binaries
| http://s2e.systems/
| {{free | yes}} 
|-
| Symbolic PathFinder (SPF)
| Java Bytecode
| https://github.com/SymbolicPathFinder
| {{free|yes}} 
|-
| SymDroid
| [[Dalvik (software)|Dalvik]] bytecode
| http://www.cs.umd.edu/~jfoster/papers/symdroid.pdf
| {{proprietary|no}}
|-
| SymJS
| [[JavaScript]]
| https://core.ac.uk/download/pdf/24067593.pdf
| {{proprietary|no}}
|-
| SymCC
| LLVM
| https://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
| {{free | yes}} 
|-
| Triton
| x86, x86-64, ARM and AArch64
| https://triton.quarkslab.com
| {{free | yes}} 
|-
| Verifast
| C, Java
| https://people.cs.kuleuven.be/~bart.jacobs/verifast
| {{free | yes}}
|-
|}