一句话：提出 Qt 操作模型（QtOM），首次将显式状态与有界符号模型检测结合，用于 Qt 应用的形式化验证。
基于 Qt 框架的 C++ 应用因框架本身复杂而难以进行形式化验证。本文提出一种 Qt 框架的抽象——Qt 操作模型（QtOM），并将其集成到两种验证途径中：显式状态模型检测与符号（有界）模型检测。该方法被作者称为首个对基于 Qt 的应用进行形式化验证的方法，有望为可移植代码的软件验证开辟新方向。论文完整版发表于 Software Testing, Verification and Reliability（2017 年 3 月 2 日）。
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.
@inproceedings{paperbot4705,
title = {Bounded model checking of C++ programs based on the Qt cross-platform framework (journal-first abstract)},
author = {Felipe R. Monteiro and Mário A. P. Garcia and Lucas C. Cordeiro and Eddie B. de Lima Filho},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3241981}
}