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.

Downloads


Github repository: Gklee main repository for sources and docs

Publications

NOTE: A comprehensive list of publications can be found on THIS PAGE.