KLEE is a symbolic virtual machine built on top of the LLVM compiler. KLEE uses symbolic execution to generate tests by constructing the “path conditions” associated with paths through the program and, for each path, using a constraint solver to solve those conditions to generate inputs that would cause the program to follow that path.
Notes related to KLEE verifier
Fuzz testing, S2E verifier, Symbolic execution, Software Testing Competition (Test-Comp), Verification performance of code, Verification profiling of code, Verifier performance
Papers related to KLEE verifier
- BinRec: Dynamic binary lifting and recompilation [altinay:eurosys:2020]
- Automatic exploit generation [avgerinos:cacm:2014]
- A survey of symbolic execution techniques [baldoni:compsurv:2018]
- TestCov: Robust test-suite execution and coverage measurement [beyer:ase:2019]
- Software verification: Testing vs. model checking [beyer:hvc:2017]
- Running symbolic execution forever [busse:issta:2020]
- Symbolic execution for software testing: Three decades later [cadar:cacm:2013]
- Targeted program transformations for symbolic execution [cadar:fse:2015]
- SAVIOR: Towards bug-driven hybrid testing [chen:sp:2020]
- Selective symbolic execution [chipounov:hotdep:2009]
- Verifying systems rules using rule-directed symbolic execution [cui:asplos:2013]
- Evaluating manual intervention to address the challenges of bug finding with KLEE [galea:arxiv:2018]
- TracerX: Dynamic symbolic execution with interpolation [jaffar:arxiv:2020]
- Software model checking [jhala:compsurv:2009]
- A segmented memory model for symbolic execution [kapus:fse:2019]
- Efficient state merging in symbolic execution [kuznetsov:pldi:2012]
- No panic! Verification of Rust programs by symbolic execution [lindner:indin:2018]
- Verification of safety functions implemented in Rust: A symbolic execution based approach [lindner:indin:2019]
- Noninterference via symbolic execution [milushev:forte:2012]
- Deferred concretization in symbolic execution via fuzzing [pandey:issta:2019]
- Symbolic execution with SymCC: Don't interpret, compile! [poeplau:usenix:2020]
- Practical, low-effort equivalence verification of real code [ramos:cav:2011]
- Under-constrained symbolic execution: Correctness checking for real code [ramos:sec:2015]
- Interoperability-guided testing of QUIC implementations using symbolic execution [rath:epiq:2018]
- Methods for binary symbolic execution [romano:phd:2014]
- PG-KLEE: Trading soundness for coverage [rutledge:icse:2020]
- Scaling symbolic execution using ranged analysis [siddiqui:oopsla:2012]
- Chopped symbolic execution [trabish:icse:2018]
- -Overify: Optimizing programs for fast verification [wagner:hotos:2013]
- Boost symbolic execution using dynamic state merging and forking [zhang:apsec:2018]