15230

Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking

Phillipe A. Pereira, Higo F. Albuquerque, Hendrio M. Marques, Isabela S. Silva, Celso B. Carvalho, Lucas C. Cordeiro
Federal University of Amazonas
ACM Symposium on Applied Computing (SAC), 2016
@article{pereira2016verifying,

   title={Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking},

   author={Pereira, Phillipe A and Albuquerque, Higo F and Marques, Hendrio M and Silva, Isabela S and Carvalho, Celso B and Cordeiro, Lucas C},

   year={2016}

}

Download Download (PDF)   View View   Source Source   Source codes Source codes

Package:

503

views

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.
VN:F [1.9.22_1171]
Rating: 5.0/5 (1 vote cast)
Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking, 5.0 out of 5 based on 1 rating

* * *

* * *

TwitterAPIExchange Object
(
    [oauth_access_token:TwitterAPIExchange:private] => 301967669-yDz6MrfyJFFsH1DVvrw5Xb9phx2d0DSOFuLehBGh
    [oauth_access_token_secret:TwitterAPIExchange:private] => o29ji3VLVmB6jASMqY8G7QZDCrdFmoTvCDNNUlb7s
    [consumer_key:TwitterAPIExchange:private] => TdQb63pho0ak9VevwMWpEgXAE
    [consumer_secret:TwitterAPIExchange:private] => Uq4rWz7nUnH1y6ab6uQ9xMk0KLcDrmckneEMdlq6G5E0jlQCFx
    [postfields:TwitterAPIExchange:private] => 
    [getfield:TwitterAPIExchange:private] => ?cursor=-1&screen_name=hgpu&skip_status=true&include_user_entities=false
    [oauth:protected] => Array
        (
            [oauth_consumer_key] => TdQb63pho0ak9VevwMWpEgXAE
            [oauth_nonce] => 1480779823
            [oauth_signature_method] => HMAC-SHA1
            [oauth_token] => 301967669-yDz6MrfyJFFsH1DVvrw5Xb9phx2d0DSOFuLehBGh
            [oauth_timestamp] => 1480779823
            [oauth_version] => 1.0
            [cursor] => -1
            [screen_name] => hgpu
            [skip_status] => true
            [include_user_entities] => false
            [oauth_signature] => 1rXSjWF2Gl17LCSXmTYTJvJSsL8=
        )

    [url] => https://api.twitter.com/1.1/users/show.json
)
Follow us on Facebook
Follow us on Twitter

HGPU group

2079 peoples are following HGPU @twitter

HGPU group © 2010-2016 hgpu.org

All rights belong to the respective authors

Contact us: