Tool Talk: KLEE
summary
KLEE is an open source dynamic symbolic execution engine that runs on LLVM bitcode for C/C++ and claims concrete-test generation that actually triggers bugs. It models memory with an object level copy and write schema and holds tens of thousands of paths in memory simultaneously. Solvers offered include STP and C3 (with bindings to others), release 2.1 ships March, and mainline lacks threading while Cloud9 adds pthreads support.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 0:20Dynamic Symbolic Execution
- 2:00KLEE
- 3:22Impact
- 4:36Getting Started
- 8:29Workshop
- 8:57Questions
related talks
14mCompatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
51mCompile-time tools supporting generic programming in C++
42mMeta-programming with K2 compiler plugins
53mLocknote: How Badly Do We Want Correct Compilers?
24mKeystone Engine: Next Generation Assembler Framework
22mBoosting Compiler Testing by Injecting Real-World Code
01h 04mLean4Lean: Mechanizing the Metatheory of Lean
16mCompiling Symbolic Execution with Staging and Algebraic Effects