Title
Bounded model checking of C++ programs based on the Qt cross-platform framework (journal-first abstract).
Abstract
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.
Year
DOI
Venue
2018
10.1145/3238147.3241981
ASE
Keywords
Field
DocType
Software Engineering, Qt Framework, Model Checking, Formal Verification, Verification in Industrial Practice
Programming language,Abstraction,Model checking,Computer science,Theoretical computer science,Cross-platform,Software testing,Formal verification,Bounded function,Software verification
Conference
ISSN
ISBN
Citations 
1527-1366
978-1-4503-5937-5
0
PageRank 
References 
Authors
0.34
3
4
Name
Order
Citations
PageRank
Felipe R. Monteiro1195.85
Mário A. P. Garcia200.34
Lucas C. Cordeiro3338.51
E. B. de Lima Filho44512.51