模型检测作为提高软件正确性的有效技术被广泛研究，并于近年开始实际应用于计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中，取得了令人瞩目的成功。然而，现有技术和工具仍无法实现对大规模软件系统正确性的验证。研究所着眼于可处理较大规模验证问题的限界模型检测技术，为进一步提升其验证能力和性能，提出新型的基于混成计算的多核限界模型检测技术。
针对上述挑战，研究团队提出基于混成计算的限界模型检测技术，将显式状态空间搜索技术与符号化限界模型检测技术进行融合，对系统状态空间进行有效压缩并进行正确性的形式化验证；开发出模型检测工具Garakabu2，可对并发及异构嵌入式软件系统进行正确性验证；提出定理证明与模型检测技术融合的方法论并实际应用于电子政务系统的验证；提出基于OpenScenario和决策表的自动驾驶控制决策满足交通法规的形式化验证技术。
该研究方向发表如下代表性论文：
[1] Weiqiang Kong, Gang Hou, Xiangpei Hu,et al. Garakabu2: an SMT-based bounded model checker
for HSTM designs in ZIPC. Journal of Information Security and Applications, 2016, 31: 61-74.
[2] Weiqiang Kong, Leyuan Liu, Takahiro Ando,et al. Facilitating Multicore Bounded Model
Checking with Stateless Explicit-State Exploration. The Computer Journal, 2015, 58(11):2824-2840.
[3] Weiqiang Kong, Gang Hou, Xiangpei Hu,et al. ZipPath: A Simple-But-Useful Path Finder for
HSTM Designs in ZIPC. IEEE International Conference on Agents (ICA-16) 2016.
