Trabalho em anais de eventoOpen Access
Bounded model checking of C++ programs based on the Qt cross-platform framework (journal-first abstract)
MONTEIRO, FELIPE R.; GARCIA, MÁRIO A. P.; CORDEIRO, LUCAS C.; DE LIMA FILHO, EDDIE B
Resumo
Resumo
This work proposes an abstraction of the Qt framework, named as Qt Operational Model (QtOM), which is integrated into two different verification approaches: explicit-state model checking and symbolic (bounded) model checking. The proposed methodology is the first one to formally verify Qt-based applications, which has the potential to devise new directions for software verification of portable code. The full version of this paper is published in Software Testing, Verification and Reliability, on 02 March 2017 and it is available at https://doi.org/10.1002/stvr.1632.
Autoria
Autores do grupo (1)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
Qt frameworkbounded model checkingsymbolic model checkingexplicit-state model checkingC programssoftware verificationcross-platform softwareportable codeformal verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento