"KLEE on LC-3," Symbolic Execution Engine for LC-3 Programs

KLEE Symbolic Execution Engine

A symbolic execution engine for x86-32 that allows starting execution from a concrete execution's core dump.

Examples and Programs for Probabilistic Symbolic Execution project. This has been built using KLEE, LLVM, Haskell & python3.

gradient-based symbolic execution engine implemented from scratch

CASM Numeric and Symbolic Interpreter

Prototype implementation of a hyperbug finder for ∀∃-safety hyperproperties to accompany the OOPSLA 2024 paper "Finding ∀∃ Hyperbugs using Symbolic Execution" by Arthur Correnson, Tobias Nießen, Bernd Finkbeiner, and Georg Weissenbacher.

Modified Kirenenko for Constraints Dumping

BubaaK-LEE: A fork of KLEE Symbolic Execution Engine used in the tool Bubaak

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

A tool for detecting Spectre vulnerabilities

Virtual Prototype with symbolic execution support and HardBound path analyzer

A library for concolic execution of RV32 instruction set simulators

A framework for user-guided symbolic execution (with visualization) of LLVM Bitcode. A demo of the project can be viewed at https://www.youtube.com/watch?v=0VNe4BjjF90

Symbolic execution of LLVM IR

Symbolic Liveness Analysis of real-world software building upon KLEE to detect liveness violations (e.g. infinite loop bugs)

Code for my blog post on solving Google's Unbreakable CTF challenge with S2E

Code for my blog post on combining S2E and Kaitai Struct

Data-driven symbolic execution engine, implemented on top of KLEE