Skip to main content
PPGEE/UFAM

Artigo em periódicoOpen Access

ESBMC-GPU A context-bounded model checking tool to verify CUDA programs

SOUSA, F. R. M.2017SOUSA, F. R. M.; DA S. ALVES, ERICKSON H.; SILVA, ISABELA S.; ISMAIL, HUSSAMA I.; CORDEIRO, L. C.; DE LIMA FILHO, EDDIE B

2018 • Science of Computer Programming • 23 citações

Resumo

Resumo

The Compute Unified Device Architecture (CUDA) is a programming model used for exploring the advantages of graphics processing unit (GPU) devices, through parallelization and specialized functions and features. Nonetheless, as in other development platforms, errors may occur, due to traditional software creation processes, which may even compromise the execution of an entire system. In order to address such a problem, ESBMC-GPU was developed, as an extension to the Efficient SMT-Based Context-Bounded Model Checker (ESBMC). In summary, ESBMC processes input code through ESBMC-GPU and an abstract representation of the standard CUDA libraries, with the goal of checking a set of desired properties. Experimental results showed that ESBMC-GPU was able to correctly verify 85% of the chosen benchmarks and it also overcame other existing GPU verifiers regarding the verification of data-race conditions, array out-of-bounds violations, assertive statements, pointer safety, and the use of specific CUDA features.

palavras-chave

Palavras-chave

SMT-based model checkingpointer safetyparallel program verification

Volume

152

Páginas

63-69

Editora

Elsevier BV

Status

Published

links

DOI

10.1016/j.scico.2017.09.005

Link Externo

https://doi.org/10.1016/j.scico.2017.09.005

Repositório

https://research.manchester.ac.uk/en/publications/a813bf14-efac-4e4a-82b6-c83826ca1c29

Abrir publicação

Artigo em periódico

Electrocardiographic signal compression based on distributed source codingDE SOUZA, PATRESE E.B.2027DE SOUZA, PATRESE E.B.; DE LIMA FILHO, EDDIE B.; CORDEIRO, LUCAS C.; DE MELO, WHEIDIMA C.; DA SILVA, WALDIR S.; CARVALHO, CELSO B2027 • Biomedical Signal Processing and Control
Handling Asynchronous Scheduling Functions in Periodic Event-Triggered Gain-Scheduled Control With Guaranteed Polytopic InclusionCOUTINHO, Pedro Henrique Silva2026 COUTINHO, Pedro Henrique Silva; PESSIM, Paulo Sérgio Pereira; BESSA, Iury Valente; PEIXOTO, Márcia Luciana da Costa; PALHARES, Reinaldo Martinez2026 • IEEE Transactions on Cybernetics2citações
Systematic LMI approaches to design multivariable sliding mode controllers for uncertain systemsCOUTINHO, Pedro Henrique Silva2026COUTINHO, Pedro Henrique Silva; BESSA, Iury Valente; RODRIGUES, Victor Hugo Pereira; OLIVEIRA, Tiago Roux2026 • Automatica1citações
Finding software vulnerabilities in large C projects via bounded model checkingDE SOUSA, JANISLLEY O.2026DE SOUSA, JANISLLEY O.; DE FARIAS, BRUNO C.; DA SILVA, THALES A.; TIHANYI, NORBERT; DUBNICZKY, RICHARD A.; FILHO, EDDIE B. L.; CORDEIRO, LUCAS C2026 • International Journal on Software Tools for Technology Transfer

Ver todas as publicações