Verifying CUDA programs using SMT-based context-bounded model checking
Verifying CUDA programs using SMT-based context-bounded model checking
复制标题
使用基于 SMT 的上下文边界模型检查来验证 CUDA 程序
DOI：
10.1145/2851613.2851830
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
R. Ferreira
中科院分区：
文献类型：
--
作者：
P. A. Pereira;Higo F. Albuquerque;Hendrio Marques;I. D. Silva;C. Carvalho;L. Cordeiro;Vanessa Santos;R. Ferreira
我们提出ESBMC-GPU，ESBMC模型检查器的扩展，旨在验证为CUDA框架编写的GPU程序。ESBMC-GPU使用操作模型进行验证，即，标准CUDA库的抽象表示，保守地近似其语义。ESBMC-GPU通过显式探索可能的交织（直到给定的上下文边界）来验证CUDA程序，同时象征性地处理每个交织本身。实验结果表明，ESBMC-GPU能够检测更多的属性违规，同时保持较低的错误率。
We present ESBMC-GPU, an extension to the ESBMC model checker that is aimed at verifying GPU programs written for the CUDA framework. ESBMC-GPU uses an operational model for the verification, i.e., an abstract representation of the standard CUDA libraries that conservatively approximates their semantics. ESBMC-GPU verifies CUDA programs, by explicitly exploring the possible interleavings (up to the given context bound), while treating each interleaving itself symbolically. Experimental results show that ESBMC-GPU is able to detect more properties violations, while keeping lower rates of false results.