Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time

CRETE: Versatile Binary-Level Concolic Testing

Build Status

CRETE is a versatile binary-level concolic testing framework developed by the System Validation Lab at Portland State University. It can be applied to various kinds of software systems for test case generation and bug detection, including proprietary user-level programs, closed-source libraries, kernel modules, etc.


  • Open and extensible architecture: totally decoupled concrete and symbolic execution from virtual machine
  • Standardized execution trace: llvm-based, self-contained, and composable
  • Binary-level analysis: no source code or debug information required
  • In-vivo analysis: use real full software stack and require no environment modeling
  • Compact execution trace: selective binary-level tracing based on Dynamic Taint Analysis
  • Trace/test selection and scheduling algorithms to improve effectiveness
  • Simple usage model: no expertise required and accessible for general users



If you need help with CRETE, or want to discuss the project, you can open new GitHub issues, or contact the maintainer.

We also have a very brief user manual, which contains building instruction, running example, etc.