Bounded model checking of C++ programs based on the Qt cross-platform framework (journal-first 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 appl...

Full description

Saved in:
Bibliographic Details
Main Authors: Monteiro, Felipe R., Garcia, Mário A. P., Cordeiro, Lucas C., de Lima Filho, Eddie B.
Format: Conference Proceeding
Language:English
Subjects:
Formal Verification
General and reference > Cross-computing tools and techniques > Verification
Model Checking
Qt Framework
Software and its engineering > Software creation and management > Software verification and validation > Formal software verification
Software and its engineering > Software organization and properties > Software functional properties > Formal methods > Model checking
Software and its engineering > Software organization and properties > Software functional properties > Formal methods > Software verification
Software Engineering
Verification in Industrial Practice
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2643-1572
DOI:10.1145/3238147.3241981