GKLEE is a concolic verifier-cum-analyzer for CUDA (Compute Unified Device Architecture) C/C++ programs that are typically executed on GPUs (Graphical Processing Unit). GKLEE actually analyzes whole programs, which means that it verifies the 'main' (CPU) program together with the collection of GPU kernel functions that it calls (we call these programs 'GPU programs'). The term 'concolic' is a portmanteau of the terms 'Concrete' and 'Symbolic.' Concolic verifiers are gaining widespread adoption in many areas of software testing. They aim to achieve the union of the good features of concrete and symbolic verification methods, while also aiming for the intersection of their disadvantages. GKLEE extends KLEE in many ways. While KLEE provides the basic capabilities for sequential program analysis, GKLEE ('GPU + KLEE') extends KLEE to provide self-contained and powerful facilities for analyzing GPU programs.
Github repository: Gklee main repository for sources and docs
NOTE: A comprehensive list of publications can be found on THIS PAGE.
- Peng Li, Guodong Li, and Ganesh Gopalakrishnan, “Practical Symbolic Checking of GPU Programs”, Supercomputing 2014. [PDF] [BIB]
- Peng Li, Guodong Li, and Ganesh Gopalakrishnan, “Parametric Flows: Automated Behavior Equivalencing for Symbolic Analysis of Races in CUDA Programs”, Supercomputing 2012, Salt Lake City, November 2012. [.bib]
- Guodong Li and Ganesh Gopalakrishnan, “Parameterized Verification of GPU Kernels”, PLC Workshop 2012 (an IPDPS 2012 workshop) [.bib]
- Guodong Li, Peng Li, Geof Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, and Sreeranga P. Rajan, “GKLEE: Concolic Verification and Test Generation for GPUs,” Principles and Practices of Parallel Programming (PPoPP), February, 2012. Paper PDF and a Remote Execution Portal [.bib]